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-2017, Usenix Security 2017, IEEE CSF 2016, ACM POPL 2015, ETAPS POST 2015, SEC@SAC 2016, SEC@SAC 2015

News: