Paper 2017/536

HACL*: A Verified Modern Cryptographic Library

Jean-Karim Zinzindohoué and Karthikeyan Bhargavan and Jonathan Protzenko and Benjamin Beurdouche

Abstract

HACL* is a new verified cryptographic library that implements popular modern cryptographic primitives such as the ChaCha20 and Salsa20 encryption algorithms, Poly1305 and HMAC authentication, SHA-256 and SHA-512 hash functions, the Curve25519 elliptic curve Diffie-Hellman group, and Ed25519 signatures. Using these primitives, HACL* implements the NaCl cryptographic API and can be used as a drop-in replacement for NaCl implementations like libsodium and TweetNaCl. HACL* also provides the cryptographic components for one of the mandatory ciphersuites of TLS 1.3, and is already being used within the miTLS verified implementation. HACL* is written and verified in the F* programming language and then compiled to readable C code. The F* source code is verified for side-channel mitigations, memory safety, and functional correctness with respect to succinct high-level specifications derived from the standard specification for each cryptographic primitive. The translation to C preserves these properties and the generated 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 implementations are as fast as the fastest C implementations in OpenSSL and libsodium, significantly faster than the reference C code in TweetNaCl and SuperCop, and between 3x-5x of hand-optimized assembly code. We show how to verify code that relies on low-level hardware features like 128-bit integers and vector instructions. A distinctive feature of HACL* is that we aggressively try to share code and verification effort across primitives, while preserving performance. Our results show that writing fast, verified, and self-contained C cryptographic libraries is now practical.