DOCSEARCHbyAlgolia
Submit Docs

libcrux: The Formally Verified Cryptography Library

repository·main·Indexed 42 days ago

https://github.com/celabshq/libcrux

A Rust implementation of formally verified, constant-time cryptography. It provides high-performance post-quantum cryptography including FIPS 203 ML-KEM, as well as implementations of AES-GCM, AES-CCM, Blake2, Chacha20-Poly1305, Curve 25519, ECDSA, and Ed25519. Many algorithms are derived from the HACL* project and verified using the F* framework for memory safety, functional correctness, and secret independence. Supports no_std environments and provides tools to extract implementations into C.

Tokens
71.5K
Snippets
231
Records
363
Agent score
54%

What's inside libcrux

  1. Overview of Formal Verification backends in libcrux

    main

    libcrux uses multiple formal verification backends to ensure the correctness of its cryptographic implementations. Documentation and proofs are organized by the specific backend used for each component:

    • AU Curves: Verification related to AU curves.
    • HACL*: Verification using the HACL* framework.
    • libjade: Verification using the libjade framework.
    • Vale: Verification using the Vale framework.

  3. Overview of Libcrux SHA3

    main

    The sha3 crate provides implementations of the SHA3 (FIPS 202) hashing algorithm. It is designed to be highly performant and portable, offering different implementation paths depending on the target architecture:

    • Portable implementation: A standard implementation that works across various platforms.
    • AVX2 optimized implementation: Leverages AVX2 instructions for high performance on supported x86 architectures.
    • Neon optimized implementation: Leverages Neon instructions for high performance on supported ARM architectures.

    The crate is suitable for embedded or restricted environments as it supports no_std targets and performs no heap allocations.

  4. Overview of libjade in libcrux

    main

    libjade is a formally verified cryptographic library used within libcrux. It is written in the Jasmin programming language and features computer-verified proofs in EasyCrypt.

    Each assembly implementation in libjade provides the following security properties:

    • Memory Safety
    • Functional Correctness: Verified against a formal specification in EasyCrypt.
    • Timing Attack Protection
    • Spectre Protection: Specifically against Spectre v1 and Spectre v4.
    • Stack cleanup

    libjade provides reference implementations for x86 platforms and optimized SIMD implementations for AVX2 platforms where available.

  5. Overview of AUCurves in libcrux

    main

    AUCurves is a tool used by libcrux to synthesize formally verified implementations of pairing-friendly elliptic curves. It currently provides verified Rust implementations for the groups G1 and G2 of the BLS12-381 elliptic curve, including the quadratic field extension arithmetic required for G2.

    AUCurves builds upon the Fiat-Crypto and Bedrock2 infrastructures. It uses Fiat-Crypto's base field arithmetic as atomic building blocks and Bedrock2's ExprImp as an intermediate language to prove correctness while abstracting over parameters like prime modulos and system bitwidth.

  6. Overview of AES-based AEADs crate

    main

    This crate provides implementations for AES-GCM (128 and 256) and AES-CCM (128 and 256). It supports multiple execution paths depending on the architecture:

    • Portable: A bit-sliced implementation.
    • x64: An optimized implementation using AES-NI instructions.
    • Aarch64: An optimized implementation using ARM AES instructions.

  7. Overview of HPKE implementation

    main
    This crate provides an implementation of [RFC 9180] (Hybrid Public Key Encryption). It allows for public-key encryption of arbitrary-sized plaintexts for a recipient's public key. The implementation supports various authenticated variants, including those that authenticate possession of a pre-shared key (PSK) or a KEM private key.

  9. Use Elliptic Curve Diffie-Hellman (ECDH) in libcrux

    main

    The libcrux-ecdh crate provides an API for performing Elliptic Curve Diffie-Hellman (ECDH) key exchanges. It currently supports the following curves:

    • Curve25519
    • NIST P256

    The implementation is based on safe Rust compiled from verified C code originating from the HACL* project, ensuring memory safety, functional correctness, and secret independence (resistance to timing side-channels).

  12. Run constant-time tests with ctgrind-test

    main

    The ctgrind-test utility uses Valgrind memcheck to verify constant-time (CT) properties. It works by marking secret data as "undefined" using crabgrind::memcheck::mark_memory, executing a cryptographic operation, and then marking the output as defined. If Valgrind detects that undefined bits influence program behavior (observable differences), it flags a potential timing side channel.

    Available Test Binaries

    BinaryWhat is testedExpected result
    ctgrind-testInsecure vs. secure byte comparison (demo)Insecure comparison flagged
    sha3SHA-256, SHA-512, SHAKE-256 over a secret messageClean
    mlkemML-KEM-512 decapsulate with an undefined private keyClean
    mldsaML-DSA-{44, 65, 87} sign with an undefined signing keyClean

    Note: For libcrux-ml-dsa, Valgrind requests are automatically issued if the crate is compiled with the valgrind_ct_test cfg enabled.