|
|
Jean GOUBAULT-LARRECQ
Professeur associé
Laboratoire Spécification et Vérification
CNRS UMR 8643
École Normale Supérieure de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex - France
|
|
|
- notes de cours
- Quelques exposés récents:
- L'exposé "Cryptographic Protocol Analysis on Real C Code", présenté
à VMCAI'05, 19 février 2005;
- L'exposé "Relations logiques pour types monadiques ... et homologie?" du séminaire CATIA, Université Montpellier II, 14 février 2003 : ps pdf;
- L'exposé "Une fois qu'on n'a pas trouvé de preuve,
comment le faire comprendre
à un assistant de preuve?", journées francophones des langages
applicatifs (JFLA'04),
26 janvier 2004.
Il y est notamment question de protocoles cryptographiques, de logique,
d'automates d'arbres, et de l'outil H1 (bientôt sur vos écrans!).
Version étendue à SASYFT'2004 (ci-dessous), en anglais.
- L'exposé "On cryptographic protocols,
regular tree languages,
and automated deduction", invité à SASYFT'2004, Orléans, France, 21 juin 2004. Un peu étendu par rapport à celui des JFLA'2004, et en anglais.
- L'exposé "Plate-forme de détection d'intrusions Orchids -
Analyse et corrélation temporelle d'évènements en temps réel",
journées INRIA-industrie 2004, 27 janvier 2004.
- L'exposé "protocoles cryptographiques, analyse de code, détection d'intrusions", séminaire de cryptographie de Rennes, 30 janvier 2004. Un petit survol du précédent et de celui des JFLA, avec en plus l'attaque OpenSSL v2 comme transition habile entre les premier et troisième thèmes de l'exposé. (Où est passé le second? Je n'en ai effectivement pas parlé.)
- La page d'ORCHIDS,
un logiciel de détection d'intrusions temps réel, multi-événements, multi-sources,
fondé sur une approche efficace de model-checking de logique temporelle
(en cours de développement).
- La page de CSur,
un outil en cours de développement d'analyse statique de code C,
dont le but est de détecter des fuites de secrets (comme dans
les protocoles cryptographiques, mais sur du code C réel).
- le langage HimML
- Les contrats que je gère au LSV, ou auxquels je participe:
- le projet DICO (responsable);
- l'ACI Jeunes Chercheurs Intrusion (titulaire);
- l'ACI cryptologie PSI-robuste (responsable);
- l'action INRIA Futurs SECSI (responsable scientifique);
- Anciens contrats:
- le projet EVA (participant);
- l'ACI cryptologie VERNAM (participant);
- L'atelier "Sécurité des Communications sur Internet" (SECI'02, Tunis, 19-21 septembre 2002), dont je suis président du comité de programme:
- Les actes, en PDF ou en Postscript (un seul gros fichier bien massif);
- Le sommaire, avec pointeurs vers les papiers individuels;
- Les actes, papier par papier comme ci-dessus, mais dans une seule archive gzippée.
|
|