Romain Bardou

Mail : mon prénom at mon nom point fr

Blog

Efficient Padding Oracle Attacks (2012)

Le papier que nous publions à CRYPTO cet été fait l'objet de plusieurs articles, notamment sur internet. Les informations données sont cependant parfois imprécises ou exagérées. Notre FAQ répond aux questions que nous avons reçues. N'hésitez pas à lire l'article de Matthew Green qui donne un excellent aperçu de notre papier.

Thèse

J'ai effectué ma thèse de septembre 2007 à octobre 2011 à l'INRIA Saclay - Île-de-France avec Claude Marché, dans l'équipe ProVal.

Titre : Vérification de programmes avec pointeurs à l'aide de régions et de permissions
Téléchargez le résumé, le manuscript ou l'exposé.

Voir aussi Capucine.

Projets

Je contribue à Tookan, un outil pour l'analyse de Cryptoki.
Capucine, un prototype d'implémentation de mes travaux de thèse : un système de type avec régions et capacités pour la vérification déductive.
Melt permet d'écrire des documents LaTeX en OCaml. Il est composé d'une librairie pour produire des fichiers .tex, et d'un préprocesseur fournissant une syntaxe permettant le mélange d'OCaml et LaTeX. Voir les transparents.
Fury Puyo est un clone libre de Puyo Puyo, un puzzle game rapide et addictif. Il est codé en OCaml et utilise la librairie OCamlSDL.
Je contribue à Mlpost, une librairie pour OCaml permettant de produire des figures pour LaTeX par l'intermédiaire de Metapost.

Publications

[5] Romain Bardou, Riccardo Focardi, Yusuke Kawamoto, Lorenzo Simionato, Graham Steel and Joe-Kai Tsay. Efficient Padding Oracle Attacks on Cryptographic Hardware. In the 32nd International Cryptology Conference (CRYPTO'12) [ bib | pdf ©IACR ]

[4] Romain Bardou and Claude Marché. Perle de preuve : les tableaux creux. In Vingt-deuxièmes Journées Francophones des Langages Applicatifs (JFLA'11) [ bib | pdf ]

[3] Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Technical Report RR-7414, INRIA, 2010. [ bib | pdf ]

[2] Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, and Stéphane Lescuyer. Faire bonne figure avec Mlpost. In Vingtièmes Journées Francophones des Langages Applicatifs (JFLA'09) [ bib | pdf ]

[1] Romain Bardou. Ownership, Pointer Arithmetic and Memory Separation. In Formal Techniques for Java-like Programs (FTfJP'08), Paphos, Cyprus, July 2008. [ bib | pdf | pdf (long) | pdf (slides) ]

Exposés

Introduction to Functional Programming Using OCaml, ou : tentative de conversion de chimistes de Fortran à OCaml, le 6 Juillet 2011 pour le LCT, Jussieu.
Regions and Permissions for Data Invariants, présentation de mes travaux de thèse, le 14 Janvier 2011 pour les équipes INRIA Typical et ProVal.
Melt: LaTeX with OCaml, présentation de mon outil Melt permettant d'écrire des documents LaTeX en OCaml.
Regions and Permissions for Data Invariants, présentation de mes travaux de thèse, le 2 Novembre 2009 à Eindhoven pour l'action COST FVOOS, ainsi qu'à la réunion d'équipe ProVal du 25 Septembre 2009.
Capacités, invariants et régions abstraites, présentation de mes travaux de thèse, le 13 Mars 2009 pour l'ARC INRIA CeProMi.
If you only knew the power of the Darcs side... une présentation du gestionnaire de version distribué Darcs.
Regional Logic et Dynamic Frames, une présentation des cadres dynamiques de Ioannis T. Kassios et de la logique de région d'Anindya Banerjee et al.

Stages

Mars-Juillet 2007 : Invariants de classe et systèmes d'ownership, à l'INRIA Futurs (maintenant INRIA Saclay - Île-de-France), avec Claude Marché
Avril-Août 2006 : Unions de variants polymorphes abstraits, à l'université de Nagoya (Japon), avec Jacques Garrigue
- Rapport
- Présentation
Juin-Juillet 2005 : Typage des modules récursifs en Caml, au LIP, avec Tom Hirschowitz
- Rapport
- Présentation

[5]	Romain Bardou, Riccardo Focardi, Yusuke Kawamoto, Lorenzo Simionato, Graham Steel and Joe-Kai Tsay. Efficient Padding Oracle Attacks on Cryptographic Hardware. In the 32nd International Cryptology Conference (CRYPTO'12) [ bib \| pdf ©IACR ]
[4]	Romain Bardou and Claude Marché. Perle de preuve : les tableaux creux. In Vingt-deuxièmes Journées Francophones des Langages Applicatifs (JFLA'11) [ bib \| pdf ]
[3]	Romain Bardou and Claude Marché. Regions and permissions for verifying data invariants. Technical Report RR-7414, INRIA, 2010. [ bib \| pdf ]
[2]	Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, and Stéphane Lescuyer. Faire bonne figure avec Mlpost. In Vingtièmes Journées Francophones des Langages Applicatifs (JFLA'09) [ bib \| pdf ]
[1]	Romain Bardou. Ownership, Pointer Arithmetic and Memory Separation. In Formal Techniques for Java-like Programs (FTfJP'08), Paphos, Cyprus, July 2008. [ bib \| pdf \| pdf (long) \| pdf (slides) ]