Paper 2017/536

HACL*: A Verified Modern Cryptographic Library

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

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 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.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint.
Keywords
implementationformal verification
Contact author(s)
jonathan protzenko @ gmail com
History
2017-09-01: last of 3 revisions
2017-06-08: received
See all versions
Short URL
https://ia.cr/2017/536
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/536,
      author = {Jean Karim Zinzindohoué and Karthikeyan Bhargavan and Jonathan Protzenko and Benjamin Beurdouche},
      title = {HACL*: A Verified Modern Cryptographic Library},
      howpublished = {Cryptology ePrint Archive, Paper 2017/536},
      year = {2017},
      note = {\url{https://eprint.iacr.org/2017/536}},
      url = {https://eprint.iacr.org/2017/536}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.