diff --git a/README.md b/README.md index 12ce726..3947375 100644 --- a/README.md +++ b/README.md @@ -5,11 +5,16 @@ 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 round 1 applied) +## STATUS: eleven certificates over the extracted verify model (external review round 2 applied) `verification/check.sh` is **green** (exit 0): the model compiles, the -proofs compile, and the axiom audit passes (the Phase-3 parser was rewritten -to be fail-closed and wrap-safe after external review round 1, 2026-07-24). +proofs compile, and the axiom audit passes. The audit now runs **inside +Lean** (`verification/Proofs/Audit.lean`): it reads each certificate's cone +from the kernel via `collectAxioms` and asserts SET EQUALITY against that +certificate's expected boundary — so an *added* axiom and a silently +*dropped* oracle dependency both fail, with no text parsing to misparse +(external review round 2, 2026-07-24, replaced the earlier `#print axioms` +text parser, which could fail open on an empty or truncated report). **What is actually established** — eleven Lean theorems about the Aeneas-generated model of the **monomorphic `verify_mono` compatibility @@ -56,14 +61,15 @@ The trust base and residual assumptions are stated in - **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the extracted `chain_free` loop equals the explicit s-fold hash chain, with the hash address set to i, i+1, …, i+s−1 in turn. This rules out — - machine-checked, for the deployed monomorphic SHA2-128s verify path — an + machine-checked, for the monomorphic SHA2-128s `verify_mono` path — an off-by-one loop bound, a wrong address field, and wrong threading. Its `#print axioms` cone is **exactly** `[propext, Classical.choice, Quot.sound, verify_mono.oracle.f]` — the three kernel axioms plus the one hash oracle it touches, and nothing else (no transpiler plumbing; the u32 range machinery was discharged with real definitions). check.sh Phase 3 - fails the build if any certificate cone contains anything outside the - kernel three + the five documented SHA-2 oracles. + (the in-Lean exact-cone audit) fails the build if any certificate's cone + differs from its expected set — an extra axiom or a dropped oracle both + break it. - **`fips205.wots_loop1_eq`** (Algorithm 8, WOTS+ pk recomputation — the chain loop): the extracted `wots_pk_from_sig_free_loop1` equals the fold @@ -103,10 +109,11 @@ exit 0); the u32 range-loop de-plumbing (faithful `Step` defs vs pinned rustc, axiom-clean); the 8-site source de-plumbing (snapshot commit `6f6a9d6`: `try_from`/`is_err`/`unwrap` on pre-masked values → plain casts, the WOTS+ checksum `iter().take()` + `&u32` Sub → an index loop — -each site semantics-identical for every FIPS 205 parameter set, and the -obsoleted transpiler axioms deleted from the external files); fidelity -pinned by a differential test in the snapshot (valid / corrupted / -wrong-message), re-run green after every source patch. +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. - **`fips205.fors_inner_loop_eq`** + **`fips205.fors_outer_loop_eq`** (Algorithm 17, FORS pk-from-sig): a nested loop, split into two theorems. @@ -131,10 +138,14 @@ wrong-message), re-run green after every source patch. removing the last `Take`/`IterMut` iterator adapters; the obsoleted `Take` axiom was then deleted. -The remaining work (the digest-split composition and the apex — the top-level -`slh_verify` accepting iff the recomputed hypertree root equals the pinned -public-key root) is not yet proven. The pyramid rises one certificate at a -time, each audited to the same boundary. +The apex (`slh_verify_128s_accepts_iff`, above) sits at the top of this layer: +the extracted `verify_mono::slh_verify_128s` accepts iff the recomputed +hypertree root byte-equals the pinned public-key root. What remains genuinely +unproven is stated in "What is NOT (yet) established" above — most sharply the +opaque `base_2b` inner loop (no certificate) and the bridge from this private +`verify_mono` facade to the deployed generic verifier (a finite differential +test, not a machine-checked refinement). Each certificate is audited to the +same boundary. ## Subject @@ -143,12 +154,15 @@ time, each audited to the same boundary. modules mirroring the FIPS 205 algorithm structure. - Pinned at upstream commit `30bac08580aa61f653e5436d1bbacb5ffac446c4` (2025-09-01), snapshotted with full history at - `saymrwulf/fips205-source` (snapshot head `5dca0db`, whose single - deviation from verbatim is the removal of upstream CI workflows, - documented in that commit). Aeneas-compat patches will land in the - snapshot repo as transparent, individually-justified commits — never - upstream. **No affiliation with, and no changes proposed to, the - upstream project.** + `saymrwulf/fips205-source`. The verbatim-import base commit's only + deviation from upstream is the removal of CI workflows (documented in + that commit); the Aeneas-compat and de-plumbing patches then landed as + transparent, individually-justified commits on top — never upstream. + The current snapshot head is **`797b4ef`** (the round-2 reproducibility + commit — committed `Cargo.lock` + pinned `rust-toolchain.toml` — on top of + de-plumbing round 2, `bea1051`); the model in this repo is extracted from + it, and `verification/extract.sh` refuses any other commit. **No + affiliation with, and no changes proposed to, the upstream project.** - Parameter set: **SLH-DSA-SHA2-128s** first (the small-signature profile deployed in the firmware/code-signing lane). The architecture generalizes; each further parameter set is a separate claim (rigor @@ -169,9 +183,15 @@ Key generation and signing are out of scope (trusted base), exactly as ed25519 signing was. The five verify-path hash oracles (`h_msg, f, h, t_l, t_len` — SHA-2 instantiations; `prf`/`prf_msg` are sign-side only and never enter the cone) are opaque external models with written -justifications, kept outside every certificate's dependency cone -(honesty invariant H4); their semantics are the standing SHA-2 oracle -boundary documented in [TRUSTED-BASE.md](TRUSTED-BASE.md). +justifications. They are the *only* things beyond Lean's three kernel +axioms that any certificate cone contains: each cone is exactly the +kernel three plus the specific oracles that certificate's computation +reaches (e.g. `chain` reaches `F`, so `oracle.f` is inside its cone; the +input-prep helpers reach no hash, so their cones are kernel-3 alone). +That the cones contain *nothing else* — no transpiler plumbing, no +hidden axiom — is what the audit enforces (honesty invariant H4); their +semantics are the standing SHA-2 oracle boundary documented in +[TRUSTED-BASE.md](TRUSTED-BASE.md). ## Gate-0 record (2026-07-22) @@ -195,32 +215,44 @@ this repository was created: (nested `&[&[u8]]` is untranslatable), and one `let-else` became the `is_err`/`unwrap` idiom. `verification/extract.sh` now re-derives the model from the mono root; charon + aeneas both exit 0, and - `verification/check.sh` compiles the result. The generic paths and all - twelve parameter sets are untouched (the only change to existing code is - two lines wiring the module). + `verification/check.sh` compiles the result. At this compat-patch commit + the only change to pre-existing code was two lines wiring the new module; + the generic paths and all twelve parameter sets stayed untouched. (The + later de-plumbing commits — rounds 1 and 2 — then made further local edits + to `helpers.rs`/`wots.rs`, each documented and differential-tested; see the + snapshot history at head `797b4ef`.) -## What will be claimed (when the button is green, not before) +## What is claimed (the button is green) -One theorem per layer, each a statement about the **extracted** functions -(H3), compiled by `verification/check.sh` with a per-certificate -`#print axioms` audit (H1): chain semantics, WOTS+ pk recomputation, -XMSS path recomputation, hypertree acceptance, FORS pk recomputation, -and the apex — `slh_verify_internal` accepts iff the recomputed -hypertree root equals the pinned public-key root. +Each certificate is a statement about the **extracted** functions (H3), +compiled by `verification/check.sh` with the in-Lean exact-cone audit (H1): +chain semantics, WOTS+ pk recomputation, XMSS path recomputation, hypertree +acceptance, FORS pk recomputation, the input-prep helpers, and the apex — +`verify_mono::slh_verify_128s` accepts iff the recomputed hypertree root +equals the pinned public-key root. The precise scope and non-claims are in +the STATUS section above. **The allowed axiom set, stated precisely:** unlike the ed25519 field and scalar layers (whose cones are exactly `[propext, Classical.choice, Quot.sound]`), the hash oracles permeate *every* SLH-DSA layer — `chain` -already calls `F`. So each certificate's cone may contain the three -kernel axioms **plus at most the five named oracles** -(`verify_mono.oracle.{h_msg, f, h, t_l, t_len}`) — and nothing else: the -transpiler-plumbing axioms currently in `FunsExternal.lean` must be -discharged before any certificate ships, and the audit fails the button -if any of them (or anything unlisted) appears in a cone. +already calls `F`. Each certificate's cone is therefore the three kernel +axioms **plus exactly the named oracles its computation reaches** (and +nothing else). The transpiler-plumbing axioms that once sat in +`FunsExternal.lean` were discharged (de-plumbing rounds 1+2) before any +certificate shipped; the audit fails the button if anything outside a +certificate's expected boundary — plumbing, an extra oracle, or a dropped +one — appears in its cone. ## Discipline Every Lean compile in this repository runs under `verification/lean-guard` -(memory-capped, machine-wide serialized). Extraction is reproducible from -the committed `extract.sh` against the pinned snapshot (R1). What cannot -be proven is named in [TRUSTED-BASE.md](TRUSTED-BASE.md), not hidden (H5). +(memory-capped, machine-wide serialized). Extraction is reproducible: the +full pin set (source commit, Charon/Aeneas commits + toolchain channel, Lean +and OCaml versions) is in [verification/PROVENANCE.json](verification/PROVENANCE.json); +`verification/extract.sh` refuses to run against a wrong-commit or dirty +source tree, and re-running it reproduces the aeneas-generated model +byte-identically (verified 2026-07-24). The axiom audit runs inside Lean +([verification/Proofs/Audit.lean](verification/Proofs/Audit.lean)): exact +per-certificate cone equality, fail-closed, adversarially exercised by +`verification/check-selftest.sh`. What cannot be proven is named in +[TRUSTED-BASE.md](TRUSTED-BASE.md), not hidden (H5). diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 7fa7660..7c4db1e 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -1,7 +1,10 @@ -# TRUSTED-BASE — what the certificates will NOT cover +# TRUSTED-BASE — what the certificates do NOT cover -Initial statement, written at skeleton time (nothing proven yet); this -file is maintained as the campaign proceeds and is part of every claim. +Eleven certificates over the extracted `verify_mono` model are now proven +(`verification/check.sh` green; the apex is +`fips205.slh_verify_128s_accepts_iff`). This file states what those +certificates deliberately do NOT establish; it is maintained as the campaign +proceeds and is part of every claim. 1. **The five verify-path hash oracles.** `h_msg, f, h, t_l, t_len` (SLH-DSA-SHA2-128s instantiations over SHA-256; `prf`/`prf_msg` are @@ -25,7 +28,20 @@ file is maintained as the campaign proceeds and is part of every claim. 6. **Parameter-set scope.** Claims will bind SLH-DSA-SHA2-128s only; other parameter sets are unverified until separately extracted and proven (R2). -7. **Aeneas-compat patch surface.** The fn-pointer-to-named-oracle - rewrite in `fips205-source` (phase 1) is part of the verified surface: - the certificate covers the patched verify path, and the patch commits - are the auditable delta from upstream `30bac08`. +7. **Aeneas-compat + de-plumbing patch surface.** The fn-pointer-to-named- + oracle rewrite in `fips205-source` (phase 1) and the two de-plumbing + rounds (index-loop rewrites of the iterator adapters on the verify path, + de-plumbing round 2 at `bea1051`; current snapshot head `797b4ef`) are + part of the verified surface: the + certificates cover the *patched* verify path, and the patch commits are + the auditable delta from upstream `30bac08`. Each rewrite's equivalence + to upstream is argued in its commit and checked, for SHA2-128s, by the + snapshot differential test — it is not itself machine-checked. +8. **The `base_2b` inner loop.** `helpers.base_2b_loop0_loop0` (which + determines the FORS indices and WOTS digits) is threaded opaquely and + 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. diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json new file mode 100644 index 0000000..9cf7e79 --- /dev/null +++ b/verification/PROVENANCE.json @@ -0,0 +1,36 @@ +{ + "_comment": "Single machine-readable pin set to reproduce the extracted Lean model in gen/SlhVerify from source. External review round 2 (2026-07-24). Running verification/extract.sh against the pinned source tree with the pinned Charon/Aeneas toolchain reproduces the two aeneas-generated files byte-identically (sha256 below). The *External*.lean files are hand-maintained (not regenerated) and are NOT part of this reproducibility claim.", + "parameter_set": "SLH-DSA-SHA2-128s", + "source": { + "repo": "github.com/saymrwulf/fips205-source", + "head": "797b4ef26338e27363683656f93cb065a77daa0e", + "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", + "cargo_lock": "committed", + "rust_toolchain_toml": "nightly-2026-06-01" + }, + "transpiler": { + "charon": { "commit": "9dd7f23c", "toolchain_channel": "nightly-2026-06-01" }, + "aeneas": { "commit": "bf13c42e" } + }, + "proof_env": { + "lean": "v4.30.0-rc2 (3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc)", + "ocaml": "5.3.0" + }, + "extraction": { + "driver": "verification/extract.sh (refuses a wrong-commit or dirty source tree)", + "charon": "charon cargo --preset=aeneas --start-from crate::verify_mono::slh_verify_128s --opaque crate::verify_mono::oracle --opaque sha2 --opaque sha3 --opaque zeroize --opaque rand_core --hide-marker-traits --dest-file SlhVerify.llbc -- --no-default-features --features slh_dsa_sha2_128s", + "aeneas": "aeneas -backend lean -split-files -subdir SlhVerify -dest gen SlhVerify.llbc" + }, + "generated_artifacts_sha256": { + "SlhVerify.llbc": "d8ec0b00593eee1778bc4cc0cc1801fb6415bb294425f01384434849c6443f58", + "gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384", + "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f" + }, + "hand_maintained_not_regenerated": [ + "gen/SlhVerify/TypesExternal.lean", + "gen/SlhVerify/FunsExternal.lean" + ], + "byte_identical_regeneration_verified": "2026-07-24", + "audit_gate": "verification/Proofs/Audit.lean — in-Lean exact per-certificate cone equality via collectAxioms (fail-closed); compiled by check.sh Phase 3; adversarially exercised by check-selftest.sh" +} diff --git a/verification/Proofs/Audit.lean b/verification/Proofs/Audit.lean new file mode 100644 index 0000000..69f30aa --- /dev/null +++ b/verification/Proofs/Audit.lean @@ -0,0 +1,97 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/Audit.lean — the axiom-cone audit, performed INSIDE Lean. + + Round-2 external review (2026-07-24) showed the bash `#print axioms` text + parser was still fragile: it fail-OPENED on an empty `[]` or a truncated + (missing-`]`) report, and it only subset-checked (a *removed* oracle + dependency would pass unnoticed). This file removes text parsing entirely. + + `collectAxioms` reads the kernel's own axiom set for each certificate. We + assert, for every one of the eleven: + + · the certificate EXISTS and is a `theorem` (not an axiom/opaque sham, + not a renamed/deleted name — `collectAxioms` returns `#[]` for a + missing name, so existence is checked explicitly, fail-closed); + · its cone equals its EXPECTED set EXACTLY — extras (a smuggled axiom) + AND missing (a silently dropped oracle dependency) both fail. + + Any mismatch is a `throwError`, i.e. a Lean elaboration error → non-zero + `lean` exit. There is no text to misparse and nothing fails open. This is + the single source of the axiom claim; check.sh Phase 3 just compiles it. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ChainSpec +import Proofs.WotsSpec +import Proofs.XmssSpec +import Proofs.HtSpec +import Proofs.ForsInnerSpec +import Proofs.ForsOuterSpec +import Proofs.InputPrepSpec +import Proofs.ApexSpec +open Lean Elab Command + +namespace SlhVerify.Audit + +/-- Lean's three kernel axioms — permitted in every cone. -/ +def kernel3 : List Name := [`propext, `Classical.choice, `Quot.sound] + +/-- The five SHA-2 verify-path hash oracles — the documented cryptographic + boundary (TRUSTED-BASE.md). No other axiom may appear anywhere. -/ +def oracleF : Name := `verify_mono.oracle.f +def oracleH : Name := `verify_mono.oracle.h +def oracleTL : Name := `verify_mono.oracle.t_l +def oracleTLen : Name := `verify_mono.oracle.t_len +def oracleHMsg : Name := `verify_mono.oracle.h_msg + +/-- The entire allowed boundary: nothing outside this set is permitted in any + certificate cone, and the expected table below may reference nothing else. -/ +def allowedBoundary : List Name := + kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg] + +/-- EXACT expected cone per certificate. Ground truth captured 2026-07-24 via + `collectAxioms` (Probe.lean) and cross-checked against both round-1 + reviewers' independent reconstructions. Each entry is asserted for SET + EQUALITY, so this table is a load-bearing specification of the boundary: + changing a proof so it drops an oracle, or adds one, breaks the audit. -/ +def expectedCones : List (Name × List Name) := + [ (`fips205.chain_free_loop_eq, kernel3 ++ [oracleF]), + (`fips205.wots_loop1_eq, kernel3 ++ [oracleF]), + (`fips205.xmss_loop_eq, kernel3 ++ [oracleH]), + (`fips205.ht_loop_eq, kernel3 ++ [oracleF, oracleH, oracleTL]), + (`fips205.fors_inner_loop_eq, kernel3 ++ [oracleH]), + (`fips205.fors_outer_loop_eq, kernel3 ++ [oracleF, oracleH]), + (`fips205.to_int_loop_eq, kernel3), + (`fips205.to_byte_loop_eq, kernel3), + (`fips205.wots_csum_loop_eq, kernel3), + (`fips205.base2b_outer_loop_eq, kernel3), + (`fips205.slh_verify_128s_accepts_iff, kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg]) ] + +elab "auditCones" : command => do + let env ← getEnv + -- (0) the expected table itself must stay within the boundary — guards a typo + -- in this file from silently widening what "allowed" means. + for (cert, expected) in expectedCones do + for a in expected do + unless allowedBoundary.contains a do + throwError "audit table references non-boundary axiom {a} for {cert}" + -- (1) per certificate: exists ∧ is a theorem ∧ cone == expected set exactly. + let mut errs : Array String := #[] + for (cert, expected) in expectedCones do + match env.find? cert with + | none => errs := errs.push s!"{cert}: NOT FOUND (renamed/deleted?)" + | some (.thmInfo _) => + let got := (← collectAxioms cert).toList + let extras := got.filter (fun a => !expected.contains a) + let missing := expected.filter (fun a => !got.contains a) + unless extras.isEmpty && missing.isEmpty do + errs := errs.push s!"{cert}: extra={extras} missing={missing}" + | some (.axiomInfo _) => errs := errs.push s!"{cert}: is an AXIOM, not a proven theorem" + | some (.opaqueInfo _) => errs := errs.push s!"{cert}: is OPAQUE, not a proven theorem" + | some _ => errs := errs.push s!"{cert}: not a theorem" + unless errs.isEmpty do + throwError "EXACT-CONE AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}" + logInfo s!"exact-cone audit PASSED: {expectedCones.length} certificates, each cone == its expected boundary set (kernel-3 + only the named SHA-2 oracles)" + +end SlhVerify.Audit + +open SlhVerify.Audit in +auditCones diff --git a/verification/Proofs/ChainSpec.lean b/verification/Proofs/ChainSpec.lean index 612b571..8e59bb1 100644 --- a/verification/Proofs/ChainSpec.lean +++ b/verification/Proofs/ChainSpec.lean @@ -3,8 +3,9 @@ THEOREM chain_free_loop_eq: the extracted `chain_free` loop equals the explicit s-fold application of the hash F, with the hash-address set to i, i+1, …, i+s−1 in turn. This rules out — machine-checked, for the - deployed monomorphic SHA2-128s verify path — an off-by-one loop bound, a - wrong address field, and wrong threading. F stays opaque + monomorphic SHA2-128s `verify_mono` path (a private facade, not the + deployed generic verifier) — an off-by-one loop bound, a wrong address + field, and wrong threading. F stays opaque (verify_mono.oracle.f), so the certificate cone is the three kernel axioms + oracle.f, and nothing else (audited by check.sh Phase 3). diff --git a/verification/RECORDED-RUN.md b/verification/RECORDED-RUN.md new file mode 100644 index 0000000..695ec43 --- /dev/null +++ b/verification/RECORDED-RUN.md @@ -0,0 +1,50 @@ +# Recorded clean run — check.sh + independent cone dump + +External review round 2 asked for a recorded clean run at the current pin +by a party with the toolchain, so a reviewer who cannot run Lean has current +evidence. Captured 2026-07-24. Pins are in [PROVENANCE.json](PROVENANCE.json). +The cone dump below is an *independent* `collectAxioms` read (not the asserted +table in Proofs/Audit.lean); it matches each certificate's expected boundary. + +``` +RECORDED CLEAN RUN — fips205-slhdsa-verified +date(UTC): 20260724T171145Z +host lean: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release) +source pin: 797b4ef26338e27363683656f93cb065a77daa0e +============================================== +fips205-slhdsa-verified — check +=============================== +=== Phase 1: compile the extracted model === + · gen/SlhVerify/TypesExternal + · gen/SlhVerify/Types + · gen/SlhVerify/FunsExternal + · gen/SlhVerify/Funs +=== Phase 2: compile the proofs === + · ChainSpec + · WotsSpec + · XmssSpec + · HtSpec + · ForsInnerSpec + · ForsOuterSpec + · InputPrepSpec + · ApexSpec +=== Phase 3: axiom audit (exact cone per certificate — inside Lean) === + ✓ exact-cone audit PASSED: each of the 11 certificate cones == its expected boundary set + +ALL GREEN — model compiles, proofs compile, and every certificate cone +equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles. +Certificates proven: fips205.chain_free_loop_eq fips205.wots_loop1_eq fips205.xmss_loop_eq fips205.ht_loop_eq fips205.fors_inner_loop_eq fips205.fors_outer_loop_eq fips205.to_int_loop_eq fips205.to_byte_loop_eq fips205.wots_csum_loop_eq fips205.base2b_outer_loop_eq fips205.slh_verify_128s_accepts_iff + +=== INDEPENDENT cone dump (collectAxioms, 20260724T171253Z) === +fips205.chain_free_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f +fips205.wots_loop1_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f +fips205.xmss_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.h +fips205.ht_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.t_l +fips205.fors_inner_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.h +fips205.fors_outer_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f, verify_mono.oracle.h +fips205.to_int_loop_eq :: propext, Classical.choice, Quot.sound +fips205.to_byte_loop_eq :: propext, Classical.choice, Quot.sound +fips205.wots_csum_loop_eq :: propext, Classical.choice, Quot.sound +fips205.base2b_outer_loop_eq :: propext, Classical.choice, Quot.sound +fips205.slh_verify_128s_accepts_iff :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.h_msg, verify_mono.oracle.t_l, verify_mono.oracle.t_len +``` diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index fe827d6..9939756 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -1,25 +1,41 @@ #!/usr/bin/env bash -# Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit -# that cannot fail is theater). Three attacks, all MUST make check.sh fail: +# Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit that +# cannot fail is theater). The axiom audit now runs INSIDE Lean +# (Proofs/Audit.lean, exact cone per certificate via collectAxioms), so these +# attacks target that gate's actual guarantees — not the retired text parser. +# Every attack MUST make check.sh fail, via the intended gate: # -# 1. DEAD FILE — a stray Proofs/*.lean not in the manifest. -# 2. SMUGGLED AXIOM (short cone) — an axiom outside {kernel-3} ∪ {5 oracles}, -# on the FIRST line of the cone. -# 3. SMUGGLED AXIOM (WRAPPED cone) — an axiom on a CONTINUATION line of a -# cone that wraps (the exact fail-open exploit external review found on -# 2026-07-24: the old single-line parser saw only line 1). This attack -# guards the flattened-parse fix; a self-test that only plants short cones -# cannot detect a wrapped-cone parser regression. +# 1. DEAD FILE — a stray Proofs/*.lean not in the manifest. +# 2. SMUGGLED AXIOM — a certificate whose real cone contains a disallowed +# axiom, declared clean. Exact-equality must report it +# as `extra=[...]` (the classic extra-axiom detection). +# 3. DROPPED ORACLE — a certificate whose expected cone claims an oracle +# its real proof does NOT use. A subset checker would +# pass this; exact-equality must report `missing=[...]`. +# This is the property the round-2 review demanded and +# the retired subset parser could never enforce. +# 4. VANISHED CERT — a certificate name that no longer resolves. Since +# `collectAxioms` returns [] for a missing name (a +# fail-open trap), the audit must report NOT FOUND. # -# Green here means: the gates genuinely reject all three. Self-cleaning. +# Green here means: the gate genuinely rejects all four. Self-cleaning: the real +# check.sh / Proofs/Audit.lean are backed up and restored around every attack. set -euo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" cd "$HERE" -cleanup() { rm -f Proofs/Stray.lean Proofs/Stray.olean Proofs/EvilSpec.lean \ - Proofs/EvilSpec.olean Proofs/EvilWrapSpec.lean \ - Proofs/EvilWrapSpec.olean check-evil-tmp.sh check-evilwrap-tmp.sh; } +restore() { + [ -f check.sh.selftest.bak ] && mv -f check.sh.selftest.bak check.sh + [ -f Proofs/Audit.lean.selftest.bak ] && mv -f Proofs/Audit.lean.selftest.bak Proofs/Audit.lean + return 0 +} +cleanup() { + restore + rm -f Proofs/Stray.lean Proofs/Stray.olean \ + Proofs/EvilSpec.lean Proofs/EvilSpec.olean Proofs/Audit.olean +} trap cleanup EXIT +backup() { cp -f check.sh check.sh.selftest.bak; cp -f Proofs/Audit.lean Proofs/Audit.lean.selftest.bak; } echo "check-selftest: attacking the gates" echo "====================================" @@ -30,76 +46,82 @@ if ./check.sh > /tmp/selftest-dead.out 2>&1; then echo "✗ ATTACK 1 SUCCEEDED: check.sh stayed green with a dead file"; exit 1 fi grep -q "DEAD FILE" /tmp/selftest-dead.out \ - || { echo "✗ ATTACK 1: failed, but not via the dead-file gate"; exit 1; } + || { echo "✗ ATTACK 1: failed, but not via the dead-file gate"; cat /tmp/selftest-dead.out; exit 1; } rm -f Proofs/Stray.lean Proofs/Stray.olean echo "✓ attack 1 rejected (dead-file gate works)" -# ── Attack 2: smuggled axiom ──────────────────────────────────────────────── +# ── Attack 2: smuggled disallowed axiom in a real cone ────────────────────── +# A new certificate whose cone genuinely contains `evil_ax`, declared as clean +# (kernel-3) in the expected table. Exact-equality must flag extra=[evil_ax]. +backup cat > Proofs/EvilSpec.lean <<'EOF' import Proofs.ChainSpec axiom evil_ax : True theorem evil_thm : True := evil_ax EOF python3 - <<'PY' +import re +# check.sh: add EvilSpec to PROOFS so Phase 2 builds it and the dead-file gate +# passes (inject right after the array's opening paren — no hard-coded contents). s = open("check.sh").read() -s = s.replace('PROOFS=(\n "ChainSpec"\n)', 'PROOFS=(\n "ChainSpec"\n "EvilSpec"\n)') -# Robust to the growing PROOFS / CERTS lists (do NOT hard-code their current -# contents — that rots the self-test as certificates are added): inject the -# evil entries right after each array's opening paren. -assert 'PROOFS=(\n' in s and 'CERTS=(\n' in s, "check.sh array shape changed" +assert 'PROOFS=(\n' in s, "check.sh PROOFS array shape changed" s = s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilSpec"\n', 1) -s = s.replace('CERTS=(\n', 'CERTS=(\n "evil_thm"\n', 1) -assert '{ echo "import Proofs.ChainSpec"' in s, "check.sh audit import shape changed" -s = s.replace('{ echo "import Proofs.ChainSpec"', - '{ echo "import Proofs.EvilSpec"; echo "import Proofs.ChainSpec"', 1) -open("check-evil-tmp.sh","w").write(s) +open("check.sh","w").write(s) +# Audit.lean: import EvilSpec and claim evil_thm is kernel-3 clean. +a = open("Proofs/Audit.lean").read() +assert 'import Proofs.ApexSpec' in a, "Audit.lean import shape changed" +a = a.replace('import Proofs.ApexSpec', 'import Proofs.ApexSpec\nimport Proofs.EvilSpec', 1) +assert 'def expectedCones : List (Name × List Name) :=' in a and ' [ (' in a, "Audit.lean table shape changed" +a = a.replace(' [ (', ' [ (`evil_thm, kernel3),\n (', 1) +open("Proofs/Audit.lean","w").write(a) PY -chmod +x check-evil-tmp.sh -if ./check-evil-tmp.sh > /tmp/selftest-evil.out 2>&1; then - echo "✗ ATTACK 2 SUCCEEDED: audit passed a smuggled axiom"; exit 1 +if ./check.sh > /tmp/selftest-evil.out 2>&1; then + echo "✗ ATTACK 2 SUCCEEDED: audit passed a smuggled disallowed axiom"; exit 1 fi -grep -q "DISALLOWED" /tmp/selftest-evil.out \ - || { echo "✗ ATTACK 2: failed, but not via the axiom gate"; exit 1; } -rm -f Proofs/EvilSpec.lean Proofs/EvilSpec.olean check-evil-tmp.sh -echo "✓ attack 2 rejected (axiom gate works)" +grep -q "AUDIT FAILED" /tmp/selftest-evil.out \ + || { echo "✗ ATTACK 2: failed, but not via the axiom audit"; cat /tmp/selftest-evil.out; exit 1; } +grep -q "evil_ax" /tmp/selftest-evil.out \ + || { echo "✗ ATTACK 2: rejected, but the audit did not name the smuggled axiom"; cat /tmp/selftest-evil.out; exit 1; } +restore; rm -f Proofs/EvilSpec.lean Proofs/EvilSpec.olean Proofs/Audit.olean +echo "✓ attack 2 rejected (extra-axiom detection works — evil_ax named)" -# ── Attack 3: smuggled axiom on a WRAPPED cone (the fail-open exploit) ─────── -# evil_wrapped_thm bundles a disallowed axiom with the apex theorem, so its cone -# is 9 axioms and WRAPS across physical lines with review_evil_ax on a -# continuation line — exactly what the old single-line parser missed. -cat > Proofs/EvilWrapSpec.lean <<'EOF' -import Proofs.ApexSpec -open Aeneas Aeneas.Std Result -open fips205 -axiom review_evil_ax : True -theorem evil_wrapped_thm - (mprime : Slice Std.U8) - (sig : types.SlhDsaSig 12#usize 7#usize 9#usize 14#usize 35#usize 16#usize) - (pk : types.SlhPublicKey 16#usize) : - True ∧ (verify_mono.slh_verify_128s mprime sig pk - = (do let root ← slhVerifyRoot 63#usize 30#usize mprime sig pk - ok (decide (root.val = pk.pk_root.val)))) := - ⟨review_evil_ax, slh_verify_128s_accepts_iff mprime sig pk⟩ -EOF +# ── Attack 3: dropped-oracle (subset would pass; exact must not) ───────────── +# Claim to_int_loop_eq depends on oracle.f. Its real cone is kernel-3 only, so +# the audit must report missing=[verify_mono.oracle.f]. +backup python3 - <<'PY' -s = open("check.sh").read() -assert 'PROOFS=(\n' in s and 'CERTS=(\n' in s, "check.sh array shape changed" -s = s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilWrapSpec"\n', 1) -s = s.replace('CERTS=(\n', 'CERTS=(\n "evil_wrapped_thm"\n', 1) -assert '{ echo "import Proofs.ChainSpec"' in s, "check.sh audit import shape changed" -s = s.replace('{ echo "import Proofs.ChainSpec"', - '{ echo "import Proofs.EvilWrapSpec"; echo "import Proofs.ChainSpec"', 1) -open("check-evilwrap-tmp.sh","w").write(s) +import re +a = open("Proofs/Audit.lean").read() +new, n = re.subn(r'(`fips205\.to_int_loop_eq,\s*)kernel3\)', r'\1kernel3 ++ [oracleF])', a) +assert n == 1, f"expected exactly one to_int table entry, patched {n}" +open("Proofs/Audit.lean","w").write(new) PY -chmod +x check-evilwrap-tmp.sh -if ./check-evilwrap-tmp.sh > /tmp/selftest-evilwrap.out 2>&1; then - echo "✗ ATTACK 3 SUCCEEDED: audit passed a smuggled axiom on a WRAPPED cone (fail-open!)"; exit 1 +if ./check.sh > /tmp/selftest-drop.out 2>&1; then + echo "✗ ATTACK 3 SUCCEEDED: audit passed a certificate missing a claimed oracle (subset hole!)"; exit 1 fi -grep -q "DISALLOWED" /tmp/selftest-evilwrap.out \ - || { echo "✗ ATTACK 3: failed, but not via the axiom gate (wrapped-cone parse?)"; exit 1; } -grep -q "review_evil_ax" /tmp/selftest-evilwrap.out \ - || { echo "✗ ATTACK 3: rejected, but the audit did not name the continuation-line axiom"; exit 1; } -echo "✓ attack 3 rejected (wrapped-cone axiom gate works — the continuation-line axiom was seen)" +grep -q "AUDIT FAILED" /tmp/selftest-drop.out \ + || { echo "✗ ATTACK 3: failed, but not via the axiom audit"; cat /tmp/selftest-drop.out; exit 1; } +grep -q "missing=\[verify_mono.oracle.f\]" /tmp/selftest-drop.out \ + || { echo "✗ ATTACK 3: rejected, but not by naming the missing oracle (exact-cone not enforced?)"; cat /tmp/selftest-drop.out; exit 1; } +restore; rm -f Proofs/Audit.olean +echo "✓ attack 3 rejected (missing-oracle detection works — exact cone enforced, not subset)" + +# ── Attack 4: vanished certificate (collectAxioms-returns-[] trap) ────────── +backup +python3 - <<'PY' +a = open("Proofs/Audit.lean").read() +assert a.count('`fips205.chain_free_loop_eq') >= 1 +a = a.replace('`fips205.chain_free_loop_eq,', '`fips205.chain_free_loop_eq_VANISHED,', 1) +open("Proofs/Audit.lean","w").write(a) +PY +if ./check.sh > /tmp/selftest-vanish.out 2>&1; then + echo "✗ ATTACK 4 SUCCEEDED: audit stayed green for a non-existent certificate (fail-open!)"; exit 1 +fi +grep -q "NOT FOUND" /tmp/selftest-vanish.out \ + || { echo "✗ ATTACK 4: failed, but not via the existence check"; cat /tmp/selftest-vanish.out; exit 1; } +restore; rm -f Proofs/Audit.olean +echo "✓ attack 4 rejected (existence check works — a vanished cert cannot pass as 0-axiom)" echo -echo "SELFTEST GREEN: all three gates genuinely reject their attacks." +echo "SELFTEST GREEN: the audit genuinely rejects extra axioms, dropped oracles," +echo "vanished certificates, and dead proof files." diff --git a/verification/check.sh b/verification/check.sh index 4ef6d44..7731323 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -5,9 +5,12 @@ # # Phase 1 — compile the extracted Lean model (gen/SlhVerify). # Phase 2 — compile the proof files (Proofs/). -# Phase 3 — axiom audit: every certificate's #print axioms cone must be a -# subset of {propext, Classical.choice, Quot.sound} plus the five -# SHA-2 hash oracles (the documented boundary) — nothing else. +# Phase 3 — axiom audit, performed INSIDE Lean (Proofs/Audit.lean): each +# certificate's cone, read from the kernel via `collectAxioms`, must +# EQUAL its expected set EXACTLY — kernel-3 plus only the named SHA-2 +# oracles. No text parsing (round-2 review closed that class of bug); +# any extra, any missing, a renamed/deleted cert, or an axiom/opaque +# sham is a Lean elaboration error → non-zero exit → fail-closed. set -euo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" @@ -49,9 +52,6 @@ CERTS=( "fips205.base2b_outer_loop_eq" "fips205.slh_verify_128s_accepts_iff" ) -ORACLES="verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.t_l, verify_mono.oracle.t_len, verify_mono.oracle.h_msg" -ALLOWED="[propext, Classical.choice, Quot.sound, ${ORACLES}]" - echo "fips205-slhdsa-verified — check" echo "===============================" @@ -74,49 +74,30 @@ lake env bash -c " compile() { echo \" · \$1\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' \"Proofs/\${1}.lean\" >/dev/null || { echo \"FAIL: Proofs/\$1\"; exit 1; }; } for m in ${PROOFS[*]}; do compile \"\$m\"; done # no dead proof files: everything under Proofs/ must be in the manifest + # (PROOFS) or be the audit driver (Audit, compiled in Phase 3). for f in Proofs/*.lean; do b=\$(basename \"\$f\" .lean) - case \" ${PROOFS[*]} \" in *\" \$b \"*) ;; *) echo \"DEAD FILE: Proofs/\$b.lean not in manifest\"; exit 1 ;; esac + case \" ${PROOFS[*]} Audit \" in *\" \$b \"*) ;; *) echo \"DEAD FILE: Proofs/\$b.lean not in manifest\"; exit 1 ;; esac done " -# ── Phase 3: axiom audit ──────────────────────────────────────────────────── -echo "=== Phase 3: axiom audit (cone ⊆ kernel-3 + 5 oracles) ===" +# ── Phase 3: axiom audit (exact cone per certificate, inside Lean) ─────────── +echo "=== Phase 3: axiom audit (exact cone per certificate — inside Lean) ===" cd "$AENEAS_LEAN" -AUD="$HERE/Proofs/.audit.lean" -{ echo "import Proofs.ChainSpec"; echo "import Proofs.WotsSpec" - echo "import Proofs.XmssSpec"; echo "import Proofs.HtSpec" - echo "import Proofs.ForsInnerSpec"; echo "import Proofs.ForsOuterSpec"; echo "import Proofs.InputPrepSpec"; echo "import Proofs.ApexSpec" - for c in "${CERTS[@]}"; do echo "#print axioms $c"; done -} > "$AUD" -OUT=$(lake env bash -c "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' 'Proofs/.audit.lean'" 2>&1) -rm -f "$AUD" -# CRITICAL: Lean WRAPS long axiom cones across physical lines. A per-line parse -# silently drops continuation-line axioms (fail-OPEN — external review round 1, -# 2026-07-24, demonstrated a smuggled axiom on line 2 passing). FLATTEN the whole -# report first, then extract each cert's complete bracketed cone with a -# literal-string (regex-safe) scan and subset-check it. Missing/empty report => -# fail-CLOSED. -FLAT=$(echo "$OUT" | tr '\n' ' ' | tr -s ' ') -fail=0 -for c in "${CERTS[@]}"; do - marker="'$c' depends on axioms: [" - if ! grep -qF "$marker" <<<"$FLAT"; then - echo " ✗ $c — no axiom report (fail-closed)"; fail=1; continue - fi - # full cone between this cert's '[' and the next ']' (literal index, not regex) - cone=$(awk -v m="$marker" '{ i=index($0,m); if(i>0){ r=substr($0,i+length(m)); j=index(r,"]"); if(j>0) print substr(r,1,j-1) } }' <<<"$FLAT") - bad=$(echo "$cone" | tr ',' '\n' | sed 's/^ *//;s/ *$//' | while read -r ax; do - [ -z "$ax" ] && continue - case " propext Classical.choice Quot.sound verify_mono.oracle.f verify_mono.oracle.h verify_mono.oracle.t_l verify_mono.oracle.t_len verify_mono.oracle.h_msg " in - *" $ax "*) ;; *) echo "$ax" ;; - esac - done) - if [ -n "$bad" ]; then echo " ✗ $c — DISALLOWED axioms: $(echo $bad | tr '\n' ' ')"; fail=1 - else echo " ✓ $c cone ⊆ allowed ($(echo "$cone" | tr ',' '\n' | grep -c .) axioms audited)"; fi -done -[ "$fail" = 0 ] || { echo "AXIOM AUDIT FAILED"; exit 1; } +# Proofs/Audit.lean reads each cert's cone from the kernel (collectAxioms) and +# asserts SET EQUALITY against its expected boundary. Compiling it IS the audit: +# any mismatch throws → non-zero exit. We additionally require the explicit +# PASSED line, so a build that somehow exits 0 without running the audit still +# fails closed. +AUD_OUT=$(lake env bash -c "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' 'Proofs/Audit.lean'" 2>&1) || { + echo "$AUD_OUT" | sed 's/^/ /' + echo "AXIOM AUDIT FAILED (Audit.lean did not compile — cone mismatch, missing cert, or sham)"; exit 1; } +if ! grep -qF "exact-cone audit PASSED" <<<"$AUD_OUT"; then + echo "$AUD_OUT" | sed 's/^/ /' + echo "AXIOM AUDIT FAILED (no PASSED line — fail-closed)"; exit 1 +fi +echo " ✓ exact-cone audit PASSED: each of the ${#CERTS[@]} certificate cones == its expected boundary set" echo -echo "ALL GREEN — model compiles, proofs compile, every certificate cone is" -echo "the three kernel axioms plus (at most) the SHA-2 hash oracles." +echo "ALL GREEN — model compiles, proofs compile, and every certificate cone" +echo "equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles." echo "Certificates proven: ${CERTS[*]}" diff --git a/verification/extract.sh b/verification/extract.sh index 84b89cc..a0cffa7 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -9,20 +9,49 @@ # # Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean # +# REPRODUCIBILITY (external review round 2, 2026-07-24): this script now +# REFUSES to extract from a source tree that is not at the pinned commit or +# is dirty (a wrong/uncommitted source would silently produce a different +# model). The full pin set (source + charon + aeneas + lean + ocaml) is in +# verification/PROVENANCE.json; re-running this against the pinned tree +# reproduces gen/SlhVerify/{Types,Funs}.lean byte-identically. +# # HISTORY (gate-0 finding, resolved 2026-07-22): upstream models the hash # family as `crate::hashers::Hashers`, a struct of plain function pointers, -# which Aeneas cannot translate. The compat patch in fips205-source -# (>= 2d89ee3) provides the additive monomorphic verify_mono module whose -# hash suite is reached through named free functions — this script roots -# there, and charon + aeneas both exit 0. Regeneration is byte-identical -# (verified against the committed gen/ during the 2026-07-22 audit). +# which Aeneas cannot translate. The compat patch in fips205-source provides +# the additive monomorphic verify_mono module whose hash suite is reached +# through named free functions — this script roots there. # -# Usage: ./extract.sh +# Usage: ./extract.sh [PATH_TO_fips205-source] +# (default: ~/GitClone/FormalVerification/sources/fips205-source) +# Override the required commit only for a deliberate re-pin: +# EXPECTED_SRC_COMMIT= ./extract.sh [PATH] set -euo pipefail source ~/aeneas-toolchain/env.sh HERE="$(cd "$(dirname "$0")" && pwd)" -CRATE=~/GitClone/FormalVerification/sources/fips205-source +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}" + +# ── 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; } +GOT_COMMIT="$(git -C "$CRATE" rev-parse HEAD)" +if [ "$GOT_COMMIT" != "$EXPECTED_SRC_COMMIT" ]; then + echo "ERROR: source is at ${GOT_COMMIT:0:12}, but this repo is pinned to" >&2 + echo " ${EXPECTED_SRC_COMMIT:0:12}. Check out the pin, or set" >&2 + echo " EXPECTED_SRC_COMMIT= for a deliberate re-pin." >&2 + exit 3 +fi +if [ -n "$(git -C "$CRATE" status --porcelain)" ]; then + echo "ERROR: source tree at '$CRATE' is dirty. Extraction must run against" >&2 + echo " a clean, committed tree so the model is reproducible." >&2 + git -C "$CRATE" status --porcelain | sed 's/^/ /' >&2 + exit 4 +fi +echo "[0/2] provenance OK: fips205-source @ ${EXPECTED_SRC_COMMIT:0:12} (clean)" echo "[1/2] charon: Rust -> LLBC (monomorphic SHA2-128s verify cone;" echo " crate::verify_mono::oracle is the opaque SHA-2 boundary)"