7 releases

0.0.2-pre.2 Dec 1, 2023
0.0.2-pre.1 Sep 25, 2023
0.0.1 Jun 13, 2023
0.0.1-dev.3 Apr 18, 2023
0.0.0 Jan 10, 2023

#3 in #proofs

Download history 69/week @ 2024-03-13 35/week @ 2024-03-20 33/week @ 2024-03-27 74/week @ 2024-04-03 37/week @ 2024-04-10 38/week @ 2024-04-17 109/week @ 2024-04-24 129/week @ 2024-05-01 91/week @ 2024-05-08 85/week @ 2024-05-15 86/week @ 2024-05-22 152/week @ 2024-05-29 72/week @ 2024-06-05 93/week @ 2024-06-12 182/week @ 2024-06-19 173/week @ 2024-06-26

525 downloads per month

Apache-2.0

6MB
182K SLoC

C 113K SLoC // 0.1% comments GNU Style Assembly 42K SLoC Rust 15K SLoC // 0.0% comments Assembly 10K SLoC // 0.0% comments F* 1.5K SLoC // 0.0% comments Shell 44 SLoC // 0.2% comments

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.

Dependencies