Software:EverCrypt
| Developer(s) | Microsoft Research, Inria, Carnegie Mellon University |
|---|---|
| Repository | github |
| Written in | F* |
| Type | Cryptography API |
| License | Apache License 2.0[1] |
| Website | hacl-star |
EverCrypt is a verified software library of cryptographic functions developed as part of Project Everest[2], a collaboration between Microsoft Research, Inria, and Carnegie Mellon University. It provides strong mathematical guarantees about the security and correctness of its cryptographic implementations, while achieving strong performance, in some cases even matching or beating other libraries[3][4].
EverCrypt is implemented and verified in the F* programming language. Once verified, EverCrypt's F* code extracts to a mixture of C and assembly, and is callable from C clients. Wrappers allow the use of EverCrypt in Rust and OCaml programs. A subset of the code also compiles to WebAssembly, enabling the use of the library for any Web context.
EverCrypt is an open-source library licensed under the terms of the Apache License 2.0.
Verified Software
Formal verification involves using software tools to analyze all possible behaviors of a program and prove mathematically that they comply with the code’s specification (i.e., a machine-readable description of the developer’s intentions). Unlike software testing, formal verification provides strong guarantees that a program behaves as expected and is free from entire classes of errors.
EverCrypt relies on formal verification to provide the following guarantees:
- Memory safety: The code is free from common bugs and vulnerabilities like buffer overflows, null-pointer dereferences, use-after-frees, and double-frees.
- Type safety: The code respects the interfaces among its components including any abstraction boundaries; e.g., one component never passes the wrong kind of parameters to another, or accesses its private state.
- Functional correctness: The code’s input/output behavior is fully characterized by simple mathematical functions derived directly from the official cryptographic standards (e.g., from NIST or the IETF).
- Secret Independence: Observations about the code’s low-level behavior (specifically, the time it takes to execute or the memory addresses that it accesses) are independent of the secrets manipulated by the library. Hence, an adversary monitoring these “side-channels” learns nothing about the secrets. Information may still be leaked via other side channels, however, for example via electromagnetic radiation or speculative execution.
Architecture
At its core, EverCrypt relies on two components written in F*: HACL*[5][6] and Vale[7][8]. Vale is a framework to verify optimized cryptographic implementations written in assembly. HACL* is a verified library of highly efficient C implementations of cryptographic algorithms.
EverCrypt brings HACL* and Vale together under a single, unified C API. For a given algorithm, it automatically picks the best Vale or HACL* implementation available depending on the machine the code is running on (multiplexing). Furthermore, it offers a single, agile API for all algorithms from the same family (for instance, hashes), allowing clients to easily pick a different algorithm without modifying their code, when for instance a cryptographic algorithm becomes obsolete.
List of supported algorithms
- Authenticated encryption: AES-GCM, Chacha20-Poly1305
- Elliptic curves: Curve25519, P-256
- Signatures: Ed25519, P-256
- Cryptographic hash functions: MD5, SHA1, SHA2-224, SHA2-256, SHA2-384, SHA2-512, SHA3, Blake2
- Key derivation: HKDF
- Ciphers: AES-128, AES-256, Chacha20
- Message authentication code: HMAC, Poly1305
Adoption
EverCrypt (or portions thereof) has been deployed in the following projects:
- Mozilla Firefox[9]
- The Wireguard VPN[10]
- The Zinc crypto library for the Linux Kernel[11]
- The MirageOS unikernel[12]
- The Tezos blockchain[13]
Additionally, several verification projects rely on EverCrypt for their cryptographic needs. These include:
- miTLS[14], an implementation of the TLS protocol
- LibSignal*[15][16], an implementation of the Signal protocol
- A Merkle-tree library[17]
Reference section
- ↑ "EverCrypt - LICENSE". https://github.com/project-everest/hacl-star/blob/master/LICENSE.
- ↑ "Project Everest". https://project-everest.github.io/.
- ↑ Protzenko, Jonathan; Parno, Bryan; Fromherz, Aymeric; Hawblitzel, Chris; Polubelova, Marina; Bhargavan, Karthikeyan; Beurdouche, Benjamin; Choi, Joonwon et al. (2019). EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. https://eprint.iacr.org/2019/757.
- ↑ "How the EverCrypt Library Creates Hacker-Proof Cryptography" (in en). https://www.quantamagazine.org/how-the-evercrypt-library-creates-hacker-proof-cryptography-20190402/.
- ↑ Beurdouche, Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin (2017). HACL*: A Verified Modern Cryptographic Library. https://eprint.iacr.org/2017/536.
- ↑ Polubelova, Marina; Bhargavan, Karthikeyan; Protzenko, Jonathan; Beurdouche, Benjamin; Fromherz, Aymeric; Kulatova, Natalia; Zanella-Béguelin, Santiago (2020). HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). https://eprint.iacr.org/2020/572.
- ↑ Bond, Barry; Hawblitzel, Chris; Kapritsos, Manos; Leino, K. Rustan M.; Lorch, Jacob R.; Parno, Bryan; Rane, Ashay; Setty, Srinath et al. (2017) (in en). Vale: Verifying High-Performance Cryptographic Assembly Code. pp. 917–934. ISBN 978-1-931971-40-9. https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/bond.
- ↑ Fromherz, Aymeric; Giannarakis, Nick; Hawblitzel, Chris; Parno, Bryan; Rastogi, Aseem; Swamy, Nikhil (2019-01-02). "A verified, efficient embedding of a verifiable assembly language". Proceedings of the ACM on Programming Languages 3 (POPL): 63:1–63:30. doi:10.1145/3290376. https://doi.org/10.1145/3290376.
- ↑ "Security/CryptoEngineering/HACL* - MozillaWiki". https://wiki.mozilla.org/Security/CryptoEngineering/HACL*.
- ↑ "Zinc: a new kernel cryptography API [LWN.net"]. https://lwn.net/Articles/770750/.
- ↑ "[PATCH 3/17 zinc: introduce minimal cryptography library - Herbert Xu"]. https://lore.kernel.org/lkml/E1h7DgR-0001H9-UN@gondobar/.
- ↑ "Blog :: TLS 1.3 support for MirageOS". https://mirage.io/blog/tls-1-3-mirageos.
- ↑ "HACL* v2 integration (#589) · Issues · Tezos / tezos" (in en). https://gitlab.com/tezos/tezos/-/issues/589.
- ↑ "miTLS, Triple Handshake, SMACK, FREAK, Logjam, and SLOTH". https://www.mitls.org/.
- ↑ Protzenko, Jonathan; Beurdouche, Benjamin; Merigoux, Denis; Bhargavan, Karthikeyan (2019). Formally Verified Cryptographic Web Applications in WebAssembly. https://eprint.iacr.org/2019/542.
- ↑ "Signal*". https://signalstar.gforge.inria.fr/.
- ↑ "project-everest/hacl-star" (in en). https://github.com/project-everest/hacl-star.
 |
