Skip to Main content Skip to Navigation
Conference papers

HACL * : A Verified Modern Cryptographic Library

Abstract : 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 cryptographic 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.
Complete list of metadata

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-01588421
Contributor : Benjamin Beurdouche <>
Submitted on : Saturday, December 8, 2018 - 11:28:13 AM
Last modification on : Tuesday, December 11, 2018 - 1:16:12 AM
Long-term archiving on: : Saturday, March 9, 2019 - 12:58:52 PM

File

haclstar.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01588421, version 2

Collections

Citation

Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche. HACL * : A Verified Modern Cryptographic Library. ACM Conference on Computer and Communications Security (CCS), Oct 2017, Dallas, United States. ⟨hal-01588421v2⟩

Share

Metrics

Record views

982

Files downloads

913