News & Events

---

Seminar: A report on Project Everest

Speaker: Jonathan Protzenko & Tahina Ramananandro (RiSE, Microsoft Research, Redmond)

Location: 60 Fifth Avenue 446

Date: May 2, 2019, 11:15 a.m.

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 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. We will present the project, as well as the many components of the verified software stack we are building.

We will focus in particular on EverCrypt, the cryptographic provider that powers our TLS implementation, offering a variety of cryptographic algorithms in both C and assembly. 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.

We will also present EverParse, our library and tools for verified efficient parsing and serialization for transport data formats such as TLS handshake messages.