Project Everest is a large, multi-year, collaborative research effort spread between Microsoft Research, Carnegie Mellon, INRIA and University of Edinburgh. The aim of Project Everest is to deploy formally verified implementations of the TLS protocol, which now powers the majority of online communications. Project Everest is about half-way through its projected five year lifespan.
After a brief presentation of Everest at large, I will focus on EverCrypt, the cryptographic provider that powers our TLS implementation, offering a variety of cryptographic algorithms written in a mixture of C and assembly. I will detail the various techniques we used, the verification APIs we offer, and the state-of-the art performance we obtain. EverCrypt is suitable for use by verified and unverified clients alike, using an agile and multiplexing API. Parts of EverCrypt have been deployed, among others, in Firefox, the Wireguard VPN, Windows, and the Tezos blockchain.
Jonathan Protzenko is a Researcher in the RiSE group at Microsoft Research Redmond, which he joined in Fall 2014.
Jonathan’s research 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.
Jonathan’s flagship project is EverCrypt, a complete cryptographic library that offers abstraction, multiplexing, agility and CPU auto-detection, verified in F*, compiled to C and assembly. My work is part of the larger Everest Project, an ambitious research effort spanning three continents, five institutions and twelve timezones.
In his spare time, he maintains several open-source projects, including a Thunderbird addon that is now the 4th most-used addon with 200,000 users.