I am a Principal 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 focuses on advancing the theory and practice of software verification, i.e. showing with mathematical certainty that a critical piece of code exhibits the intended behavior. This is important for the software industry (e.g. cryptography), but also for society at large (e.g. the law). See our interview in Quanta Magazine for an accessible introduction, or this roundtable on verified cryptography for a research perspective.

Current projects

Verified Protocol Stacks (2019-). Security protocols are pervasive in modern communication software, yet true end-to-end verification results for real-world protocols remain elusive. New developments:

  • Noise*, a protocol compiler, proven correct and secure once and for all – we generate 59 protocol stacks “for free”, complete with state machine and peer management, in C.
  • MLS* (ongoing), a hybrid JS/WebAssembly implementation of the MLS protocol with security proofs.
  • Signal*, a provably secure implementation of the Signal protocol, including compilation the Web via WebAssembly.

The Low* toolchain (2016-) compiles F* programs to C. Code written in Low* has been integrated into Windows, Firefox, mbedTLS, and the Tezos blockchain, among others. I co-lead several verified software libraries which use Low*, such as:

  • 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
  • EverQUIC, a verified implementation of the QUIC record layer, complete with a proof of cryptographic security

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

The Catala project (2020-) looks at the intersection of language design and computational law. I work on the design and formal aspects of the language, as well as applications in the context of US federal and local laws.

Open-source (2009-). 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

  • Théophile Wallez (2021-), co-advised with Karthik Bhargavan at INRIA
  • Son Ho (2020-), co-advised with Karthik Bhargavan at INRIA
  • Denis Merigoux (2018-2021), co-advised with Karthik Bhargavan at INRIA. Denis is now a junior researcher at INRIA.

News

  • 2021/09/16: I am co-chairing two upcoming POPL workshops: PriSC and ProLaLa – submit your best work!
  • 2021/09/09: I will present Catala at AISEC’21.
  • 2021/09/08: I will participate in a panel at PPDP’21 on “Applicability and usability of programming languages for legal contracts”.
  • 2021/08/18: We will present Catala at ICFP 2021.
  • 2021/05/12: keynote on Catala and formalizing the law
  • 2021/05/11: more coverage of Catala: reddit, hacker news, again
  • 2021/03/11: the ML’21 workshop website is up; I’m the chair, and expect you to submit your finest work!
  • 2021/01/22: IEEE Computer Magazine publishes a roundtable on verified cryptography, where I appear

Recent blog entries

subscribe via RSS