About
I am a member of the Confidential AI team at Microsoft Research Cambridge, working on Security and Privacy of Machine Learning systems. Previously, I worked in the Constructive Security, and Programming Principles and Tools teams, most notably on Project Everest, building secure implementation of key components of the HTTPS ecosystem.
Before that, I held a Research Engineer position at Inria Paris, and Post-Doctoral positions at Microsoft Research and IMDEA Software. I got my PhD from École Nationale Supérieure des Mines de Paris while working at Inria Sophia Antipolis-Méditerranée on the formal verification of game-based proofs of security in cryptography.
Featured
Project Everest: Advancing the science of program proof
Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post—about the proving methodology and verification tools of Project Everest—is the third in…
Project Everest: Reaching greater heights in internet communication security
Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the verification tools and techniques the Everest team is using and…
Scaling the Everest of software security with Dr. Jonathan Protzenko
Episode 58, January 9, 2019 - Dr. Protzenko talks about what’s wrong with software (and why it’s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he’s been working on), and finally, acts as our digital Sherpa for Project Everest, an assault on software integrity and confidentiality that aims to build and deploy a verified HTTPS stack.
EverCrypt
EverCrypt is a high-performance, cross-platform, formally verified modern cryptographic provider distributed as a combined C/ASM library. EverCrypt packages cryptographic implementations from the HACL* and ValeCrypt projects, and automatically picks the fastest one available, depending on processor support and the target…