Project Everest aims to build and deploy a verified HTTPS stack.
The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks such as FREAK and LogJam and emergency patches many times a year.
Project Everest proposes to solve this problem by constructing a high-performance, standards-compliant, and veriﬁed implementation of the full HTTPS ecosystem. We are looking to cover from the HTTPS API down to TLS and including cryptographic algorithms such as RSA and AES. At the TLS level, for instance, we will develop new implementations of existing and new protocol standards while formally proving that our implementations provide a secure-channel abstraction between the communicating endpoints. Project Everest aims to be a drop-in replacement for the HTTPS library in mainstream web browsers, servers, and other popular libraries and tools.
Project Everest is built as an open source project involving contributions from Microsoft, Microsoft-INRIA Partnership, Carnegie Mellon University, and the Community at large. For more information, see here.
The project brings together the following Microsoft Research projects
- miTLS – a verified implementation of TLS 1.2
- F* – an ML-like functional programming language aimed at program verification
- Dafny – a verification-aware programming language
- Z3 – a SMT theorem prover
- Ironclad – provably secure and reliable systems