I am a Researcher in the RiSE group at Microsoft Research Redmond, which I joined in Fall 2014. Previously, I was in the Gallium team at INRIA Paris from 2010 to 2014, designing and implementing Mezzo for my PhD under the direction of François Pottier.

My research now focuses on formally verifying critical software, i.e. showing with mathematical certainty that the software has no bugs and exhibits the intended behavior. To that end, I use the F* programming language, and its new Low* toolchain. It allows compiling a subset of F* programs to C for integration into existing software ecosystems. Code written in Low* and compiled by KReMLin has been integrated into Windows, Firefox, mbedTLS, and the Tezos blockchain, among others.

In addition to tooling, I work on the following software verification projects:

  • EverCrypt, a complete cryptographic library that offers abstraction, multiplexing, agility and CPU auto-detection, verified in F*, compiled to C and assembly
  • HACL*, a collection of verified cryptographic algorithms, verified in F*, compiled to C
  • miTLS, a verified implementation of QUIC and TLS 1.2/1.3 in F*, compiled to C

My work is part of the larger Everest Project, an ambitious research effort spanning three continents, five institutions and twelve timezones.

In my spare time, I maintain several open-source projects, including a Thunderbird addon that is now the 4th most-used addon with 200,000 users.

More information on the research and software pages.

Students

  • Son Ho (2020-), co-advised with Karthik Bhargavan at INRIA
  • Denis Merigoux (2018-), co-advised with Karthik Bhargavan at INRIA

News

  • 2021/01/22: IEEE Computer Magazine publishes a roundtable on verified cryptography, where I appear
  • 2021/01/08: Our paper on formalizing the French tax code gets accepted for CC’2021. Interesting Hacker News discussion.
  • 2020/09/22: attending a virtual HACS where I’ll talk about the latest, exciting developments in Everest-land
  • 2020/08/26: thrilled to chair PriSC 2021 with the excellent Deian Stefan; submit your best work!
  • 2020/05/15: new techniques for verified cryptography: HACLxN
  • 2020/02/04: a new verified component for Everest: EverQuic, now accepted at S&P’21
  • 2019/10/01: Our work on EverCrypt is accepted at IEEE S&P 2020
  • 2019/05/15: I’ll be at S&P to present our work on Signal*, a verified implementation of the Signal protocol compiled to WebAssembly.
  • 2019/04/02: delighted to announce that I’ll be at Daghstul this summer to give a lecture at the Second International Summer School on Metaprogramming
  • 2019/04/02: read more about EverCrypt on the official Microsoft Research Blog
  • 2019/04/02: Quanta Magazine talks about our work
  • 2019/04/02: we are announcing EverCrypt, a verified cryptographic library many years in the making
  • 2019/01/15: read more about Project Everest on the official Microsoft Research Blog
  • 2019/01/09: I had the pleasure of participating in the MSR Podcast Series

Recent blog entries

subscribe via RSS