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 Ecole Polytechnique and 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 large security-critical applications. My recent work focuses on using dependent type systems, such as F*. to investigate the (in)security of cryptographic protocols, such as TLS. A full list of my publications is available from my publications page.

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 AJACS grant on JavaScript security, and from the ERC H2020 Grant NEXTLEAP on privacy-preserving protocols for secure messaging.

Projects: HACL*, miTLS, F*, RefTLS, ProScript, SMACK-TLS, WebSpi, Defensive JavaScript, F7

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


PhD Students: Evmorfia-Iro Bartzia, Antoine Delignat-Lavaud, Jean Karim Zinzdohoue, Nadim Kobeissi
Positions: We are always on the lookout for outstanding masters interns, PhD candidates, and Post-Doctoral researchers. To apply, send me an email with your CV and a short research statement.

mailing address: INRIA, 23 avenue d'Italie, Paris 75013, France
email: <firstName>.<lastName>@inria.fr