Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary

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 verified 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.

GitHub Repo

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 https://project-everest.github.io/

Related Projects

The project brings together the following Microsoft Research projects

People

Publications

2016

Verified Secure Implementations of the HTTPS Ecosystem