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.
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.
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
- Papers@EuroS&P, June 2019
Our papers on proving WireGuard and on Noise Explorer appeared at IEEE EuroS&P 2019.
- Paper@Oakland, May 2019
Our paper on Verified Crypto Applicationa in WebAssembly appeared at IEEE S&P 2019.
- Paper@Oakland, May 2018
Our paper on TLS proxies appeared at IEEE S&P 2018.
- Paper@CCS, November 2017
Our paper on the HACL* cryptographic library appeared at ACM CCS 2017.
- Paper@ICFP, September 2017
Our paper on generating C code from verified F* programs appears at ICFP 2017.
- Award@Oakland, May 2017
Our paper on verifying TLS 1.3 using ProVerif and CryptoVerif was awarded the Distinguished Paper award at IEEE S&P (Oakland 2017).
- Papers@Oakland, May 2017
We had two papers on TLS 1.3 at IEEE S\&P (Oakland) 2017.
- Invited Talk@ACNS, July 2017
I gave an invited talk on High Assurance Cryptographic Software at ACNS 2016
- Impact@NIST, July 2017
NIST deprecated 3DES, partly due to our Sweet32 paper at CCS 2016.
- Papers@EuroS&P, April 2017
We had two papers at Euro S&P 2017, which was organized by my group in Paris.
- Award@France, November 2016
I was awarded the Prix Jeune Chercheur Inria – Academie des sciences 2016.
- Award@MSR, July 2016
I was given one of the Microsoft Research Outstanding Collaborator Awards
- Invited Talk@EUROCRYPT, May 2016
I gave an invited talk on protecting TLS against legacy crypto at EUROCRYPT 2016
- Paper@S&P, May 2016
Our paper on downgrade resilience in TLS, SSH, and IPsec appeared at IEEE S&P (Oakland) 2016
- Award@NDSS, February 2016
Our SLOTH paper on weak hash functions wins a Best Paper award at ISOC NDSS 2016
- Levchin Prize, January 2016
The miTLS project wins the Levchin Prize for significant contributions to real-world cryptography
- Sloth Attack, January 2016
We disclosed Sloth, a new attack on many TLS clients and servers, triggering security updates to many TLS libraries and web servers.
Some press: Register, Ars Technica
- Award@CCS, October 2015
Our Logjam paper on weak Diffie-Hellman groups wins a Best Paper award at ACM CCS 2015
- Paper@POPL 2016
Our paper on the new F* was accepted at POPL 2016
- Grant@Mozilla, October 2015
Mozilla Corporation has awarded our team a research grant to support our research on verifying TLS 1.3.
- Standard@IETF, September 2015
RFC 7627 our proposal to prevent the Triple Handshake attacks on TLS becomes an Internet standard.
- Song@CRYTPO, August 2015
Cryptographers sing "500 bits - Implementor's Lament": a concise summary of our recent attacks, Freak and Logjam, at the CRYPTO rump session.
- Award@WOOT, August 2015
Our paper on FlexTLS: a tool for testing TLS implementations won the Best Paper award at WOOT 2015
- Award@BlackHat, August 2015
Our paper on Logjam won a Pwnie award for Most Innovative Research at BlackHat 2015
- Award@S&P, May 2015
Our paper on state machine flaws in TLS implementations won the Distinguished Paper award at IEEE S&P (Oakland) 2015
- Logjam Attack, May 2015
We disclosed Logjam, a new attack on many TLS clients and servers, triggering security updates to many web browsers.
Security updates for Logjam: OpenSSL, Firefox, Windows, IBM
Some press: Wall Street Journal, Ars Technica, ZDnet
- Paper@WWW, May 2015
Our paper on origin confusion attacks on web servers appeared at WWW 2015
- FREAK Attack, March 2015
We disclosed FREAK, a new attack on TLS clients and servers, resulting in security updates to mainstream web browsers and TLS libraries.
Security updates for FREAK: OpenSSL, Windows, Apple
Some press: Washington Post, BBC, Figaro, New York Times, Guardian
- Paper@NDSS, February 2015
Our paper on analysing channel bindings in TLS, SSH, and IPsec appeared at NDSS 2015
- Talk@BlackHat, August 2014
Antoine Delignat-Lavaud presented our various new attacks on TLS and HTTPS at BlackHat USA 2014
- Paper@CRYPTO, July 2014
Our paper on proving security for an implementation of the TLS Handshake appeared at CRYPTO 2014
- Paper@S&P, May 2014
Our paper on triple handshake and cookie cutter attacks on TLS appeared at Oakland (IEEE S&P) 2014.
- Triple Handshake Attack, March 2014
We presented Triple Handshake attacks on authentication over TLS to the TLS working group at IETF'89.
Security updates (CVEs) for triple handshake attacks: Google Chrome, Mozilla NSS, Apple Safari/SecureTransport.
Some press: [1, 2, 3, 4, 5, 6, 7]
- Paper@POPL, January 2014
- Cookie Cutter Attack, October 2013
Security updates (CVEs) for cookie cutter attacks: Google Chrome, Apple Safari/CFNetwork