Skip to content
/ libcrux Public
forked from cryspen/libcrux

The formally verified crypto library for Rust

License

Notifications You must be signed in to change notification settings

mtgag/libcrux

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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.

About

The formally verified crypto library for Rust

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • C 56.3%
  • Assembly 16.8%
  • Rust 13.7%
  • F* 11.5%
  • Python 0.8%
  • C++ 0.5%
  • Other 0.4%