HACL* is a formally verified library of modern cryptographic algorithms written in the F* language and compiled to portable C. Each implementation in HACL* is verified for:
- Memory Safety in the C memory model
- Functional Correctness against a formal specification also written in F*
- Secret Independence, i.e. that control flow and memory accesses do not depend on secrets
Once these properties are proved, the code is compiled to C using a compiler called KaRaMeL. HACL* includes portable C implementations for a wide variety of modern crypto algorithms, including hash functions, encryption schemes, Diffie-Hellman, elliptic curves, and signature schemes. For each algorithm, HACL* includes a reference implementation in portable C, and often also includes verified implementations optimized for specific SIMD platforms such as Intel AVX2, AVX512, and ARM Neon.
The libcrux library currently uses the following verified implementations from HACL*:
- ChaCha20 - portable C + Intel AVX2 + ARM Neon
- Poly1305 - portable C + Intel AVX2 + ARM Neon
- ChaCha20Poly1305 - portable C
- Curve25519 - portable C + Intel ADX+BMI2 (using ValeCrypto)
- SHA-2 - portable C
- SHA-3 - portable C
We pull code from the HACL* repository and run the verification on the whole repository using the provided Makefile. The build depends upon F* and KaRaMeL. There is also a Docker image and a Nix recipe for building HACL*. Once all the code is verified, the generated C code is taken from dist/.
For each algorithm we import into libcrux, we inspect the high-level verified APIs provided by HACL* and reflect the correct types and pre-conditions in the libcrux Rust APIs. This is a manual process and is carefully reviewed by multiple developers. We include pointers to the formal specs, the F* APIs, and the C APIs for all the algorithms we use in libcrux:
- ChaCha20 - Spec, F* API, C API
- Poly1305 - Spec, F* API, C API
- ChaCha20Poly1305 - Spec, F* API, C API
- Curve25519 - Spec, F* API, C API
- SHA-2 - Spec, F* API, C API
- SHA-3 - Spec, F* API, C API
We can formally relate crypo specification in hacspec to those used by HACL*, by first compiling the hacspec to F* and then proving that the two specifications are equivalent in F*. In the subdirectory spec-equivalence We show how this can be done for two algorithms.
We start from the Chacha20 specification in hacspec and compile it to F* using the Circus tool. We then prove that the result is equivalent to the F* Chacha20 specification used in HACL*. The proof of equivalence is in Hacspec.Chacha20.Proof.fst and it needs an F* installation to verify.
As with ChaCha20, we take the Poly1305 specification in hacspec and compile it to F* using the Circus tool. We then prove that the result is equivalent to the F* Poly1305 specification used in HACL*. The proof of equivalence is in Hacspec.Chacha20.Proof.fst and it needs an F* installation to verify.
Spec equivalence proofs for other algorithms are ongoing. In the future, we hope that new HACL* implementations will start from the hacspec-generated specs, so that spec equivalence proofs will become unnecessary.
HACL* and its associated proof methodologies have been published in the following papers:
- J. K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, “Hacl*: A verified modern cryptographic library,” in Proceedings of the 2017 ACM SIGSAC conference on computer and communications security, CCS 2017, dallas, tx, usa, october 30 – november 03, 2017, 2017, p. 1789–1806.
- J. Protzenko, J. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Béguelin, A. Delignat-Lavaud, C. Hritcu, K. Bhargavan, C. Fournet, and N. Swamy, “Verified low-level programming embedded in F*,” PACMPL, vol. 1, iss. {ICFP}, p. 17:1–17:29, 2017.
- J. Protzenko, B. Beurdouche, D. Merigoux, and K. Bhargavan, “Formally Verified Cryptographic Web Applications in WebAssembly,” in IEEE Symposium on Security and Privacy (S&P), 2019.
- J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, A. D. -, C. Fournet, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. M. Wintersteiger, and S. Z. Béguelin, “Evercrypt: A fast, verified, cross-platform cryptographic provider,” in 2020 IEEE symposium on security and privacy, SP 2020, san francisco, ca, usa, may 18-21, 2020, 2020, p. 983–1002.
- M. Polubelova, K. Bhargavan, J. Protzenko, B. Beurdouche, A. Fromherz, N. Kulatova, and S. Z. Béguelin, “Haclxn: verified generic SIMD crypto (for all your favourite platforms),” in CCS ’20: 2020 ACM SIGSAC conference on computer and communications security, virtual event, usa, november 9-13, 2020, 2020, p. 899–918