From bb12849346de9c7bfe69d7a161134cf8771445d0 Mon Sep 17 00:00:00 2001 From: Mike Lodder Date: Tue, 8 Sep 2026 13:33:02 -0600 Subject: [PATCH] ml-kem: add Kani proof harnesses and CI verification Add harnesses for field arithmetic, compression, encoding, and NTT primitives. Run Kani in CI with cached tooling and a 30-minute timeout. Document proof scope, assumptions, ABI coverage, and runtime impact. --- .github/workflows/ml-kem.yml | 45 ++++++++ Cargo.toml | 1 + ml-kem/README.md | 14 +++ ml-kem/VERIFICATION.md | 187 ++++++++++++++++++++++++++++++++++ ml-kem/src/algebra.rs | 24 +++-- ml-kem/src/algebra/proofs.rs | 171 +++++++++++++++++++++++++++++++ ml-kem/src/compress.rs | 3 + ml-kem/src/compress/proofs.rs | 56 ++++++++++ ml-kem/src/lib.rs | 3 + ml-kem/src/proofs.rs | 74 ++++++++++++++ 10 files changed, 572 insertions(+), 6 deletions(-) create mode 100644 ml-kem/VERIFICATION.md create mode 100644 ml-kem/src/algebra/proofs.rs create mode 100644 ml-kem/src/compress/proofs.rs create mode 100644 ml-kem/src/proofs.rs diff --git a/.github/workflows/ml-kem.yml b/.github/workflows/ml-kem.yml index 7a10d72b..f872b868 100644 --- a/.github/workflows/ml-kem.yml +++ b/.github/workflows/ml-kem.yml @@ -79,6 +79,51 @@ jobs: - run: cargo test - run: cargo test --all-features + kani: + name: Primitive proofs (Kani) + runs-on: ubuntu-24.04 + timeout-minutes: 30 + env: + KANI_VERSION: "0.67.0" + # Must match rust-toolchain-version in the pinned Kani release bundle. + KANI_TOOLCHAIN: nightly-2025-11-21-x86_64-unknown-linux-gnu + permissions: + contents: read + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - uses: cargo-bins/cargo-binstall@v1.23.0 + with: + version: "1.23.0" + - name: Install prebuilt Kani launcher + # QuickInstall provides the launcher; setup obtains the official Kani bundle. + # Fail if binaries are unavailable instead of falling back to compilation. + run: cargo binstall --no-confirm --disable-strategies compile --version "$KANI_VERSION" kani-verifier + - name: Cache Kani bundle and Rust toolchain + id: kani-cache + uses: actions/cache/restore@v4 + with: + key: kani-ubuntu-24.04-${{ runner.arch }}-${{ env.KANI_VERSION }}-${{ env.KANI_TOOLCHAIN }}-v1 + path: | + ~/.kani/kani-${{ env.KANI_VERSION }} + ~/.rustup/toolchains/${{ env.KANI_TOOLCHAIN }} + - name: Set up Kani + if: steps.kani-cache.outputs.cache-hit != 'true' + run: cargo kani setup + - name: Check Kani installation + run: cargo kani --version + - name: Save Kani installation + # Keep a successful setup even if a subsequent proof fails. + if: steps.kani-cache.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + key: ${{ steps.kani-cache.outputs.cache-primary-key }} + path: | + ~/.kani/kani-${{ env.KANI_VERSION }} + ~/.rustup/toolchains/${{ env.KANI_TOOLCHAIN }} + - name: Verify ML-KEM primitives + run: cargo kani --lib --no-default-features --jobs 2 --output-format terse + cross: needs: set-msrv strategy: diff --git a/Cargo.toml b/Cargo.toml index 6a65b1e7..95407e8c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -44,6 +44,7 @@ unwrap_in_result = "warn" unwrap_used = "warn" [workspace.lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } missing_copy_implementations = "warn" missing_debug_implementations = "warn" missing_docs = "warn" diff --git a/ml-kem/README.md b/ml-kem/README.md index 730bc6cc..4d4968bb 100644 --- a/ml-kem/README.md +++ b/ml-kem/README.md @@ -47,6 +47,20 @@ The implementation contained in this crate has never been independently audited! USE AT YOUR OWN RISK! +This crate includes Kani proof harnesses for arithmetic and encoding primitives +as an initial step toward formal verification of the complete Rust implementation. +Their input assumptions and scope are documented in [VERIFICATION.md](VERIFICATION.md). +Correctness and constant-time execution are design goals that guide the +implementation and its ongoing development. Testing and incremental formal +verification strengthen confidence in the implementation, but do not yet +establish full KEM correctness or guarantee constant-time execution. + +Kani is needed only to run the development/CI proofs. Applications using this +library do not need Kani; normal debug and release builds exclude the proof +harnesses and incur no runtime overhead from them. The proofs check a model of +the Rust implementation, not the optimized release binary. See +[Library use and release builds](VERIFICATION.md#library-use-and-release-builds). + ## Minimum Supported Rust Version (MSRV) Policy MSRV increases are not considered breaking changes and can happen in patch diff --git a/ml-kem/VERIFICATION.md b/ml-kem/VERIFICATION.md new file mode 100644 index 00000000..1ccd9155 --- /dev/null +++ b/ml-kem/VERIFICATION.md @@ -0,0 +1,187 @@ +# Primitive verification + +The Kani harnesses in this crate check the production ML-KEM arithmetic and +its use of `module-lattice`. They are compile only and add no runtime dependency +or public API. + +## Library use and release builds + +Kani is a development and CI tool. Applications that depend on `ml-kem` do not +need to install, run, or link Kani. Normal debug and release builds exclude the +proof harnesses through `#[cfg(kani)]`, so those harnesses add no runtime checks, +binary size, or execution overhead. Build and use the library normally, including +with `cargo build --release`. + +The CI proof job runs a separate Kani verification build. It checks a model of +the production Rust implementation against the assertions in each harness, +using symbolic inputs. A successful proof covers all inputs admitted by the +harness's assumptions and checked loop bounds, rather than a sample of test +cases. + +This is not verification of the optimized release binary. The proofs rely on +the compiler preserving the verified behavior and do not establish that release +machine code executes in constant time. See [Scope and assumptions](#scope-and-assumptions) +for the remaining limits of these primitive proofs. + +## Running the proofs + +Install the pinned verifier (requires Rust installed through rustup): + +```sh +cargo install --locked kani-verifier --version 0.67.0 +cargo kani setup +``` + +If `cargo-binstall` is already installed, the launcher can be installed without +compilation instead: + +```sh +cargo binstall --no-confirm --disable-strategies compile --version 0.67.0 kani-verifier +cargo kani setup +``` + +This uses a prebuilt launcher (available from cargo-bins/QuickInstall). Kani's +setup command separately downloads the official compiler/solver bundle and +installs its required Rust toolchain. The binary-only command fails if no +compatible launcher is available; the `cargo install` command above remains +the source-build alternative. + +From the workspace root, run: + +```sh +cargo kani -p ml-kem --lib --no-default-features +``` + +Individual harnesses can be selected with `--harness`, for example: + +```sh +cargo kani -p ml-kem --lib --no-default-features --harness algebra::proofs::small_reduce +``` + +The `kani` job in `.github/workflows/ml-kem.yml` installs the same pinned +version and runs every harness, with two concurrent solver processes. It runs +on pull requests affecting this crate, `module-lattice`, the workspace manifests, +or that workflow, and on pushes to `master`. Proof failures fail the job; its +30-minute timeout also fails rather than treating unfinished proofs as passed. + +CI uses `cargo-binstall` for the launcher and caches both the Kani bundle and +its required nightly Rust toolchain. Setup runs only on an exact cache miss. +The installation is saved before proof execution, so a failing proof does not +force the next CI run to download the toolchain again. +The cache key includes the Ubuntu release, architecture, Kani version, and +toolchain version. When upgrading Kani, update `KANI_TOOLCHAIN` to match the +new bundle's `rust-toolchain-version` as well. Proofs always rerun; proof results +are not cached or skipped. Installation caching does not reduce solver time. + +Keep Kani's default safety checks and unwinding assertions enabled. A timeout, +unsupported operation, or failed unwinding assertion is not a successful proof. +The encoding harnesses specify an unwind bound of 513 to accommodate fixed-size +array initialization (at most 384 bytes) and loops over 256 coefficients. + +## Target and ABI coverage + +The CI Kani job is configured for `x86_64-unknown-linux-gnu` on Ubuntu 24.04, +with 64-bit pointers and `usize`, little-endian byte order, and +`--no-default-features`. A successful run establishes the harness properties +for that modeled target and feature configuration. It is not a proof for every +architecture, operating system, or ABI, nor a validation of machine-level +calling conventions or FFI boundaries. + +The verified primitives use fixed-width coefficient arithmetic and explicit +little-endian serialization. These choices support portability, but do not +automatically extend the proofs to 32-bit targets, big-endian targets, or other +environments such as Windows/MSVC, Linux/musl, or Apple platforms. Pointer width, +`usize` arithmetic, type layout, target-specific dependencies, and conditional +compilation can change the modeled program. An ARM64 run would add coverage for +that target, but would not by itself cover 32-bit or big-endian behavior. + +The existing `powerpc-unknown-linux-gnu` release tests provide complementary +32-bit, big-endian coverage. The `thumbv7em-none-eabi` and +`wasm32-unknown-unknown` jobs check that the crate builds for those targets. +These tests and build checks are not Kani proofs for those targets. + +One ABI is sufficient for the current CI verification baseline because the +properties under examination concern shared Rust arithmetic and encoding +primitives: fixed-width integer calculations, coefficient bounds, bit packing, +and bounded array indices. These primitives do not select different arithmetic +implementations by OS or ABI, call foreign functions, or depend on a particular +struct layout. Their specifications describe values and indices rather than +register assignments or calling conventions. Repeating the suite on another +64-bit, little-endian ABI would therefore largely repeat the same checks while +increasing CI cost. + +This is a scope and coverage decision, not a claim that a proof on one ABI +formally establishes correctness on every other ABI. The target-dependent +limits above remain, with cross-platform tests providing additional empirical +coverage. + +Revisit formal coverage when +adding target-specific implementations, SIMD, assembly, unsafe code, FFI, or +features that change code reached by the harnesses. Constant-time assurance +requires separate checks of compiled binaries for the relevant architectures +and compiler configurations; expanding the Kani matrix alone does not provide +that assurance. + +## Properties and input domains + +The modulus in the specifications is independently fixed to FIPS 203's `q = 3329`. +The harnesses call the actual `BaseField` implementation generated by +`module_lattice::define_field!`; they do not substitute a copy of its arithmetic. +Reference formulas use wider integers and ordinary division/remainder, which +are acceptable in proof specifications even when inappropriate for production +secret-dependent computation. + +| Harnesses | Input domain | Properties | +| --- | --- | --- | +| `algebra::proofs::small_reduce` | `0 <= x < 2q` | Result is `x mod q` and below `q` | +| `algebra::proofs::barrett_reduce` | `0 <= x <= 2(q-1)^2` | Result is `x mod q` and below `q` | +| `algebra::proofs::{add,subtract,negate,multiply}` | Each coefficient is below `q` | Exact field operation and canonical result | +| `algebra::proofs::{forward_butterfly,inverse_butterfly}` | Coefficients and twiddle below `q` | Both scalar outputs match the butterfly equations and are canonical | +| `algebra::proofs::{layer_*,inverse_layer_*}` | 256 independent coefficients below `q`; each of the seven production layer sizes and starting twiddle indices | Array/table accesses and arithmetic are safe, outputs are canonical, and twiddle index advances as expected | +| `algebra::proofs::base_case` | Four coefficients below `q`; `0 <= i < 128` | Multiplication modulo `X^2 - GAMMA[i]` and canonical outputs | +| `compress::proofs::compress_*` | `0 <= x < q` | FIPS 203 compression formula and `d`-bit output | +| `compress::proofs::decompress_*` | `0 <= x < 2^d` | FIPS 203 decompression formula and canonical output | +| `proofs::encode_*` | Each coefficient below `2^d`, or below `q` for `d=12` | Every output bit matches little-endian coefficient packing | +| `proofs::decode_*` | Arbitrary bytes of the required length | Every output coefficient matches bit unpacking, reduced modulo `q` for `d=12` | + +Compression and encoding cover widths 1, 4, 5, 6, 10, 11, and 12. Compression +at widths 6 and 12 is extra primitive coverage matching the existing tests; +the KEM uses compression widths 1, 4, 5, 10, and 11. Encoding at width 6 also +covers CBD sampling input. These primitives are shared by all three ML-KEM +parameter sets. + +Encoding inputs contain independently symbolic elements. The output bit or +coefficient selected for comparison is also symbolic, so a successful proof +establishes the specified property at every position, not just one fixed index. +The full production encoding/decoding loops still execute under verification. + +## Scope and assumptions + +These are proofs of isolated primitives under explicit preconditions, not a +proof of the complete KEM. In particular, `Elem::new` does not enforce a range; +establishing that every caller satisfies these preconditions is separate work. +The Barrett input range covers products of canonical coefficients and the sums +of two products used in `base_case_multiply`. It is not a claim about arbitrary +`u32` inputs or other instantiations of the field macro, such as ML-DSA. + +The butterfly proofs cover scalar arithmetic; layer proofs cover bounds and +index safety. They do not establish twiddle ordering, inverse scaling, or +correctness of the complete transform. Base-case +multiplication is specified relative to the existing `GAMMA` table; these proofs +do not independently establish that the table matches FIPS 203. + +Also outside this scope: sampling, key validation, PKE/KEM composition, implicit +rejection, SHA3/SHAKE, secret erasure, allocation failure, and constant-time +execution. In particular, the CBD lookup in `sample_poly_cbd` is unchanged. + +Kani checks the reachable Rust operations for panics, arithmetic overflow, and +the memory-safety properties supported by its model. Intentional truncation +and wrapping operations are allowed by Rust; the functional assertions check +their consequences within the stated domains. The proofs use no function +stubs and do not disable safety checks. + +Assurance depends on Kani's Rust model and translation, CBMC and its solver, +the specifications and assumptions in each harness, and the compiler and +hardware used to run the resulting library. Source-level proofs do not prove +properties of emitted machine code. Existing unit, ACVP, and Wycheproof tests +remain complementary checks. diff --git a/ml-kem/src/algebra.rs b/ml-kem/src/algebra.rs index 4d5f8bbe..79b65c40 100644 --- a/ml-kem/src/algebra.rs +++ b/ml-kem/src/algebra.rs @@ -7,6 +7,9 @@ use array::{Array, ArraySize, typenum::U256}; use module_lattice::{Encode, Field, MultiplyNtt, Truncate}; use sha3::digest::XofReader; +#[cfg(kani)] +mod proofs; + module_lattice::define_field!(BaseField, u16, u32, u64, 3329); pub(crate) type Int = ::Int; @@ -135,6 +138,19 @@ pub(crate) trait Ntt { fn ntt(&self) -> Self::Output; } +/// Forward butterfly over canonical field elements. +#[inline(always)] +fn ntt_butterfly(a: Elem, b: Elem, zeta: Elem) -> (Elem, Elem) { + let t = zeta * b; + (a + t, a - t) +} + +/// Inverse butterfly over canonical field elements, before final scaling. +#[inline(always)] +fn ntt_inverse_butterfly(a: Elem, b: Elem, zeta: Elem) -> (Elem, Elem) { + (a + b, zeta * (b - a)) +} + /// One layer of the forward NTT butterfly. /// /// `LEN` is the butterfly half-length and `ITERATIONS = 128 / LEN` is the number of @@ -149,9 +165,7 @@ fn ntt_layer(f: &mut Array( *k -= 1; for j in start..(start + LEN) { - let t = f[j]; - f[j] = t + f[j + LEN]; - f[j + LEN] = zeta * (f[j + LEN] - t); + (f[j], f[j + LEN]) = ntt_inverse_butterfly(f[j], f[j + LEN], zeta); } } } diff --git a/ml-kem/src/algebra/proofs.rs b/ml-kem/src/algebra/proofs.rs new file mode 100644 index 00000000..6cff5cbf --- /dev/null +++ b/ml-kem/src/algebra/proofs.rs @@ -0,0 +1,171 @@ +//! Proofs of the production arithmetic instantiated with the ML-KEM field. +//! +//! Preconditions apply to each primitive in isolation. These harnesses do not +//! establish that all higher-level callers satisfy those preconditions. + +#![allow( + clippy::integer_division_remainder_used, + reason = "mathematical specifications" +)] + +use super::{ + BaseField, Elem, Field, GAMMA, base_case_multiply, ntt_butterfly, ntt_inverse_butterfly, + ntt_inverse_layer, ntt_layer, +}; +use array::{Array, typenum::U256}; + +const Q: u32 = 3329; + +fn coefficient() -> Elem { + let x: u16 = kani::any(); + kani::assume(u32::from(x) < Q); + Elem::new(x) +} + +#[kani::proof] +fn small_reduce() { + let x: u16 = kani::any(); + kani::assume(u32::from(x) < 2 * Q); + let r = BaseField::small_reduce(x); + assert!(u32::from(r) < Q); + assert_eq!(u32::from(r), u32::from(x) % Q); +} + +#[kani::proof] +fn barrett_reduce() { + let x: u32 = kani::any(); + // Covers a product and the sum of two products in BaseCaseMultiply. + kani::assume(x <= 2 * (Q - 1) * (Q - 1)); + let r = BaseField::barrett_reduce(x); + assert!(u32::from(r) < Q); + assert_eq!(u32::from(r), x % Q); +} + +#[kani::proof] +fn add() { + let a = coefficient(); + let b = coefficient(); + let r = a + b; + assert!(u32::from(r.0) < Q); + assert_eq!(u32::from(r.0), (u32::from(a.0) + u32::from(b.0)) % Q); +} + +#[kani::proof] +fn subtract() { + let a = coefficient(); + let b = coefficient(); + let r = a - b; + assert!(u32::from(r.0) < Q); + assert_eq!(u32::from(r.0), (u32::from(a.0) + Q - u32::from(b.0)) % Q); +} + +#[kani::proof] +fn negate() { + let a = coefficient(); + let r = -a; + assert!(u32::from(r.0) < Q); + assert_eq!(u32::from(r.0), (Q - u32::from(a.0)) % Q); +} + +#[kani::proof] +fn multiply() { + let a = coefficient(); + let b = coefficient(); + let r = a * b; + assert!(u32::from(r.0) < Q); + assert_eq!(u32::from(r.0), (u32::from(a.0) * u32::from(b.0)) % Q); +} + +#[kani::proof] +fn forward_butterfly() { + let a = coefficient(); + let b = coefficient(); + let zeta = coefficient(); + let (c0, c1) = ntt_butterfly(a, b, zeta); + let t = u32::from(zeta.0) * u32::from(b.0) % Q; + assert!(u32::from(c0.0) < Q); + assert!(u32::from(c1.0) < Q); + assert_eq!(u32::from(c0.0), (u32::from(a.0) + t) % Q); + assert_eq!(u32::from(c1.0), (u32::from(a.0) + Q - t) % Q); +} + +#[kani::proof] +fn inverse_butterfly() { + let a = coefficient(); + let b = coefficient(); + let zeta = coefficient(); + let (c0, c1) = ntt_inverse_butterfly(a, b, zeta); + assert!(u32::from(c0.0) < Q); + assert!(u32::from(c1.0) < Q); + assert_eq!(u32::from(c0.0), (u32::from(a.0) + u32::from(b.0)) % Q); + assert_eq!( + u32::from(c1.0), + u32::from(zeta.0) * (u32::from(b.0) + Q - u32::from(a.0)) % Q + ); +} + +#[kani::proof] +fn base_case() { + let a0 = coefficient(); + let a1 = coefficient(); + let b0 = coefficient(); + let b1 = coefficient(); + let i: usize = kani::any(); + kani::assume(i < 128); + let (c0, c1) = base_case_multiply(a0, a1, b0, b1, i); + // Independent polynomial multiplication modulo X^2 - GAMMA[i]. + // Widen before multiplying: the unreduced triple product exceeds u32. + let q = u64::from(Q); + let expected0 = (u64::from(a0.0) * u64::from(b0.0) + + u64::from(a1.0) * u64::from(b1.0) * u64::from(GAMMA[i].0)) + % q; + let expected1 = (u64::from(a0.0) * u64::from(b1.0) + u64::from(a1.0) * u64::from(b0.0)) % q; + assert!(u32::from(c0.0) < Q); + assert!(u32::from(c1.0) < Q); + assert_eq!(u64::from(c0.0), expected0); + assert_eq!(u64::from(c1.0), expected1); +} + +fn layer() { + let mut f: Array = Array::from_fn(|_| coefficient()); + // The forward transform starts this layer at twiddle 128 / LEN. + let mut k = ITERATIONS; + ntt_layer::(&mut f, &mut k); + assert_eq!(k, 2 * ITERATIONS); + let index: usize = kani::any(); + kani::assume(index < 256); + assert!(u32::from(f[index].0) < Q); +} + +fn inverse_layer() { + let mut f: Array = Array::from_fn(|_| coefficient()); + // The inverse transform traverses the twiddles in reverse order. + let mut k = 2 * ITERATIONS - 1; + ntt_inverse_layer::(&mut f, &mut k); + assert_eq!(k, ITERATIONS - 1); + let index: usize = kani::any(); + kani::assume(index < 256); + assert!(u32::from(f[index].0) < Q); +} + +macro_rules! layers { + ($($forward:ident, $inverse:ident: $len:literal, $iterations:literal);+ $(;)?) => {$ ( + #[kani::proof] + #[kani::unwind(257)] + fn $forward() { layer::<$len, $iterations>(); } + + #[kani::proof] + #[kani::unwind(257)] + fn $inverse() { inverse_layer::<$len, $iterations>(); } + )+}; +} + +layers! { + layer_128, inverse_layer_128: 128, 1; + layer_64, inverse_layer_64: 64, 2; + layer_32, inverse_layer_32: 32, 4; + layer_16, inverse_layer_16: 16, 8; + layer_8, inverse_layer_8: 8, 16; + layer_4, inverse_layer_4: 4, 32; + layer_2, inverse_layer_2: 2, 64; +} diff --git a/ml-kem/src/compress.rs b/ml-kem/src/compress.rs index 7a70299d..17e7229a 100644 --- a/ml-kem/src/compress.rs +++ b/ml-kem/src/compress.rs @@ -3,6 +3,9 @@ use array::ArraySize; use module_lattice::EncodingSize; use module_lattice::{Field, Truncate}; +#[cfg(kani)] +mod proofs; + // A convenience trait to allow us to associate some constants with a typenum pub(crate) trait CompressionFactor: EncodingSize { const POW2_HALF: u32; diff --git a/ml-kem/src/compress/proofs.rs b/ml-kem/src/compress/proofs.rs new file mode 100644 index 00000000..8e12eee5 --- /dev/null +++ b/ml-kem/src/compress/proofs.rs @@ -0,0 +1,56 @@ +//! Scalar FIPS 203 compression and decompression, with symbolic inputs. + +#![allow( + clippy::integer_division_remainder_used, + reason = "mathematical specifications" +)] + +use super::{Compress, CompressionFactor, Elem}; +use array::typenum::{U1, U4, U5, U6, U10, U11, U12}; + +const Q: u32 = 3329; + +fn compression() { + let x: u16 = kani::any(); + kani::assume(u32::from(x) < Q); + let mut actual = Elem::new(x); + actual.compress::(); + let scale = 1u32 << D::USIZE; + // Integer division implements nearest rounding, with ties rounded up. + let expected = ((u32::from(x) * scale + Q / 2) / Q) % scale; + assert!(u32::from(actual.0) < scale); + assert_eq!(u32::from(actual.0), expected); +} + +fn decompression() { + let x: u16 = kani::any(); + let scale = 1u32 << D::USIZE; + kani::assume(u32::from(x) < scale); + let mut actual = Elem::new(x); + actual.decompress::(); + let expected = (u32::from(x) * Q + scale / 2) / scale; + assert!(u32::from(actual.0) < Q); + assert_eq!(u32::from(actual.0), expected); +} + +macro_rules! proofs { + ($($compress:ident, $decompress:ident: $d:ty);+ $(;)?) => {$ ( + #[kani::proof] + fn $compress() { compression::<$d>(); } + + #[kani::proof] + fn $decompress() { decompression::<$d>(); } + )+}; +} + +// All widths exercised by the existing scalar compression tests. The KEM +// itself uses 1, 4, 5, 10, and 11; 6 and 12 are additional primitive coverage. +proofs! { + compress_1, decompress_1: U1; + compress_4, decompress_4: U4; + compress_5, decompress_5: U5; + compress_6, decompress_6: U6; + compress_10, decompress_10: U10; + compress_11, decompress_11: U11; + compress_12, decompress_12: U12; +} diff --git a/ml-kem/src/lib.rs b/ml-kem/src/lib.rs index 4c7cf7aa..6f811d41 100644 --- a/ml-kem/src/lib.rs +++ b/ml-kem/src/lib.rs @@ -65,6 +65,9 @@ mod pke; /// Section 7. Parameter Sets mod param; +#[cfg(kani)] +mod proofs; + // PKCS#8 key encoding support (doc comments in module) pub mod pkcs8; diff --git a/ml-kem/src/proofs.rs b/ml-kem/src/proofs.rs new file mode 100644 index 00000000..e5942e15 --- /dev/null +++ b/ml-kem/src/proofs.rs @@ -0,0 +1,74 @@ +//! Bit-level specifications for ML-KEM's use of module-lattice encoding. + +#![allow( + clippy::integer_division_remainder_used, + reason = "mathematical specifications" +)] + +use crate::algebra::{BaseField, Elem}; +use array::{ + Array, + typenum::{U1, U4, U5, U6, U10, U11, U12}, +}; +use module_lattice::{EncodedPolynomial, EncodingSize, byte_decode, byte_encode}; + +fn encode() { + let input = Array::from_fn(|_| { + let x: u16 = kani::any(); + // ByteEncode_12 accepts canonical field elements; smaller widths + // encode compressed coefficients or CBD sampling values. + let limit = if D::USIZE == 12 { + 3329 + } else { + 1u16 << D::USIZE + }; + kani::assume(x < limit); + Elem::new(x) + }); + let bytes = byte_encode::(&input); + // One arbitrary output bit establishes the bit ordering for every bit. + let bit: usize = kani::any(); + kani::assume(bit < 256 * D::USIZE); + let expected = (input[bit / D::USIZE].0 >> (bit % D::USIZE)) & 1; + assert_eq!(u16::from((bytes[bit / 8] >> (bit % 8)) & 1), expected); +} + +fn decode() { + let bytes: EncodedPolynomial = Array::from_fn(|_| kani::any()); + let vals = byte_decode::(&bytes); + let index: usize = kani::any(); + kani::assume(index < 256); + let mut expected = 0u16; + for j in 0..D::USIZE { + let bit = index * D::USIZE + j; + expected |= u16::from((bytes[bit / 8] >> (bit % 8)) & 1) << j; + } + if D::USIZE == 12 { + // Arbitrary byte strings include noncanonical values 3329..4095. + // ByteDecode reduces these; public-key validation is a separate step. + expected %= 3329; + } + assert_eq!(vals[index].0, expected); +} + +macro_rules! proofs { + ($($encode:ident, $decode:ident: $d:ty);+ $(;)?) => {$ ( + #[kani::proof] + #[kani::unwind(513)] + fn $encode() { encode::<$d>(); } + + #[kani::proof] + #[kani::unwind(513)] + fn $decode() { decode::<$d>(); } + )+}; +} + +proofs! { + encode_1, decode_1: U1; + encode_4, decode_4: U4; + encode_5, decode_5: U5; + encode_6, decode_6: U6; + encode_10, decode_10: U10; + encode_11, decode_11: U11; + encode_12, decode_12: U12; +}