| Title | HACL*: A Verified Modern Cryptographic Library |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Zinzindohoué, Jean-Karim, Bhargavan, Karthikeyan, Protzenko, Jonathan, Beurdouche, Benjamin |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | compiler security, composability, cryptographic library, formal methods, pubcrawl, Resiliency, secure compilation, software verification, vectorized code |
| 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. |
| URL | http://doi.acm.org/10.1145/3133956.3134043 |
| DOI | 10.1145/3133956.3134043 |
| Citation Key | zinzindohoue_hacl*:_2017 |
HACL*: A Verified Modern Cryptographic Library