libcrux contains specifications in hacspec as well as efficient implementations of cryptographic primitives.
HACL* is a collection of high-assurance cryptographic algorithms originally developed as part of Project Everest and now maintained by the HACL Community. libcrux uses HACL* through the Rust bindings official HACL packages distribution.
TBD
The pipeline is described here.
Every implementation in libcrux is formally verified. But it is important to be precise about proven properties and how the properties proven translate to the code that's actually used.
The HACL toolchain is depicted above.
- The hacspec code is translated to F*, which is proven equivalent to the Low* implementation in HACL*.
- The Low* code is extracted to C with KaRaMel.
- The C API is wrapped in a safe Rust API.
- The Rust API is orchestrated depending on use case and available hardware.
The equivalence proofs in 1. and the extraction in 2. ensure that the C code
- is correct with respect to the specification
- has secret independent performance
- is memory safe
Because the C API can not guarantee certain preconditions expected in the proofs of the F* code (e.g. input sizes), these properties are ensured in the safe Rust wrapper (3).
TBD
The AUCurves toolchain is depicted above.
- The hacspec BLS spec contains unit tests and property tests.
- The hacspec code is translated to Coq, which is proven equivalent to the specification of fiat-cryptography. This has been done for the group operations on both G1 and G2.
- Fiat-cryptography can be use to generate efficient (C or rust) field operations for the fields underlying G1 and G2.
- Bedrock2 can be used to generate the group operations in C, or Rust. Printing to rust is done in Coq, but it is experimental and unverified. Alternatively, we can wrap the C code in a Rust API.
See the specs for a detailed list of proofs and properties.