| CARVIEW |
Select Language
HTTP/2 200
date: Thu, 22 Jan 2026 00:00:38 GMT
content-type: text/html
content-length: 3061
server: OVHcloud
accept-ranges: bytes
vary: Accept-Encoding
content-encoding: gzip
Romain Bardou
Romain BardouMail : mon prénom at mon nom point fr |
 |
Blog
Articles divers et variés.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
- Juin-Juillet 2005 : Typage des modules récursifs en Caml, au LIP, avec Tom Hirschowitz