blue03 / hacl-star

HACL*, a formally verified cryptographic library written in F*

HACL*

HACL* is a formally verified cryptographic library in F*, developed by the Prosecco team at INRIA Paris in collaboration with Microsoft Research, as part of Project Everest.

HACL stands for High-Assurance Cryptographic Library and its design is inspired by discussions at the HACS series of workshops. The goal of this library is to develop verified C reference implementations for popular cryptographic primitives and to verify them for memory safety, functional correctness, and secret independence.

More details about the HACL* library and its design can be found in our ACM CCS 2017 research paper: https://eprint.iacr.org/2017/536

All our code is written and verified in F* and then compiled to C via the KreMLin tool. Details on the verification and compilation toolchain and their formal guarantees can be found in the ICFP 2017 paper: https://arxiv.org/abs/1703.00053

Development branch

This branch holds the last public (stable) release of HACL*. Active development and integration, including HACLv2 and the EverCrypt provider, is happening on the fstar-master branch.

Warning

While HACL* is used in several products such as Mozilla Firefox or Wireguard, we highly recommand to consult the authors before using HACL* in production systems. Active development happens in different branches between releases and should not be used without advice. Next release is due for 2019.

Supported Cryptographic Algorithms

The primitives and constructions supported currently are:

• Stream ciphers: Chacha20, Salsa20
• MACs: Poly1305, HMAC
• Elliptic Curves: Curve25519
• Elliptic Curves Signatures: Ed25519
• Hash functions: SHA2 (256,384,512)
• NaCl API: secret_box, box, sign
• TLS API: IETF Chacha20Poly1305 AEAD

Developers can use HACL* through the NaCl API. In particular, we implement the same C API as libsodium for the NaCl constructions, so any application that relies on libsodium only for these constructions can be immediately ported to use the verified code in HACL* instead. (Warning: libsodium also implements other algorithms not in NaCl that are not implemented by HACL*)

The verified primitives can also be used to support larger F* verification projects. For example, HACL* code is used through the agile cryptographic model developed in secure_api/ as the basis for cryptographic proofs of the TLS record layer in miTLS. A detailed description of the code in secure_api/ and its formal security guarantees appears in the IEEE S&P 2017 paper: https://eprint.iacr.org/2016/1178.pdf

Licenses

All F* source code is released under Apache 2.0.

All generated C, OCaml, Javascript and Web Assembly code is released under MIT.

Installation

If you only are interested in the latest version of the generated C code, or Web Assembly code, installing the toolchain is not required. In that scenario, only a recent C compiler and CMake are needed for building libraries.

The latest version of the verified C code is available in snapshots/hacl-c.

The latest version of the Web Assembly code is available in snapshots/hacl-c-wasm.

HACL* relies on F* (stable branch) and KreMLin (stable branch) for verification, extraction to OCaml (specs/) and extraction to C (code/).

See INSTALL.md for more information on how to install the toolchain.

Verifying and Building HACL*

Type make to get more information:

HACL* Makefile:
If you want to run and test the C library:
- 'make build' will use CMake to generate static and shared libraries for snapshots/hacl-c (no verification)
- 'make build-make' will use Makefiles to do the same thing (no verification)
- 'make unit-tests' will run tests on the library built from the hacl-c snapshot (no verification)
- 'make clean-build' will clean 'build' artifacts

If you want to verify the F* code and regenerate the C library:
- 'make prepare' will try to install F* and Kremlin (still has some prerequisites)
- 'make verify' will run F* verification on all specs, code and secure-api directories
- 'make extract' will generate all the C code into a snapshot and test it (no verification)
- 'make test-all' will generate and test everything (no verification)
- 'make world' will run everything (except make prepare)
- 'make clean' will remove all artifacts created by other targets

Verification and C code generation requires F* and KreMLin. Benchmarking performance in test-all requires openssl and libsodium. An additional CMake build is available and can be run with make build-cmake.

Performance

To measure see the performance of HACL* primitives on your platform and C compiler, run the targets from test/Makefile if you have the dependencies installed. (experimental) To compare its performance with the C reference code (not the assembly versions) in libsodium and openssl, download and compile libsodium with the --disable-asm flag and openssl with the -no-asm flag.

While HACL* is typically as fast as hand-written C code, it is typically 1.1-5.7x slower than assembly code in our experiments. In the future, we hope to close this gap by using verified assembly implementations like Vale for some primitives.

Experimental features

The code/experimental directory includes other (partially verified) cryptographic primitives that will become part of the library in the near future:

• Randomness: System + RDRAND mixing
• Stream cipher: XSalsa20
• Encryption: AES-128, AES-256
• MACs: GCM
• Hash functions: Blake2s
• Key Derivation: HKDF
• Signatures: RSA-PSS

We are also working on a JavaScript backend for F* that would enable us to extract HACL* as a JavaScript library.

Authors and Maintainers

HACL* was originially developed as part of the Ph.D. thesis of Jean Karim Zinzindohoué in the Prosecco team at INRIA Paris. It contains contributions from many researchers at INRIA and Microsoft Research, and is being actively developed and maintained within Project Everest.

For questions and comments, or if you want to contribute to the project, do contact the current maintainers at:

• Benjamin Beurdouche ([email protected])
• Karthikeyan Bhargavan ([email protected])