July 17th, 2019: EverCrypt: a no-excuses, industrial-grade cryptographic library

Time and Location

July 17th, 2019 at 7:00 PM
Room 1085, Building 30, Map to building 30,
Microsoft Campus,
156th Ave NE,
Redmond, WA 98052.

Title

EverCrypt: a no-excuses, industrial-grade cryptographic library, with full verification

Abstract

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

After a brief presentation of Everest at large, I will focus on EverCrypt, the cryptographic provider that powers our TLS implementation, offering a variety of cryptographic algorithms written in a mixture of C and assembly. I will detail the various techniques we used, the verification APIs we offer, and the state-of-the art performance we obtain. 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.

Speaker Bio

Jonathan Protzenko is a Researcher in the RiSE group at Microsoft Research Redmond, which he joined in Fall 2014.

Jonathan’s research focuses on formally verifying critical software, i.e. showing with mathematical certainty that the software has no bugs and exhibits the intended behavior. To that end, I use the F* programming language, and its new Low* toolchain. It allows compiling a subset of F* programs to C for integration into existing software ecosystems. Code written in Low* and compiled by KReMLin has been integrated into Windows, Firefox, mbedTLS, and the Tezos blockchain, among others.

Jonathan’s flagship project is EverCrypt, a complete cryptographic library that offers abstraction, multiplexing, agility and CPU auto-detection, verified in F*, compiled to C and assembly. My work is part of the larger Everest Project, an ambitious research effort spanning three continents, five institutions and twelve timezones.

In his spare time, he maintains several open-source projects, including a Thunderbird addon that is now the 4th most-used addon with 200,000 users.

A Word From Our Sponsor

“Molekule is a San Francisco-based science and clean technology company that has developed a fundamentally new approach to clean polluted air. While current air purifiers try to catch pollutants in filters, Molekule uses nanotechnology to break down and completely eliminate pollutants on a molecular level. Its new technology is the only one able to destroy the full spectrum of pollutants of allergens, bacteria, viruses, mold, and airborne chemicals. The technology was developed over the past 20 years at the University of Florida. Molekule devices are controlled and connected using modern software design and architecture principles in order to bring the best experience to customers. Firmware for Molekule devices is written in C++ using an actor model approach and highly test driven development focused using test frameworks for hardware in the loop testing as well as basic software unit testing.”

Resources

Video | Slides