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

Nikhil Swamy 7623202eb3 EverCrypt.AEAD.fsti and Spec.AEAD.fsti, with @aseemr and @santiago 5 years ago
.docker b065aa06dd replace sed slash with @ 5 years ago
apps 03c8dd43ff Use kremlib/compat for selected targets 5 years ago
code 8e20e26c69 [CI] regenerate hints 5 years ago
doc 0110905adf Keep a version of the CCS17 paper in doc/ 6 years ago
other_providers 94776d1768 Turn off Vale GCM for now 5 years ago
providers 7623202eb3 EverCrypt.AEAD.fsti and Spec.AEAD.fsti, with @aseemr and @santiago 5 years ago
secure_api 8e20e26c69 [CI] regenerate hints 5 years ago
snapshots 2f9cc3ccd8 Try another wild guess 5 years ago
specs 7623202eb3 EverCrypt.AEAD.fsti and Spec.AEAD.fsti, with @aseemr and @santiago 5 years ago
test df5706552f Remove LowCProvider from test Makefile 5 years ago
vale 8d8d63aed9 Need to pass more variables from the environment 5 years ago
.fstar_version a4ed973fc9 Revert "`Buffer`: test new specs for `rcreate_mm`, `rcreate_free`" 6 years ago
.gitattributes 65c38ea214 Start generating various flavors of HACL* in the dist/ directory 5 years ago
.gitignore 656019da5f Refresh snapshots following the merge + make verify part of the default target in secure_api (which now makes it a precondition for everest upgrade) 5 years ago
.gitmodules 933be84795 Remove some submodules; update OpenSSL 5 years ago
.kremlin_version 51c40b40b1 Painful merge. 5 years ago
CMakeLists.txt 2968421363 Support for more versions of HMAC in the top-level CMakeLists.txt 5 years ago
Dockerfile a9a2674d6d Dockerfile: improvements to build current toolchain 5 years ago
INSTALL.md 3e3e3d9eba Update INSTALL.md 6 years ago
LICENSE 88a7288816 License file for Apache2 6 years ago
Makefile 8bef9f882a Restore old target for the sake of CI 5 years ago
Makefile.build bab47d4fed Change path following cleanup in kremlib 5 years ago
Makefile.include bbd6a1ea04 Try to regenerate hints 5 years ago
Makefile.prepare 41ee5d2554 use fixed kremlin version 5 years ago
README.md 5e92915cf4 Update README.md 6 years ago

README.md

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

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.

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 (master 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 (benjamin.beurdouche@inria.fr)
  • Karthikeyan Bhargavan (karthikeyan.bhargavan@inria.fr)