I am a researcher (directeur de recherche) at Inria, where I lead the Prosecco project ("Programming Securely with Cryptography") at INRIA Paris. I also teach part-time at the Master Parisien de Recherche en Informatique (MPRI).

My research concerns the design and implementation of new program verification techniques that would enable formal analyses of real-world security applications. My recent work focuses on using dependent type systems, such as F*. to investigate the (in)security of cryptographic protocols, such as TLS, and to build verified cryptographic libraries, such as HACL*. A full list of my publications is available from my publications page.

I have also been involved in the design, analysis, and standardization of TLS 1.3 and Messaging Layer Security at the IETF.

My work is primarily funded by an ERC Consolidator Grant, titled "CIRCUS: Certified Implementations of Robust, Cryptographically Secure Components". I also receive some funds from the ANR SafeTLS grant, and from the Microsoft Everest Expedition.

Projects: HACL*, Project Everest, miTLS, F*, RefTLS, SMACK-TLS,

Program Committees: IEEE S&P 2016-2020, ACM CCS 2015-2019, Usenix Security 2017, IEEE CSF 2016, ACM POPL 2015, ETAPS POST 2015, SEC@SAC 2016, SEC@SAC 2015

Current PhD Students: Benjamin Beurdouche, Marina Polubelova, Natalia Kulatova, Denis Merigoux, Benjamin Lipp
Past PhD Students: Evmorfia-Iro Bartzia, Antoine Delignat-Lavaud, Jean Karim Zinzdohoue, Nadim Kobeissi

Positions: We are always on the lookout for outstanding interns, PhD candidates, and Post-Doctoral researchers. To apply, send me an email with your CV and a short research statement.
mailing address: INRIA, 2 rue Simone Iff, Paris 75012, France
email: <firstName>.<lastName>@inria.fr