EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
| Autor: | Nikhil Swamy, Antoine Delignat-Lavaud, Jonathan Protzenko, Joonwon Choi, Bryan Parno, Christoph M. Wintersteiger, Chris Hawblitzel, Aseem Rastogi, Natalia Kulatova, Aymeric Fromherz, Marina Polubelova, Santiago Zanella-Béguelin, Tahina Ramananandro, Karthikeyan Bhargavan, Benjamin Beurdouche, Cédric Fournet |
|---|---|
| Přispěvatelé: | Microsoft Research, Carnegie Mellon University [Pittsburgh] (CMU), Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Programming securely with cryptography (PROSECCO ) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Network security
business.industry Computer science Hash function API design 020207 software engineering Cryptography 02 engineering and technology Encryption Zero-cost generic programming [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] High-performance cryptographic functionalities [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Merkle-tree library EverCrypt Embedded system 0202 electrical engineering electronic engineering information engineering Curve25519 Secure network protocol 020201 artificial intelligence & image processing Cross-platform cryptographic provider business Communications protocol Production blockchain |
| Zdroj: | SP 2020-IEEE Symposium on Security and Privacy SP 2020-IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.983-1002, ⟨10.1109/SP40000.2020.00114⟩ IEEE Symposium on Security and Privacy 2020 IEEE Symposium on Security and Privacy (SP) |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|