libcrux - the formally verified crypto library
libcrux is a formally verified cryptographic library that brings together verified artifacts from different sources. It uses hacspec as a common language for the specifications underlying the correctness and security proofs.
Please refer to the Architecture document for a detailed overview of the libcrux architecture and properties and the formal verification directory for details on the underlying formal proofs.
Algorithms
Note The available algorithms is still work in progress and will grow in future.
| Algorithm | Platforms |
|---|---|
| AES | x64 (AES-NI) |
| AES-GCM | x64 (AES-NI) |
| Chacha20 | x64, arm64 |
| Poly1305 | x64, arm64 |
| Chacha20Poly1305 | x64, arm64 |
| Curve25519 | x64, arm64 |
| EdDSA 25519 | x64, arm64 |
| EcDSA P256 | x64, arm64 |
| Sha2 | x64, arm64 |
| Sha3 | x64, arm64 |
| Blake2 | x64, arm64 |
| HMAC | x64, arm64 |
| HKDF | x64, arm64 |
| Bls12-381 | x64, arm64 |
| HPKE | x64, arm64 |
Other platforms might work as well but are not tested or optimized for at this point.
Hardware support
The build enables all available hardware features for the target architecture. Further, the library always performs runtime checks to ensure that the required CPU features are available.
libcrux uses the following configurations for its hardware abstractions
- simd128 assumes 128 bit SIMD instructions on the platform. This implies SSE3 and SSE4.1 on x64 CPUs and NEON on arm CPUs.
- simd256 assumes 256 bit SIMD instructions on the platform This implies AVX and AVX2 on x64 CPUs.
Randomness
libcrux provides a DRBG implementation that can be used standalone (drbg::Drbg)
or through the Rng traits.
Verification status
As a quick indicator of overall verification status, subcrates in this workspace include the following badges:
to indicate that most (or all) of the code that is contained in default features of that crate is not (yet) verified.
to indicate that most (or all) of the code that is contained in the default feature set is verified.
In both cases, please refer to the more detailed notes on verification in each sub-crate to learn more about what has (or has not) been verified in the particular case.