pq-verify: Independent verification for ML-KEM / ML-DSA implementations

Abstract

Fixed A response answering one question twice could verify. A second answer to the same tcId replaced the first, so a response carrying a wrong answer followed by the right one reported VERIFIED. Any question answered more than once is now a finding, whatever the answers say. A truncated .json.gz response crashed the CLI with EOFError instead of reporting CANNOT VERIFY. Readers bound their input. A response larger than 64 MiB (measured after decompression, so a gzip bomb cannot expand in memory) or a hybrid transcript larger than 1 MiB is CANNOT VERIFY, and at most one byte past the limit is read. The largest genuine documents are about 3.3 MB and 8 KB. Freivalds used published seeds. Every Freivalds check drew its random vector from a constant in the source (42, trial + 1, ...), so anyone could compute it and build an NTT output that is wrong in several coefficients yet passes. The seed is now drawn from the OS once per run and printed; PQV_FREIVALDS_SEED=0x... replays a run. The Hasse check rejected genuine curves. It used 2*isqrt(p), which is one short of ⌊2√p⌋ for p = 7, 13, ..., and reported y² = x³ + 3 over F₇ (t = −5) as CRITICAL. The bound is now isqrt(4p). Since no curve can exceed it, a violation is now reported as a defect in pq-verify's point count, not the curve's, and the "near-extreme trace" MEDIUM finding, which is not a known weakness, is gone. Two self-suite checks could not fail. "100,000 NTT butterflies" compared (a + w*b) % q with itself; it now runs every butterfly through the engine's Montgomery multiply and compares with integer arithmetic. "Freivalds throughput" passed unconditionally; it now requires every correct NTT to be accepted. The self-suite is still 160 checks. The Coq certificates proved almost nothing about the run. The "Full Kyber-768 NTT" certificate contained one layer-0 butterfly, and the batch certificate proved sums of random numbers drawn for the purpose. See Changed. Changed --verify-hybrid recomputes the ML-KEM half, or does not say VERIFIED. Nothing tied the ciphertext in the server share to the ML-KEM secret in the combined secret, so a transcript with a corrupted ciphertext was reported VERIFIED. A transcript may now carry the client's ephemeral ML-KEM decapsulation key (clientMlkemDecapsulationKey, optional, like the ECDHE private scalars): pq-verify checks it against the client share and FIPS 203 §7.3, decapsulates the ciphertext and compares the result byte-for-byte. Without the key that check is NOT CHECKED and the result is PARTIAL, so transcripts that verified before without it now report PARTIAL. Coq certificates are real, and checked for axioms. The NTT certificate defines the FIPS 203 forward NTT and zeta table in Coq and proves ntt input = output for all 256 coefficients (896 butterflies), plus 17¹²⁸ ≡ −1 (mod 3329). The batch certificate proves pq-verify's ML-KEM and ML-DSA zeta tables are root^brv(i) mod q as FIPS 203/204 define them. A certificate passes only if coqc accepts it and Print Assumptions reports every theorem closed, so an Admitted proof (which coqc accepts) or an added axiom fails. The "Coq-certified" tagline is replaced by what is actually proved. Added General proofs, pq-verify --proofs. pq_verify/coq/ now holds theorems that quantify over every input, checked by coqc with every theorem required to be closed (no axioms, no Admitted): NTT.v: the FIPS 203 (ML-KEM) and FIPS 204 (ML-DSA) forward NTT equal the Chinese-remainder map they are defined to compute, for every 256-coefficient input. The transform is written once, generic over its arithmetic; a map that preserves the arithmetic commutes with it, so running it once on symbolic linear forms gives its matrix, which Coq checks entry by entry against the CRT matrix. Reduce.v: montgomery_reduce (ML-KEM, ML-DSA), barrett_reduce (ML-KEM, all 65,536 int16 inputs) and reduce32 (ML-DSA) are congruent to their input and within bound for every input in range, with no intermediate overflow. Per-run NTT certificates now emit NTT.v's transform verbatim, so they are about the proved definition. Finding: two documented bounds in pq-crystals/dilithium ref/reduce.c are off by one. montgomery_reduce documents -Q < r < Q for -2^31 Q <= a <= Q 2^31, but a = Q 2^31 returns Q; reduce32 documents r >= -6283008, but a = -255·2^23 - 2^22 returns -6283009. The code is right and no ML-DSA input comes near either point; the comments overstate it. The proofs state the true bounds, and both witnesses are checked theorems. (ML-KEM's comment excludes its corresponding point and is exact.) Wycheproof and CCTV edge-case vectors, pinned. 24 files from C2SP Wycheproof (3fa63dd) and CCTV (50a8ecf) ship in pq_verify/vectors/edge_vectors.json.gz, each with its upstream sha256 in EDGE_MANIFEST.json; tools/pin_edge_vectors.py re-pins them deterministically. They cover what NIST's ACVP vectors mostly do not: strcmp-trap ciphertexts, unlucky XOF sampling, every coefficient value q…4095 at every position of an encapsulation key, corrupted decapsulation keys, malleated ciphertexts, and ML-DSA hint, norm-bound and context edges. --audit-kem runs them against the vendor library as three new stages, edgeValid, edgeEk, edgeDk (edge=False to skip). The pinned vendor table records them: mlkem-native 4,320/4,320; PQClean accepts all 2,931 invalid encapsulation keys and all 6 invalid decapsulation keys while every valid output is byte-exact. pq-verify --edge-cases [SET] runs them against pq-verify's own references (kyber-py, dilithium-py), with --json and --fail-on-finding. The doctor checks the bundle's digests offline and runs the vectors against the installed references (--fast skips that run): a failure not in KNOWN_REFERENCE_DEFECTS BLOCKs. Finding: dilithium-py 1.4.0 accepts a repeated hint index. FIPS 204 Algorithm 21 (HintBitUnpack) requires strictly increasing indices; dilithium-py compares with < instead of <=, so Wycheproof's "repeated hint" signature verifies for ML-DSA-44/65/87. It is fixed upstream (GiacomoPope/dilithium-py bd9b552) but in no release. pq-verify grades third-party signatures against NIST's expected results, not dilithium-py's verdict, so no third-party result changes; --edge-cases reports the reference as FINDINGS PRESENT until a fixed release can be pinned. tests/fuzz_readers.py — a structure-aware fuzzer for the readers that take files from outside parties. It mutates genuine responses and transcripts ~25 ways (type confusion, truncation, deep nesting, oversized and gzipped input, flipped hex digits, duplicate entries) and requires, for every case, no exception, an honest status, prompt termination, a CLI exit of 0/1/2, and no VERIFIED for a document that differs from a genuine one. It found all three bugs above and the hybrid gap. A seeded slice runs in the test suite. Verifying this release gh attestation verify pq_verify-2.9.0-py3-none-any.whl \ --repo bigDSanalyst/pq-verify Built by .github/workflows/release.yml from commit c029a633f46b4400e34b8c3c5cbcb1bbee854dd6, after the full suite and all 855 NIST ACVP vectors passed on Python 3.9 through 3.13. An SPDX SBOM is attached and attested.