From 476f669f5c37348951c2ddd966ed4b2d5ca23e91 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 28 Jul 2026 09:46:29 +0200 Subject: [PATCH] bridge: re-pin to the NIST-ACVP source commit; state the real coverage numbers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The companion fips205-source commit adds NIST ACVP SHA2-128s verification vectors and a real differential bridge. This repo re-pins to it and replaces the word "finite" with numbers, per external review rounds 4-6. - extract.sh + PROVENANCE re-pinned 797b4ef -> 3153988. The provenance guard did its job first: it REFUSED the moved source until the pin was rotated deliberately. - VERIFIED that the test/vector commit does not perturb the proved model: after re-extraction all four pinned model files are byte-identical (Types db720b4a…, Funs 7b7de55f…, TypesExternal 37958beb…, FunsExternal 5efe551c…), check.sh is ALL GREEN, and the audit digest is unchanged (d83e297a…). The only regenerated difference is the untracked Aeneas *_Template.lean byproduct, which Phase 0 purges. - TRUSTED-BASE item 9 and the README now state the bridge's actual size: 131 assertion points (was 9), of which 20 are NIST ACVP SHA2-128s known-answer tests run against the proved path — 10 from the `internal` group (whose message IS M', exactly what slh_verify_128s consumes) and 10 from `external pure` where mono, the deployed verifier and NIST must all agree, 9 of those with a NON-EMPTY context, which is the first empirical check of the domain-separator byte and context prefix that item 10 declares outside every proof. Both documents keep saying plainly that a passing differential test is evidence, not a proof. Co-Authored-By: Claude Opus 4.8 --- README.md | 19 ++++++++++++++----- TRUSTED-BASE.md | 22 +++++++++++++++++++--- verification/PROVENANCE.json | 6 +++--- verification/extract.sh | 2 +- 4 files changed, 37 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index 0900655..345a1e1 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ path**, extracted from a pure-Rust implementation into Lean 4 via Charon/Aeneas — the same pipeline, discipline, and honesty rules as the four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`). -## STATUS: eleven certificates over the extracted verify model (external review rounds 1–5 applied) +## STATUS: eleven certificates over the extracted verify model (external review rounds 1–6 applied) `verification/check.sh` is **green** (exit 0): the model compiles, the proofs compile, and the audit passes. The audit runs **inside Lean** @@ -64,8 +64,15 @@ cannot translate the deployed `Hashers` function-pointer struct): certificate — and it determines the FORS indices / WOTS digits, so a defect there could change the recomputed root while all eleven theorems still hold. - **Not the deployed public verifier:** the proved subject is the private - `verify_mono` facade; the bridge to upstream's generic `pk.verify()` is the - finite in-snapshot **differential test**, not a machine-checked refinement. + `verify_mono` facade; the bridge to upstream's generic `pk.verify()` is a + finite **differential test**, not a machine-checked refinement. Its size is + now stated rather than left to the word "finite": **131 assertion points**, + of which **20 are NIST ACVP SHA2-128s known-answer tests run against the + proved path** (see TRUSTED-BASE.md item 9). Until 2026-07-28 it was nine + points from a single seed, and this parameter set had *no* NIST verification + coverage at all — the vectors vendored upstream contain no SHA2-128s sigVer + group, so the 128s groups were extracted from the official NIST ACVP-Server + set (provenance recorded in the vector file). - **Not closed-form FIPS 205 correctness:** the folds are transliterations of the extracted loops (the hash primitives stay opaque); nothing here relates the recomputed root to a mathematical SLH-DSA specification. @@ -156,8 +163,10 @@ casts, the WOTS+ checksum `iter().take()` + `&u32` Sub → an index loop — each site a local rewrite whose equivalence is argued in the commit and checked, for SHA2-128s, by the differential test; the obsoleted transpiler axioms were deleted from the external files); fidelity pinned by that -differential test in the snapshot (valid / corrupted / wrong-message), -re-run green after every source patch. +differential test in the snapshot — since 2026-07-28 a randomized bridge +(12 rounds, corruption across the whole signature, wrong-key and wrong-context +cases) plus NIST ACVP 128s known-answer tests — re-run green after every +source patch. - **`fips205.fors_inner_loop_eq`** + **`fips205.fors_outer_loop_eq`** (Algorithm 17, FORS pk-from-sig): a nested loop, split into two theorems. diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 56c0294..8f7fb47 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -42,9 +42,25 @@ proceeds and is part of every claim. has no certificate; a defect there could change the recomputed root while all eleven theorems still hold. 9. **The deployed generic verifier.** The proved subject is the private - `verify_mono` facade. The bridge to upstream's generic `pk.verify()` is - the finite in-snapshot differential test, not a machine-checked - refinement. + `verify_mono` facade. The bridge to upstream's generic `pk.verify()` is a + finite differential test, **not** a machine-checked refinement — no theorem + here says the two agree; the evidence is empirical and its size is stated so + a reader can judge it (external review, rounds 4–6, correctly objected that + "finite" without a number is not a disclosure): + - **131 assertion points** (was 9 until 2026-07-28: three rounds from one + fixed seed, corrupting one fixed byte of a 7856-byte signature); + - of those, **20 are NIST ACVP SHA2-128s known-answer tests run against the + proved path** — 10 from the `internal` group, whose message *is* M′ and so + is exactly what `slh_verify_128s` consumes, and 10 from the `external pure` + group where mono, the deployed verifier and NIST must all three agree. + NIST's negatives cover structurally distinct corruption sites (modified R, + SIGFORS, SIGHT, modified message) rather than one arbitrary byte; + - the remaining 108 are randomized: 12 rounds, varying message lengths + including empty, corruption spread across the whole signature, plus + wrong-public-key and wrong-context cases. + Still **not** covered by any of it: agreement on inputs nobody generated, and + the prehash variant against the mono path (see item 10). A passing + differential test is evidence, not a proof. 10. **Everything above the extraction root.** The root is `verify_mono::slh_verify_128s = slh_verify_internal_free(M′, sig, pk)`, which takes the message-digest input **M′ as an argument**. The code in diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json index bad8ff9..12ed48d 100644 --- a/verification/PROVENANCE.json +++ b/verification/PROVENANCE.json @@ -3,9 +3,9 @@ "parameter_set": "SLH-DSA-SHA2-128s", "source": { "repo": "github.com/saymrwulf/fips205-source", - "head": "797b4ef26338e27363683656f93cb065a77daa0e", + "head": "3153988c4e89df66c41e698329f2ae5460880875", "upstream_base": "integritychain/fips205 @ 30bac08580aa61f653e5436d1bbacb5ffac446c4", - "upstream_deviation": "verbatim import minus CI workflows; then the additive monomorphic verify_mono compat module + de-plumbing rounds 1-2, each an individually-justified commit", + "upstream_deviation": "verbatim import minus CI workflows; then the additive monomorphic verify_mono compat module + de-plumbing rounds 1-2, each an individually-justified commit; then NIST ACVP SHA2-128s sigVer vectors + an expanded differential bridge (TEST-ONLY: no verify-path function changed, and re-running extract.sh against this commit reproduces all four model files byte-identically)", "cargo_lock": "committed", "rust_toolchain_toml": "nightly-2026-06-01" }, @@ -36,7 +36,7 @@ "gen/SlhVerify/TypesExternal.lean", "gen/SlhVerify/FunsExternal.lean" ], - "byte_identical_regeneration_verified": "2026-07-24", + "byte_identical_regeneration_verified": "2026-07-28 (re-verified after the test/vector commit: all four pinned model files unchanged)", "model_integrity_sha256": { "_comment": "All four Lean model files check.sh Phase 0 pins before compiling anything \u2014 the two aeneas-generated files AND the two hand-maintained *External files (which carry the five oracle axioms and the Step defs). A hand-edit of the model fails the build here (round-4 reviewer F3).", "gen/SlhVerify/TypesExternal.lean": "37958beb7c90b649497a20b0802f98f0fb2d975c245eca956d7396af74d7759f", diff --git a/verification/extract.sh b/verification/extract.sh index e31600f..3599c53 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -33,7 +33,7 @@ CRATE="${1:-$HOME/GitClone/FormalVerification/sources/fips205-source}" # The pinned source commit this repo's model + proofs were verified against. # Keep in lockstep with verification/PROVENANCE.json and the README snapshot. -EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-797b4ef26338e27363683656f93cb065a77daa0e}" +EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-3153988c4e89df66c41e698329f2ae5460880875}" # ── Provenance guard: refuse a wrong or dirty source tree (fail-closed) ────── [ -d "$CRATE/.git" ] || { echo "ERROR: '$CRATE' is not a git checkout of fips205-source." >&2; exit 2; }