HACL*: A Verified Modern Cryptographic Library
- Karthikeyan Bhargavan ,
- Benjamin Beurdouche ,
- Jean-Karim Zinzindohoué ,
- Jonathan Protzenko
ACM CCS |
HACL* is a verified portable C cryptographic library that implements modern cryptographic primitives such as the ChaCha20 and Salsa20 encryption algorithms, Poly1305 and HMAC message authentication, SHA-256 and SHA-512 hash functions, the Curve25519 elliptic curve, and Ed25519 signatures.
HACL* is written in the F* programming language and then compiled to readable C code. The F* source code for each crypto- graphic primitive is verified for memory safety, mitigations against timing side-channels, and functional correctness with respect to a succinct high-level specification of the primitive derived from its published standard. The translation from F* to C preserves these properties and the generated C code can itself be compiled via the CompCert verified C compiler or mainstream compilers like GCC or CLANG. When compiled with GCC on 64-bit platforms, our primitives are as fast as the fastest pure C implementations in OpenSSL and Libsodium, significantly faster than the reference C code in TweetNaCl, and between 1.1x-5.7x slower than the fastest hand-optimized vectorized assembly code in SUPERCOP.
HACL* implements the NaCl cryptographic API and can be used as a drop-in replacement for NaCl libraries like Libsodium and TweetNaCl. HACL* provides the cryptographic components for a new mandatory ciphersuite in TLS 1.3 and is being developed as the main cryptographic provider for the miTLS verified implementation. Primitives from HACL* are also being integrated within Mozilla’s NSS cryptographic library. Our results show that writing fast, verified, and usable C cryptographic libraries is now practical.
Publication Downloads
EverCrypt
June 26, 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
June 26, 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.
HACL*
October 17, 2019
A High-Assurance Cryptographic Library (HACL*), a formally verified cryptographic library written in F*. This repository contains verified code for a library of modern cryptographic algorithms, including Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC, and HKDF.