Project Everest is a joint research effort between Microsoft Research, INRIA, Carnegie Mellon, and the University of Edinburgh. Our goal is to provide high-performance standards-based secure communication components (e.g., TLS and QUIC) backed by mathematical proofs of their correctness and security. Additionally, we aim to show that software with formal proofs can be developed and deployed at scale today, within the existing software ecosystem.
Our code is programmed in F*, a language designed for co-developing programs and proofs. We prove our code memory safe (no buffer overflows, no use-after-free, etc.); functional correct (we always compute the right result); side-channel resistant (ruling out cache and timing-based leaks); as well as provide several application-specific guarantees.
Our programming tools and verified components are open source on GitHub, including the following highlighted components:
Our code is distributed as a set of C files, for easy integration with existing code. Several large projects have already adopted our components, including Firefox, Windows, Wireguard, mbedTLS, the Tezos blockchain, and many others: you should too!
https://project-everest.github.io/
Jonathan Protzenko, PhD, (@_protz_) is a Senior Researcher at Microsoft Research in Redmond. His interests revolve around type systems, language design, and software verification. Jonathan drives the EverCrypt project and wrote the F*-to-C compiler used pervasively throughout Project Everest.
Nikhil Swamy, PhD, is a Principal Researcher at Microsoft Research in Redmond, working broadly in the area of programming languages and computer security. He leads the design and implementation of the F* programming language and co-leads Project Everest.