Project Everest: Fast, Correct, and Secure Software for Deployment Now!

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:

• EverCrypt, a functionally correct and side-channel resistant cryptographic library that matches or exceeds the performance of any other library for many algorithms
• EverParse, a library of verified parsers and formatters for binary formats
• EverQuic-transport, an implementation of the QUIC transport layer proven cryptographically secure

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/