iracaML-KEMFIPS 203VerificaciónPost-cuánticaRustCrypto

iraca: independent differential verification of ML-KEM (FIPS 203) in RustCrypto

Published on 2026-09-25 · Xiliux

What we did

iraca is a harness that verifies the post-quantum cryptography the Rust ecosystem actually ships, by differencing it against an independent implementation. First public result: the widely-used RustCrypto ml-kem crate (ML-KEM / FIPS 203), which has no published independent audit, is byte-for-byte identical to the pq-crystals C reference across key generation, encapsulation and decapsulation, and correctly rejects the non-canonical keys FIPS 203 requires.

This is a conformance spot-check, not a full audit, and it does not cover side channels (the KyberSlash class).

Why it matters

The NIST standards (FIPS 203/204/205) are final and migration is mandated. Much of the Rust world uses the RustCrypto crates, which today have no independent audit. Differencing a widely-used implementation against a separate one, in a different language, catches the class of error two same-language ports could share.

The method: the same raw bytes to both sides

iraca feeds the same bytes to the crate and to the pq-crystals C reference through their deterministic entry points, with no DRBG and no .rsp replay. With determinism end to end, any disagreement is a real one, not randomness noise. The C reference is compiled from source and linked behind a thin FFI module; everything else is safe Rust.

An adversarial layer also tests input validation: it generates non-canonical encapsulation keys (a coefficient greater than or equal to q) and checks the crate rejects them, as FIPS 203 requires (the modulus check). The oracle for canonicity is the standard itself, not another implementation.

Results

Every result ships a red/green pair and a positive control: a no-disagreement result means the comparison path actually ran and can discriminate.

What it is not

Not a full audit; not side-channel or timing analysis; one version and a few concrete properties. Assurance is cumulative, not a single stamp.

Reproducible, and open to collaboration

The harness is small, deterministic and built to be re-run. If you maintain a post-quantum implementation and want an independent differential and adversarial pass, or an oracle to diff your own work against, that is what it is for. I also work with the Ethereum Foundation's post-quantum effort on signature-scheme verification.

FAQ

What is iraca?

A differential and adversarial verification harness for post-quantum cryptography: it compares an implementation against an independent reference by feeding the same bytes, and tests input validation against the standard itself.

Did you find a bug in RustCrypto ml-kem?

No. This is an assurance result: RustCrypto passes the verified FIPS 203 checks. It is a conformance spot-check, not a full audit, and it does not cover side channels.

Is this useful for my post-quantum implementation?

Yes: the harness can difference your implementation against the reference and test its input validation, with positive controls and red/green pairs.

← More articlesRequest a quote