CryptoDB
Developing High-Performance Mechanically-Verified Cryptographic Code
| Authors: |
|
|---|---|
| Download: | |
| Presentation: | Slides |
| Honor: | Invited talk |
| Abstract: | Project Everest is constructing a high-performance, standards-compliant, formally verified implementation of the HTTPS ecosystem, including TLS, X.509, and the core cryptographic algorithms. This talk will present an overview of how we verify our implementations are correct, cryptographically secure, and resilient to basic side channels. We will focus on our EverCrypt cryptographic provider, a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. The API provably supports agility (choosing between multiple algorithms for the same functionality) and multiplexing (choosing between multiple implementations of the same algorithm). Through a combination of abstraction and zero-cost generic programming, we show how agility can simplify verification without sacrificing performance, and we demonstrate how C and assembly can be composed and verified against shared specifications. The result is several functionalities whose performance matches or exceeds the best unverified implementations. Altogether, EverCrypt consists of over 100K verified lines of specs, code, and proofs, and it produces over 45K lines of C and assembly code. |
Video from CHES 2019
BibTeX
@misc{ches-2019-29938,
title={Developing High-Performance Mechanically-Verified Cryptographic Code},
note={Invited talk},
address={Atlanta, Georgia, USA},
author={Bryan Parno},
year=2019
}