A formally verified cryptographic library written in the jasmin programming language with computer-verified proofs in EasyCrypt; libjade is part of the Formosa-Crypto project.
Each assembly implementation in libjade enjoys the following properties:
- Memory Safety
- Functional Correctness against a formal specification also written in EasyCrypt
- Timing Attack Protection
- Protection against Spectre v1
- Protection against Spectre v4
- Stack cleanup
libjade currently includes verified implementations for several hash functions, stream ciphers, authenticated encryption, scalar multiplication, and post-quantum cryptography. For each algorithm, libjade includes a reference implementation for x86 platforms, but also optimized SIMD implementations for AVX2 platforms where available.
The libcrux library currently uses the following verified implementations from HACL*:
- ChaCha20 - reference x86_64 + Intel AVX2
- Poly1305 - reference x86_64 + Intel AVX2
- Curve25519 - reference x86_64 + Intel ADX+BMI2
- SHA-3 - portable x86_64
TODO: something like the following
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/.
TODO: something like the following
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
TODO: somthing like the following
We can formally relate crypo specification in hacspec to those used by HACL*, by first compiling the hacspec to EasyCrypt and then proving that the two specifications are equivalent in EasyCrypt 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 EasyCrypt using the Circus tool. We then prove that the result is equivalent to the EasyCrypt Chacha20 specification used in libjade. The proof of equivalence is in and it needs an EasyCrypt installation to verify.
As with ChaCha20, we take the Poly1305 specification in hacspec and compile it to EasyCrypt using the Circus tool. We then prove that the result is equivalent to the EasyCrypt Poly1305 specification used in libjade. The proof of equivalence is in and it needs an EasyCrypt installation to verify.
libjade and its associated proof methodologies have been published in the following papers: