clazel-crypto: libcrux providers for TLS hashing, key schedule, records and X25519 (3.5f, part 1)

README.md

@@ -3,7 +3,7 @@
 A web browser built from the bottom up by AI, using formal verification
 instead of trust.
 
-- **Memory safe:** 100% safe Rust except `clazel-sys`: 14 `unsafe` blocks (20 lines) that enter the OS sandbox, machine-checked and audited.
+- **Memory safe:** 100% safe Rust except `clazel-sys`: 14 `unsafe` blocks (20 lines) that enter the OS sandbox, machine-checked and audited. Shipped dependencies are `libc` and libcrux.
 - **Verified where it matters:** the kernel's security policy and every parser
   of untrusted input carry machine-checked proofs (Verus, Kani).
 - **Honest about it:** each crate declares its verification tier, and the

crates/clazel-crypto/Cargo.toml

@@ -0,0 +1,33 @@
+[package]
+name = "clazel-crypto"
+version = "0.0.0"
+edition.workspace = true
+license.workspace = true
+publish.workspace = true
+description = "The libcrux providers for clazel-tls's cryptographic parameters: SHA-256, HMAC, HKDF, ChaCha20-Poly1305 and X25519."
+
+[dependencies]
+clazel-tls = { path = "../clazel-tls" }
+vstd = "=0.0.0-2026-10-04-0306"
+# Shipped cryptography (docs/DEPENDENCIES.md, class `shipped`; phase-3.md
+# items 3.0 and 3.5f). Pinned exactly: libcrux is pre-release (0.0.x), so
+# every bump is a deliberate re-pin. Every call into these crates is one
+# axiom in src/axioms.rs.
+libcrux-sha2 = { version = "=0.0.9", default-features = false }
+libcrux-hmac = { version = "=0.0.9", default-features = false }
+libcrux-hkdf = { version = "=0.0.9", default-features = false }
+libcrux-chacha20poly1305 = { version = "=0.0.10", default-features = false }
+libcrux-curve25519 = { version = "=0.0.9", default-features = false }
+
+# Verification tier (docs/VERIFICATION.md). The crate parses nothing; its
+# adapters are checked by Verus against clazel-tls's provider contracts, and
+# everything it claims about the cryptography rests on src/axioms.rs.
+[package.metadata.clazel]
+tier = 0
+target-tier = 0
+
+[package.metadata.verus]
+verify = true
+
+[lints]
+workspace = true

crates/clazel-crypto/README.md

@@ -0,0 +1,55 @@
+# clazel-crypto
+
+The libcrux providers for `clazel-tls`'s cryptographic parameters (Phase 3
+item 3.5f).
+
+`clazel-tls` is proven over abstract providers: its key schedule, record
+epochs and key exchange take the cryptography as trait parameters. This crate
+instantiates them with [libcrux](https://github.com/cryspen/libcrux), whose
+crates used here carry the `verified-hacl` badge (safe Rust compiled from
+HACL\* code that is proven memory safe, functionally correct and secret
+independent). Its own code is the adapters, which Verus checks against
+`clazel-tls`'s provider contracts.
+
+| `clazel-tls` parameter | Standard | libcrux call |
+|---|---|---|
+| `schedule::crypto::Crypto::hash` | SHA-256, FIPS 180-4 | `libcrux_sha2::sha256` |
+| `Crypto::hmac` | HMAC-SHA256, RFC 2104 | `libcrux_hmac::hmac_sha2_256` |
+| `Crypto::extract` | HKDF-Extract, RFC 5869 §2.2 | `libcrux_hkdf::sha2_256::extract` |
+| `Crypto::expand` | HKDF-Expand, RFC 5869 §2.3 | `libcrux_hkdf::sha2_256::expand` |
+| `traffic::provider::Factory` and `record::Aead` | ChaCha20-Poly1305, RFC 8439 §2.8 | `libcrux_chacha20poly1305::{encrypt, decrypt}` |
+| `hello::key_exchange::KeyExchange` | X25519, RFC 7748 | `libcrux_curve25519::{secret_to_public, ecdh}` |
+
+## The trust boundary
+
+Every libcrux call is one axiom in `src/axioms.rs`: an `external_body`
+wrapper whose `ensures` says only what libcrux documents. The output is the
+uninterpreted function of `src/spec.rs` applied to exactly these inputs,
+with the documented output length. There is also one proof axiom: the
+ChaCha20-Poly1305 tag is 16 octets. That libcrux computes the standard's
+function is HACL\*'s proof, recorded in docs/VERIFICATION.md's TCB, and is
+never assumed here. A session other than the one that changed
+`src/axioms.rs` reviews each change to it.
+
+Modelling choices:
+- **Oversized inputs abort.** libcrux refuses, or panics on, inputs at or
+  near `u32::MAX` octets, and HACL\*'s preconditions stop just short of it.
+  Each wrapper checks every variable-length input against `MAX_INPUT`
+  (2^32 - 256 octets) first and aborts the process above it, so it never
+  returns a value no axiom covers and never unwinds. No caller in this
+  browser comes near that size.
+- **X25519 refuses an all-zero result.** libcrux's `ecdh` already does this
+  (RFC 7748 §6.1). `clazel-tls` also checks it (RFC 8446 §7.4.2).
+- **The SHA-3 crates are compiled but never called.** `libcrux-hmac` 0.0.9
+  depends on `libcrux-sha3` (pre-verification) for its HMAC-SHA3 types,
+  which brings `libcrux-intrinsics` and `libcrux-platform`, both with
+  `unsafe`. The HMAC-SHA256 path calls only `libcrux-sha2`. The choice was
+  made on 2026-10-26; see docs/DEPENDENCIES.md.
+
+## Not here
+- Signature verification: ECDSA P-256, RSA-PSS and Ed25519 from libcrux, and
+  RSA PKCS#1 v1.5 from `clazel-pkcs1`. These come with certificate path
+  validation (3.5b).
+- Randomness: the caller supplies the X25519 private scalar.
+- Any side-channel claim beyond HACL\*'s. libcrux's README makes none for the
+  extracted Rust, and this crate adds no secret-dependent branches.

crates/clazel-crypto/src/axioms.rs

@@ -0,0 +1,198 @@
+//! The trust boundary: every call into libcrux, each one axiom.
+//!
+//! Each wrapper is `external_body`. Verus takes its `ensures` on trust, and
+//! the body is a direct call to one libcrux function with no logic beyond
+//! length conversion. The `ensures` states only what libcrux documents: the
+//! output is the uninterpreted function of [`crate::spec`] applied to these
+//! exact inputs, with the documented output length. That libcrux computes
+//! the standard's function is HACL*'s proof, recorded in the TCB
+//! (docs/VERIFICATION.md), and is never assumed here.
+//!
+//! The libcrux functions refuse inputs longer than `u32::MAX` octets, and
+//! some panic close to that bound: `libcrux-hkdf`'s expand computes its
+//! buffer length with a wrapping `u32` sum, so an `info` within 33 octets of
+//! `u32::MAX` makes it slice out of range. HACL*'s preconditions also stop
+//! short of `u32::MAX` (for HMAC, data plus the 64-octet block). Every
+//! wrapper therefore checks each variable-length input against
+//! [`MAX_INPUT`] first and calls [`std::process::abort`] instead, so it
+//! never returns a value no axiom covers and never unwinds. Callers in this
+//! browser never come near that size: a TLS record is at most 2^14 + 256
+//! octets, and handshake messages are bounded by the reassembler.
+//!
+//! These axioms are counted in the README table. A session other than the
+//! one that wrote them reviews every change to this file
+//! (docs/phases/phase-3.md 3.5f).
+
+#[allow(unused_imports)]
+use vstd::prelude::*;
+
+verus! {
+
+/// The longest input any wrapper passes to libcrux: 2^32 - 256 octets,
+/// below every HACL* precondition (the tightest is HKDF-Expand's inner
+/// HMAC over 32 + info + 1 octets plus its 64-octet block).
+pub const MAX_INPUT: usize = 0xffff_ff00;
+
+/// SHA-256 of `message`.
+// AXIOM: libcrux-sha2 0.0.9 `sha256(&[u8]) -> [u8; 32]` returns SHA-256 of
+// its input (verified-hacl); it panics above u32::MAX, so we abort above MAX_INPUT.
+#[verifier::external_body]
+pub fn sha256(message: &[u8]) -> (out: Vec<u8>)
+    ensures out@ == crate::spec::sha256(message@), out.len() == 32,
+{
+    if message.len() > MAX_INPUT {
+        std::process::abort();
+    }
+    libcrux_sha2::sha256(message).to_vec()
+}
+
+/// HMAC-SHA256(key, message).
+// AXIOM: libcrux-hmac 0.0.9 `hmac_sha2_256(&mut [u8; 32], key, data)` writes
+// HMAC-SHA256(key, data) (verified-hacl); we abort above MAX_INPUT first.
+#[verifier::external_body]
+pub fn hmac_sha256(key: &[u8], message: &[u8]) -> (out: Vec<u8>)
+    ensures out@ == crate::spec::hmac_sha256(key@, message@), out.len() == 32,
+{
+    if key.len() > MAX_INPUT || message.len() > MAX_INPUT {
+        std::process::abort();
+    }
+    let mut tag = [0u8; 32];
+    libcrux_hmac::hmac_sha2_256(&mut tag, key, message);
+    tag.to_vec()
+}
+
+/// HKDF-Extract(salt, IKM) with SHA-256.
+// AXIOM: libcrux-hkdf 0.0.9 `sha2_256::extract(prk, salt, ikm)` writes the
+// 32-octet HKDF-Extract PRK; errs only above u32::MAX; we abort above MAX_INPUT.
+#[verifier::external_body]
+pub fn hkdf_extract(salt: &[u8], ikm: &[u8]) -> (out: Vec<u8>)
+    ensures out@ == crate::spec::hkdf_extract(salt@, ikm@), out.len() == 32,
+{
+    if salt.len() > MAX_INPUT || ikm.len() > MAX_INPUT {
+        std::process::abort();
+    }
+    let mut prk = [0u8; 32];
+    match libcrux_hkdf::sha2_256::extract(&mut prk, salt, ikm) {
+        Ok(()) => prk.to_vec(),
+        Err(_) => std::process::abort(),
+    }
+}
+
+/// HKDF-Expand(PRK, info, length) with SHA-256.
+// AXIOM: libcrux-hkdf 0.0.9 `sha2_256::expand(okm, prk, info)` fills okm with
+// HKDF-Expand(prk[..32], info, okm.len()); panics near u32::MAX info: abort above MAX_INPUT.
+#[verifier::external_body]
+pub fn hkdf_expand(prk: &[u8], info: &[u8], length: u16) -> (out: Vec<u8>)
+    requires prk.len() == 32, length <= 8160,
+    ensures out@ == crate::spec::hkdf_expand(prk@, info@, length as nat), out.len() == length,
+{
+    // libcrux uses only prk's first 32 octets; `requires` makes that all of it.
+    if info.len() > MAX_INPUT {
+        std::process::abort();
+    }
+    let mut okm = vec![0u8; usize::from(length)];
+    match libcrux_hkdf::sha2_256::expand(&mut okm, prk, info) {
+        Ok(()) => okm,
+        Err(_) => std::process::abort(),
+    }
+}
+
+/// ChaCha20-Poly1305 encryption: ciphertext then the 16-octet tag.
+// AXIOM: libcrux-chacha20poly1305 0.0.10 `encrypt(key, ptxt, ctxt, aad, nonce)`
+// writes ciphertext then 16-octet tag into ctxt; errs only above u32::MAX (we: MAX_INPUT).
+#[verifier::external_body]
+pub fn chacha20poly1305_seal(key: &[u8], nonce: &[u8], ad: &[u8], plaintext: &[u8])
+    -> (out: Vec<u8>)
+    requires key.len() == 32, nonce.len() == 12,
+    ensures out@ == crate::spec::chacha20poly1305_seal(key@, nonce@, ad@, plaintext@),
+{
+    let (Ok(key), Ok(nonce)) = (<&[u8; 32]>::try_from(key), <&[u8; 12]>::try_from(nonce)) else {
+        std::process::abort();
+    };
+    if ad.len() > MAX_INPUT || plaintext.len() > MAX_INPUT {
+        std::process::abort();
+    }
+    let Some(length) = plaintext.len().checked_add(libcrux_chacha20poly1305::TAG_LEN) else {
+        std::process::abort();
+    };
+    let mut out = vec![0u8; length];
+    match libcrux_chacha20poly1305::encrypt(key, plaintext, &mut out, ad, nonce) {
+        Ok(_) => out,
+        Err(_) => std::process::abort(),
+    }
+}
+
+/// ChaCha20-Poly1305 decryption, or none when the tag does not verify.
+// AXIOM: libcrux-chacha20poly1305 0.0.10 `decrypt(key, ptxt, ctxt, aad, nonce)`
+// returns the plaintext iff the tag verifies, else Err (also for ctxt < 16 octets).
+#[verifier::external_body]
+pub fn chacha20poly1305_open(key: &[u8], nonce: &[u8], ad: &[u8], ciphertext: &[u8])
+    -> (out: Option<Vec<u8>>)
+    requires key.len() == 32, nonce.len() == 12,
+    ensures match out {
+        Some(p) => crate::spec::chacha20poly1305_open(key@, nonce@, ad@, ciphertext@) == Some(p@),
+        None => crate::spec::chacha20poly1305_open(key@, nonce@, ad@, ciphertext@) is None,
+    },
+{
+    let (Ok(key), Ok(nonce)) = (<&[u8; 32]>::try_from(key), <&[u8; 12]>::try_from(nonce)) else {
+        std::process::abort();
+    };
+    if ad.len() > MAX_INPUT || ciphertext.len() > MAX_INPUT {
+        std::process::abort();
+    }
+    let mut plaintext = vec![0u8; ciphertext.len().saturating_sub(libcrux_chacha20poly1305::TAG_LEN)];
+    match libcrux_chacha20poly1305::decrypt(key, &mut plaintext, ciphertext, ad, nonce) {
+        Ok(_) => Some(plaintext),
+        Err(_) => None,
+    }
+}
+
+/// The sealed output is exactly 16 octets longer than the plaintext.
+// AXIOM: libcrux-chacha20poly1305 0.0.10 appends exactly TAG_LEN = 16 octets
+// (RFC 8439 §2.8); `encrypt`'s output split is (ptxt.len(), 16).
+#[verifier::external_body]
+pub proof fn axiom_chacha20poly1305_seal_len(key: Seq<u8>, nonce: Seq<u8>, ad: Seq<u8>,
+    plaintext: Seq<u8>)
+    ensures crate::spec::chacha20poly1305_seal(key, nonce, ad, plaintext).len() == plaintext.len() + 16,
+{
+}
+
+/// X25519(private_key, 9).
+// AXIOM: libcrux-curve25519 0.0.9 `secret_to_public(pk, sk)` writes
+// X25519(sk, 9) (verified-hacl); both are 32-octet arrays.
+#[verifier::external_body]
+pub fn x25519_public(private_key: &[u8]) -> (out: Vec<u8>)
+    requires private_key.len() == 32,
+    ensures out@ == crate::spec::x25519_public(private_key@), out.len() == 32,
+{
+    let Ok(private_key) = <&[u8; 32]>::try_from(private_key) else {
+        std::process::abort();
+    };
+    let mut public = [0u8; 32];
+    libcrux_curve25519::secret_to_public(&mut public, private_key);
+    public.to_vec()
+}
+
+/// X25519(private_key, peer_key), or none for an all-zero result.
+// AXIOM: libcrux-curve25519 0.0.9 `ecdh(out, pk, sk)` writes X25519(sk, pk)
+// and returns Err exactly when HACL reports failure (an all-zero result).
+#[verifier::external_body]
+pub fn x25519_shared(private_key: &[u8], peer_key: &[u8]) -> (out: Option<Vec<u8>>)
+    requires private_key.len() == 32, peer_key.len() == 32,
+    ensures match out {
+        Some(s) => s.len() == 32 && crate::spec::x25519_shared(private_key@, peer_key@) == Some(s@),
+        None => crate::spec::x25519_shared(private_key@, peer_key@) is None,
+    },
+{
+    let (Ok(private_key), Ok(peer_key)) =
+        (<&[u8; 32]>::try_from(private_key), <&[u8; 32]>::try_from(peer_key)) else {
+        std::process::abort();
+    };
+    let mut shared = [0u8; 32];
+    match libcrux_curve25519::ecdh(&mut shared, peer_key, private_key) {
+        Ok(()) => Some(shared.to_vec()),
+        Err(_) => None,
+    }
+}
+
+} // verus!

crates/clazel-crypto/src/compare.rs

@@ -0,0 +1,89 @@
+//! Timing-safe comparison of secret byte strings (RFC 8446 §4.4.4, the
+//! Finished `verify_data` check; docs/phases/phase-3.md item 3.0).
+//!
+//! Modelling choices:
+//! - **Verus proves the result, not the timing.** The contract says only
+//!   that [`constant_time_eq`] returns `a@ == b@`. Timing independence rests
+//!   on the shape of the code: one pass over every index, an OR-accumulator
+//!   of byte XORs, no early exit, no `break`, no branch on the data inside
+//!   the loop, and no data-dependent indexing. The only branch on secret
+//!   data is the final `acc == 0`, which is the standard construction.
+//! - **The compiler is trusted not to undo that shape.** LLVM could in
+//!   principle turn the accumulator into an early exit. We do not use
+//!   `core::hint::black_box`, because its guarantee is best effort only, so
+//!   this module claims no more than the shape above. It makes no claim
+//!   about caches, speculation or the hardware.
+//! - **Lengths are public.** The contract requires equal lengths; callers
+//!   compare fixed-size values (32 octets for SHA-256 Finished), so the
+//!   length never depends on a secret.
+#[allow(unused_imports)]
+use vstd::prelude::*;
+
+verus! {
+
+/// The byte at `i`, or 0 past the end. Callers keep `i < s.len()`, so the
+/// fallback is unreachable; it depends on the index, never on the data.
+fn byte_at(s: &[u8], i: usize) -> (out: u8)
+    requires
+        i < s.len(),
+    ensures
+        out == s@[i as int],
+{
+    match s.get(i) {
+        Some(&v) => v,
+        None => 0,
+    }
+}
+
+/// Bitwise facts about `u8`: XOR is zero exactly on equal bytes, and an OR is
+/// zero exactly when both sides are.
+proof fn lemma_xor_zero(x: u8, y: u8)
+    ensures
+        (x ^ y) == 0 <==> x == y,
+{
+    assert((x ^ y) == 0 <==> x == y) by (bit_vector);
+}
+
+proof fn lemma_or_zero(p: u8, q: u8)
+    ensures
+        (p | q) == 0 <==> (p == 0 && q == 0),
+{
+    assert((p | q) == 0 <==> (p == 0 && q == 0)) by (bit_vector);
+}
+
+/// RFC 8446 §4.4.4: compare two Finished verify_data values without a
+/// data-dependent branch or early exit.
+pub fn constant_time_eq(a: &[u8], b: &[u8]) -> (out: bool)
+    requires
+        a.len() == b.len(),
+    ensures
+        out == (a@ == b@),
+{
+    let mut acc: u8 = 0;
+    let mut i: usize = 0;
+    while i < a.len()
+        invariant
+            i <= a@.len(),
+            a@.len() == b@.len(),
+            (acc == 0) <==> (forall|k: int| 0 <= k < i ==> a@[k] == b@[k]),
+        decreases a@.len() - i,
+    {
+        let x = byte_at(a, i);
+        let y = byte_at(b, i);
+        proof {
+            lemma_xor_zero(x, y);
+            lemma_or_zero(acc, x ^ y);
+        }
+        acc |= x ^ y;
+        // i < len, so this does not saturate.
+        i = i.saturating_add(1);
+    }
+    proof {
+        if acc == 0 {
+            assert(a@ =~= b@);
+        }
+    }
+    acc == 0
+}
+
+} // verus!