EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
- Jonathan Protzenko ,
- Bryan Parno ,
- Aymeric Fromherz ,
- Chris Hawblitzel ,
- Marina Polubelova ,
- Karthikeyan Bhargavan ,
- Benjamin Beurdouche ,
- Joonwon Choi ,
- Antoine Delignat-Lavaud ,
- Cédric Fournet ,
- Natalia Kulatova ,
- Tahina Ramananandro ,
- Aseem Rastogi ,
- Nikhil Swamy ,
- Christoph M. Wintersteiger ,
- Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy |
Published by IEEE
We present EverCrypt: 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 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. We substantiate the effectiveness of these techniques with new verified implementations (including hashes, Curve25519, and AES-GCM) whose performance matches or exceeds the best unverified implementations. We validate the API design with two high-performance verified case studies built atop EverCrypt, resulting in line-rate performance for a secure network protocol and a Merkle-tree library, used in a production blockchain, that supports 2.7 million insertions/sec. Altogether, EverCrypt consists of over 124K verified lines of specs, code, and proofs, and it produces over 29K lines of C and 14K lines of assembly code.
论文与出版物下载
EverCrypt
26 6 月, 2019
EverCrypt is a high-performance, cross-platform, formally verified modern cryptographic provider distributed as a combined C/ASM library. EverCrypt packages cryptographic implementations from the HACL* and ValeCrypt projects, and automatically picks the fastest one available, depending on processor support and the target execution environment (multiplexing). Furthermore, EverCrypt offers an (agile) API that makes it simple to switch between algorithms (e.g., from SHA2 to SHA3). Code from EverCrypt has been integrated in Linux, Firefox, the Tezos blockchain, the Election Guard project, and many more.
Vale
26 6 月, 2019
Vale (Verified Assembly Language for Everest) is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code. It uses existing verification frameworks, such as Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux. Additional architectures and platforms can be supported with no changes to the Vale tool. The Everest project uses Vale to provide verified assembly language code for performance-critical cryptographic algorithms, including AES-GCM, Curve25519, Poly1305, and SHA. Everest's EverCrypt API automatically chooses between Vale's assembly language code and HACL*'s C code depending on the cryptographic algorithm and the machine the code is running on.
EverCrypt: New Features and Deployments with Election Guard | JRC Workshop 2021
Systems 19 May 2021 Speaker: Jonathan Protzenko, Microsoft This virtual event brought together the PhD students and postdocs working on collaborative research engagements with Microsoft via the Swiss Joint Research Center, Mixed Reality & AI Zurich Lab, Mixed Reality & AI Cambridge Lab, Inria Joint Center, their academic and Microsoft supervisors as well as the wider research community. The event continued in the tradition of the annual Swiss JRC Workshops. PhD students and postdocs presented project updates and discussed their research with their supervisors and other attendants. In addition, Microsoft speakers provided updates on relevant Microsoft projects and initiatives. There were four event sessions according to research themes: Computer Vision, Systems, and AI Learn more about the Joint Research Center Workshop 2021 >