From 45a2f65a2db50b911a706aca545233facbc729c8 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 27 Jul 2026 19:47:39 +0200 Subject: [PATCH] review round 4: bind the cert set, statements, and model bytes (F1/F2/F3) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The third reviewer demonstrated that the round-2 in-Lean exact-cone audit, though sound for LISTED certs, left three fail-opens OUTSIDE the cone check — and made check.sh print ALL GREEN over a repo proving False. All closed; no theorem, proof, or fold changed (the 11 cones are unchanged). F1 — the audited SET was unbound. Audit.lean now (a) enumerates EVERY theorem defined in the eight certificate modules and requires each cone ⊆ boundary, so an un-manifested `theorem _ : False := cheat _` fails regardless of naming (this is the exact exploit the reviewer used); and (b) prints a MANIFEST fingerprint over the whole committed manifest, which check.sh binds to — so deleting/swapping a cert row fails outside Lean too. F2 — only cones were bound, not statements. Each cert now also carries the structural fingerprint (Expr.hash) of its elaborated type; a statement gutted to a tautology of the same cone changes the fingerprint and fails. F3 — the gen/ model bytes were unbound. New check.sh Phase 0 sha256-pins all four gen/SlhVerify/*.lean (incl. the two hand-maintained *External files, now hashed in PROVENANCE.json) BEFORE compiling; a hand-edited model fails first. F4/F5 — docs. README cone diagram now roots honestly at slh_verify_internal and states the pure/prehash domain-separator byte, the ctx>255 check, M' assembly, and deserialization are ABOVE the root and uncovered (new TRUSTED-BASE item 10). The false "rules out a wrong ADRS field" claim is corrected in README + ChainSpec (a transliteration makes the field visible, not excluded). check-selftest.sh: eight attacks, all rejected (dead file; extra axiom; dropped oracle; vanished cert; un-manifested False theorem; gutted statement; hand-edited model; deleted manifest row). Full transcript + green check.sh in verification/RECORDED-RUN.md. Standing limit unchanged and disclosed: an audit cannot defend against an author who edits the manifest AND check.sh AND the proofs together; the consumer defense is the pinned commit reviewed at the pin. Co-Authored-By: Claude Opus 4.8 --- README.md | 24 +++- TRUSTED-BASE.md | 10 ++ verification/PROVENANCE.json | 9 +- verification/Proofs/Audit.lean | 153 ++++++++++++++++-------- verification/Proofs/ChainSpec.lean | 11 +- verification/RECORDED-RUN.md | 29 +++++ verification/check-selftest.sh | 186 +++++++++++++++++------------ verification/check.sh | 68 ++++++++--- 8 files changed, 336 insertions(+), 154 deletions(-) diff --git a/README.md b/README.md index 3947375..a5a38cc 100644 --- a/README.md +++ b/README.md @@ -62,7 +62,14 @@ The trust base and residual assumptions are stated in 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 monomorphic SHA2-128s `verify_mono` path — an - off-by-one loop bound, a wrong address field, and wrong threading. Its + off-by-one loop bound and wrong state threading. (It does **not** rule out + a wrong ADRS field: the reference fold is built from the same extracted + `set_hash_address` primitive the loop calls, so a wrong field would be + faithfully copied into the fold and the theorem would still hold. What the + certificate pins is what the extracted code does at each index, so a wrong + field is *visible* in the certificate, not *excluded* by it — the mapping + onto FIPS 205 Alg 5 is a human reading step, consistent with "the folds are + transliterations of the extracted loops" above.) 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 @@ -170,15 +177,24 @@ same boundary. ## Scope -**Verify path only.** The extraction cone, mirroring FIPS 205's own -algorithm tree: +**Verify path only, rooted at `slh_verify_internal`.** The extraction root +is `verify_mono::slh_verify_128s`, which is `slh_verify_internal_free(M′, sig, +pk)` — it takes the already-assembled message digest input **M′ as an +argument**. So the covered cone is: ``` -slh_verify -> slh_verify_internal +slh_verify_internal(M′, …) ← the extraction ROOT (M′ is an input) -> fors_pk_from_sig -> ht_verify -> xmss_pk_from_sig -> wots_pk_from_sig -> chain ``` +Everything **above** this root, in `slh_verify`/`verify` (`src/lib.rs`), is +OUT of scope and is stated as such in [TRUSTED-BASE.md](TRUSTED-BASE.md): M′ +assembly, the pure-vs-prehash **domain-separator byte** (`0u8` for `verify`, +`1u8` for `hash_verify` — the entire cross-variant separation), the +`ctx.len() > 255` check, and signature/public-key deserialization. A reader +must NOT read `slh_verify -> slh_verify_internal` as "the top of the verify +path is covered" — it is not; the top-of-path input handling is trusted base. 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 diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 7c4db1e..5e37e10 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -45,3 +45,13 @@ proceeds and is part of every claim. `verify_mono` facade. The bridge to upstream's generic `pk.verify()` is the finite in-snapshot differential test, not a machine-checked refinement. +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 + `slh_verify`/`verify` (`src/lib.rs`) that runs *before* this root is NOT + covered by any certificate: the assembly of M′; the pure-vs-prehash + **domain-separator byte** (`0u8` for `verify` vs `1u8` for `hash_verify` + — the whole cross-variant domain separation); the FIPS-205 `ctx.len() > + 255` bound; and signature/public-key deserialization. The certificates + say nothing about this input handling — a defect there (e.g. a wrong + separator byte) would be outside every proof. diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json index 9cf7e79..3cfa38f 100644 --- a/verification/PROVENANCE.json +++ b/verification/PROVENANCE.json @@ -32,5 +32,12 @@ "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" + "model_integrity_sha256": { + "_comment": "All four Lean model files check.sh Phase 0 pins before compiling anything — 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", + "gen/SlhVerify/FunsExternal.lean": "73fa2a7d14b35bb6b6746534e88cba527d0e17f154f7a7d841a9c519befeea47", + "gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384", + "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f" + }, + "audit_gate": "verification/Proofs/Audit.lean — in-Lean audit (round 4): per-certificate exact cone equality (collectAxioms) + elaborated-statement fingerprint (Expr.hash) + full enumeration of every theorem in the eight certificate modules (each cone ⊆ boundary, so an un-manifested theorem cannot smuggle an axiom) + a manifest fingerprint check.sh binds to. Fail-closed; adversarially exercised by check-selftest.sh (attacks 1–6). check.sh Phase 0 pins the model bytes to model_integrity_sha256 above." } diff --git a/verification/Proofs/Audit.lean b/verification/Proofs/Audit.lean index 69f30aa..09772c8 100644 --- a/verification/Proofs/Audit.lean +++ b/verification/Proofs/Audit.lean @@ -1,23 +1,37 @@ /- ────────────────────────────────────────────────────────────────────────────── - Proofs/Audit.lean — the axiom-cone audit, performed INSIDE Lean. + Proofs/Audit.lean — the axiom-cone + statement + coverage audit, in 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. + History: round 2 moved the axiom check inside Lean (collectAxioms, exact + per-cert set equality). Round 4 (third reviewer, 2026-07-24) demonstrated + that exact-cone-per-cert, while sound FOR LISTED certs, left three gaps + OUTSIDE the cone check — all fail-open: + F1 the audited SET was unbound: deleting a manifest row silently drops a + cert, and adding an un-manifested theorem (e.g. `: False := cheat _`) + was never looked at → the repo could prove False under ALL GREEN. + F2 only cones were bound, never STATEMENTS: a certificate whose type was + replaced by a tautology of the same cone passed green. + F3 (handled in check.sh) the gen/ model bytes were unbound to provenance. - `collectAxioms` reads the kernel's own axiom set for each certificate. We - assert, for every one of the eleven: + This file now closes F1 and F2 with three layers: + (1) NAMED CERTS — each of the eleven: exists ∧ is a `theorem` ∧ cone == + its expected set EXACTLY ∧ its elaborated-type structural fingerprint + (`Expr.hash`) == the committed value. A gutted statement changes the + fingerprint → fail (F2). + (2) FULL-MODULE ENUMERATION — EVERY theorem defined in the eight + certificate modules must have a cone ⊆ the allowed boundary. An + un-manifested `: False := cheat _` has cone {cheat} ⊄ boundary → fail, + whether or not anyone "listed" it (F1, the dangerous half). + (3) MANIFEST FINGERPRINT — a hash over the whole committed manifest + (names + cones + type fingerprints) is printed; check.sh binds to the + exact committed value, so deleting/swapping a row, or editing a cone or + a fingerprint, changes it and fails the build outside Lean too (F1, the + set-binding half). - · 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. + Any mismatch is a `throwError` → non-zero `lean` exit. Nothing fails open for + a listed cert, an unlisted theorem, a gutted statement, or a dropped oracle. + The standing limit (unchanged, disclosed): an audit cannot defend against an + author who edits the manifest AND check.sh AND the proofs together; the + consumer defense is the pinned commit reviewed at the pin. ────────────────────────────────────────────────────────────────────────────── -/ import Proofs.ChainSpec import Proofs.WotsSpec @@ -31,65 +45,104 @@ open Lean Elab Command namespace SlhVerify.Audit -/-- Lean's three kernel axioms — permitted in every cone. -/ +/-- Lean's three kernel axioms. -/ 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. -/ +/-- The only axioms permitted in ANY cone in the certificate modules: kernel-3 + plus the five SHA-2 oracles. -/ 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]) ] +/-- The eight certificate-bearing proof modules. Every `theorem` defined in + these must have a cone ⊆ allowedBoundary (layer 2). -/ +def certModules : List Name := + [`Proofs.ChainSpec, `Proofs.WotsSpec, `Proofs.XmssSpec, `Proofs.HtSpec, + `Proofs.ForsInnerSpec, `Proofs.ForsOuterSpec, `Proofs.InputPrepSpec, `Proofs.ApexSpec] + +/-- THE COMMITTED MANIFEST: for each certificate, its exact expected cone and + the structural fingerprint (`Expr.hash`) of its elaborated statement. Ground + truth captured 2026-07-27 via Probe.lean; cross-checked against the round-1/2 + cone reconstructions. Changing a proof (cone) OR a statement (fingerprint) + breaks the audit; adding/removing a row changes the manifest fingerprint that + check.sh binds to. -/ +def manifest : List (Name × List Name × UInt64) := + [ (`fips205.chain_free_loop_eq, kernel3 ++ [oracleF], 2535491171), + (`fips205.wots_loop1_eq, kernel3 ++ [oracleF], 2968777228), + (`fips205.xmss_loop_eq, kernel3 ++ [oracleH], 763493610), + (`fips205.ht_loop_eq, kernel3 ++ [oracleF, oracleH, oracleTL], 1071622136), + (`fips205.fors_inner_loop_eq, kernel3 ++ [oracleH], 2102092697), + (`fips205.fors_outer_loop_eq, kernel3 ++ [oracleF, oracleH], 2749583942), + (`fips205.to_int_loop_eq, kernel3, 3797401829), + (`fips205.to_byte_loop_eq, kernel3, 3618049364), + (`fips205.wots_csum_loop_eq, kernel3, 4245103433), + (`fips205.base2b_outer_loop_eq, kernel3, 324621577), + (`fips205.slh_verify_128s_accepts_iff, kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg], 2489587792) ] + +/-- Canonical serialization of the committed manifest → one hash. check.sh binds + to the printed value, so any row add/remove/edit, cone change, or fingerprint + change flips it and fails the build. -/ +def manifestFingerprint : UInt64 := + let sortName (l : List Name) : List Name := + ((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName) + let ser := String.intercalate ";" (manifest.map (fun (n, cone, fp) => + s!"{n}|{String.intercalate "," ((sortName cone).map toString)}|{fp}")) + String.hash ser 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 + -- (0) the manifest's expected cones may reference nothing outside the boundary + for (cert, cone, _) in manifest do + for a in cone do + unless allowedBoundary.contains a do + throwError "manifest references non-boundary axiom {a} for {cert}" + -- (1) NAMED CERTS: exists ∧ theorem ∧ exact cone ∧ statement fingerprint + for (cert, expected, expFp) in manifest do match env.find? cert with | none => errs := errs.push s!"{cert}: NOT FOUND (renamed/deleted?)" - | some (.thmInfo _) => + | some (.thmInfo ci) => 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}" + errs := errs.push s!"{cert}: cone extra={extras} missing={missing}" + unless ci.type.hash == expFp do + errs := errs.push s!"{cert}: STATEMENT fingerprint {ci.type.hash} ≠ committed {expFp} (statement changed?)" | 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" + -- (2) FULL-MODULE ENUMERATION: every theorem in a cert module has a clean cone. + -- This is the layer that stops an un-manifested `: False := cheat _`. + let manifestNames := manifest.map (·.1) + let mut nModuleThms := 0 + let mut certsSeen : Array Name := #[] + for (nm, ci) in env.constants.toList do + match ci with + | .thmInfo _ => + match env.getModuleIdxFor? nm with + | some idx => + if certModules.contains env.header.moduleNames[idx.toNat]! then + nModuleThms := nModuleThms + 1 + if manifestNames.contains nm then certsSeen := certsSeen.push nm + let cone := (← collectAxioms nm).toList + let bad := cone.filter (fun a => !allowedBoundary.contains a) + unless bad.isEmpty do + errs := errs.push s!"UN-AUDITED theorem {nm} (module {env.header.moduleNames[idx.toNat]!}) has disallowed axioms {bad}" + | none => pure () + | _ => pure () + -- every manifest cert must actually be a theorem found in a cert module + for cert in manifestNames do + unless certsSeen.contains cert do + errs := errs.push s!"manifest cert {cert} not found as a theorem in any certificate module" 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)" + throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}" + logInfo s!"exact-cone audit PASSED: {manifest.length} certificates (cones + statement fingerprints), {nModuleThms} module theorems enumerated clean; MANIFEST-FINGERPRINT: {manifestFingerprint}" end SlhVerify.Audit diff --git a/verification/Proofs/ChainSpec.lean b/verification/Proofs/ChainSpec.lean index 8e59bb1..488a775 100644 --- a/verification/Proofs/ChainSpec.lean +++ b/verification/Proofs/ChainSpec.lean @@ -4,10 +4,13 @@ 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 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). + deployed generic verifier) — an off-by-one loop bound and wrong state + threading. It does NOT rule out a wrong ADRS field: `chainFoldN` calls the + same extracted `set_hash_address` the loop does, so a wrong field would be + copied into the fold and the theorem would still hold — the field is made + VISIBLE in the certificate (a transliteration), not excluded by it. 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). The proof: an induction on the step count. `chain_step` is one loop step = one fold step, proven by unfolding the Aeneas `loop` fixpoint one turn diff --git a/verification/RECORDED-RUN.md b/verification/RECORDED-RUN.md index 2699237..37998b6 100644 --- a/verification/RECORDED-RUN.md +++ b/verification/RECORDED-RUN.md @@ -158,3 +158,32 @@ Done. Now run ./check.sh (Phase 1: the regenerated model must type-check). db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384 gen/SlhVerify/Types.lean 7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f gen/SlhVerify/Funs.lean ``` + +## Round-4 hardening (third reviewer, 2026-07-27) + +The third reviewer demonstrated three fail-opens OUTSIDE the cone check +(F1 unbound cert set / un-manifested theorem; F2 statements unbound; F3 +model bytes unbound). All fixed. check.sh green with the hardened gate, +and the adversarial self-test now rejects eight attacks including the two +the reviewer used to make the button green over a repo proving False: + +``` +check.sh: ALL GREEN — MANIFEST-FINGERPRINT: 13660980750615609973 +Phase 0 model-byte integrity: 4/4 gen files match PROVENANCE.json +Phase 3 audit: 11 certs (cones + statement fingerprints), 196 module theorems enumerated clean + +check-selftest: attacking the gates +==================================== +✓ attack 1 rejected (dead-file gate) +✓ attack 2 rejected (extra-axiom detection — evil_ax named) +✓ attack 3 rejected (missing-oracle detection — exact cone, not subset) +✓ attack 4 rejected (existence check — vanished cert cannot pass as 0-axiom) +✓ attack 5 rejected (module enumeration — an un-manifested False theorem cannot pass) +✓ attack 6 rejected (statement fingerprint — a gutted statement of the same cone cannot pass) +✓ attack 7 rejected (Phase 0 model-byte integrity — a hand-edited model cannot compile) +✓ attack 8 rejected (manifest fingerprint — a silently-dropped cert cannot pass) + +SELFTEST GREEN: the gate rejects dead files, extra axioms, dropped oracles, +vanished certs, un-manifested False theorems, gutted statements, hand-edited +models, and deleted manifest rows. +``` diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index 9939756..1004b39 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -1,127 +1,155 @@ #!/usr/bin/env bash # 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: +# cannot fail is theater). The audit runs INSIDE Lean (Proofs/Audit.lean); the +# model bytes are pinned in Phase 0; the certificate SET and each STATEMENT are +# bound by a manifest fingerprint. 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 — 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. +# 1. DEAD FILE — a stray Proofs/*.lean not in the manifest. +# 2. SMUGGLED AXIOM — a listed cert whose real cone contains a disallowed +# axiom; exact-equality reports extra=[...]. +# 3. DROPPED ORACLE — a listed cert whose expected cone claims an oracle its +# proof does not use; exact-equality reports missing=[...] +# (a subset checker would pass this). +# 4. VANISHED CERT — a manifest name that no longer resolves; the explicit +# existence check reports NOT FOUND (collectAxioms would +# otherwise return [] and pass). +# 5. UN-AUDITED FALSE — round-4 F1: an UN-manifested `theorem … : False := …` +# added to a certificate module. The full-module +# enumeration must flag its disallowed cone. (This is the +# attack that made the pre-round-4 button green over a +# repo proving False.) +# 6. GUTTED STATEMENT — round-4 F2: a certificate's statement replaced by a +# tautology of the SAME cone. The statement fingerprint +# must differ from the committed manifest value. +# 7. MODEL TAMPER — round-4 F3: a hand-edit of a gen/ model file. Phase 0 +# must reject it before anything is compiled. +# 8. DELETED ROW — round-4 F1 (set half): a manifest row removed. Audit +# still compiles, but the printed MANIFEST-FINGERPRINT +# changes and check.sh's committed binding must reject it. # -# 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 +# Green here means the gate genuinely rejects all eight. Self-cleaning: every +# file a step tampers is saved and restored around that step. +set -uo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" cd "$HERE" -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 -} +TOUCHED=() +save() { for f in "$@"; do cp -f "$f" "$f.sfbak"; TOUCHED+=("$f"); done; } +restore() { for f in "${TOUCHED[@]}"; do [ -f "$f.sfbak" ] && mv -f "$f.sfbak" "$f"; done; TOUCHED=(); } cleanup() { restore - rm -f Proofs/Stray.lean Proofs/Stray.olean \ - Proofs/EvilSpec.lean Proofs/EvilSpec.olean Proofs/Audit.olean + rm -f Proofs/Stray.lean Proofs/Stray.olean Proofs/EvilSpec.lean Proofs/EvilSpec.olean \ + Proofs/Audit.olean Proofs/ChainSpec.olean *.sfbak Proofs/*.sfbak gen/SlhVerify/*.sfbak } 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 "====================================" # ── Attack 1: dead file ───────────────────────────────────────────────────── echo "-- stray" > Proofs/Stray.lean -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"; cat /tmp/selftest-dead.out; exit 1; } +if ./check.sh > /tmp/sf1.out 2>&1; then echo "✗ ATTACK 1 SUCCEEDED (dead file stayed green)"; exit 1; fi +grep -q "DEAD FILE" /tmp/sf1.out || { echo "✗ ATTACK 1: failed, not via dead-file gate"; cat /tmp/sf1.out; exit 1; } rm -f Proofs/Stray.lean Proofs/Stray.olean -echo "✓ attack 1 rejected (dead-file gate works)" +echo "✓ attack 1 rejected (dead-file gate)" # ── 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 +save check.sh Proofs/Audit.lean 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() -assert 'PROOFS=(\n' in s, "check.sh PROOFS array shape changed" -s = s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilSpec"\n', 1) -open("check.sh","w").write(s) -# Audit.lean: import EvilSpec and claim evil_thm is kernel-3 clean. +assert 'PROOFS=(\n' in s +open("check.sh","w").write(s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilSpec"\n', 1)) a = open("Proofs/Audit.lean").read() -assert 'import Proofs.ApexSpec' in a, "Audit.lean import shape changed" +assert 'import Proofs.ApexSpec' in a and ' [ (' in a 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) +a = a.replace(' [ (', ' [ (`evil_thm, kernel3, 0),\n (', 1) open("Proofs/Audit.lean","w").write(a) PY -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 "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; } +if ./check.sh > /tmp/sf2.out 2>&1; then echo "✗ ATTACK 2 SUCCEEDED (smuggled axiom)"; exit 1; fi +grep -q "evil_ax" /tmp/sf2.out || { echo "✗ ATTACK 2: rejected but evil_ax not named"; cat /tmp/sf2.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)" +echo "✓ attack 2 rejected (extra-axiom detection — evil_ax named)" # ── 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 +save Proofs/Audit.lean python3 - <<'PY' 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}" +new, n = re.subn(r'(`fips205\.to_int_loop_eq,\s*)kernel3(,\s*\d+\))', r'\1kernel3 ++ [oracleF]\2', a) +assert n == 1, f"patched {n}" open("Proofs/Audit.lean","w").write(new) PY -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 "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; } +if ./check.sh > /tmp/sf3.out 2>&1; then echo "✗ ATTACK 3 SUCCEEDED (dropped oracle, subset hole)"; exit 1; fi +grep -q "missing=\[verify_mono.oracle.f\]" /tmp/sf3.out || { echo "✗ ATTACK 3: rejected but missing oracle not named"; cat /tmp/sf3.out; exit 1; } restore; rm -f Proofs/Audit.olean -echo "✓ attack 3 rejected (missing-oracle detection works — exact cone enforced, not subset)" +echo "✓ attack 3 rejected (missing-oracle detection — exact cone, not subset)" -# ── Attack 4: vanished certificate (collectAxioms-returns-[] trap) ────────── -backup +# ── Attack 4: vanished certificate ────────────────────────────────────────── +save Proofs/Audit.lean 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) +open("Proofs/Audit.lean","w").write(a.replace('`fips205.chain_free_loop_eq,', '`fips205.chain_free_loop_eq_VANISHED,', 1)) 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; } +if ./check.sh > /tmp/sf4.out 2>&1; then echo "✗ ATTACK 4 SUCCEEDED (vanished cert)"; exit 1; fi +grep -q "NOT FOUND" /tmp/sf4.out || { echo "✗ ATTACK 4: rejected but not via existence check"; cat /tmp/sf4.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 "✓ attack 4 rejected (existence check — vanished cert cannot pass as 0-axiom)" + +# ── Attack 5: un-manifested theorem proving False (round-4 F1, the big one) ── +save Proofs/ChainSpec.lean +printf '\n-- SELFTEST ATTACK 5 (round-4 F1): an un-manifested cert proving False.\naxiom cheat : ∀ (P : Prop), P\ntheorem repo_proves_false : False := cheat _\n' >> Proofs/ChainSpec.lean +if ./check.sh > /tmp/sf5.out 2>&1; then echo "✗ ATTACK 5 SUCCEEDED: check.sh GREEN over a repo proving False!"; exit 1; fi +grep -q "repo_proves_false" /tmp/sf5.out || { echo "✗ ATTACK 5: rejected but not via the module enumeration"; cat /tmp/sf5.out; exit 1; } +restore; rm -f Proofs/ChainSpec.olean Proofs/Audit.olean +echo "✓ attack 5 rejected (module enumeration — an un-manifested False theorem cannot pass)" + +# ── Attack 6: gutted statement, cone preserved (round-4 F2) ───────────────── +# Gut a LEAF certificate (to_byte_loop_eq — nothing depends on it, so Phase 2 +# still compiles and the fingerprint gate is what must bite). Replace its +# statement+proof with a kernel-3 tautology: same cone, different type. +save Proofs/InputPrepSpec.lean +python3 - <<'PY' +s = open("Proofs/InputPrepSpec.lean").read() +i = s.index("theorem to_byte_loop_eq (n : Std.U32) (k : Nat) :") +j = s.index("theorem hbody_cs", i) # the NEXT declaration (to_byte_loop_eq is a leaf) +gut = "theorem to_byte_loop_eq : (∀ p : Prop, p ∨ ¬p) := Classical.em\n\n" +open("Proofs/InputPrepSpec.lean","w").write(s[:i] + gut + s[j:]) +PY +if ./check.sh > /tmp/sf6.out 2>&1; then echo "✗ ATTACK 6 SUCCEEDED: gutted statement passed (cone preserved)"; exit 1; fi +grep -qi "fingerprint" /tmp/sf6.out || { echo "✗ ATTACK 6: rejected but not via the statement fingerprint"; cat /tmp/sf6.out; exit 1; } +restore; rm -f Proofs/InputPrepSpec.olean Proofs/Audit.olean +echo "✓ attack 6 rejected (statement fingerprint — a gutted statement of the same cone cannot pass)" + +# ── Attack 7: hand-edited model file (round-4 F3) ─────────────────────────── +save gen/SlhVerify/Funs.lean +printf '\n-- SELFTEST ATTACK 7 (round-4 F3): hand-edited model.\n' >> gen/SlhVerify/Funs.lean +if ./check.sh > /tmp/sf7.out 2>&1; then echo "✗ ATTACK 7 SUCCEEDED: hand-edited model passed"; exit 1; fi +grep -q "MODEL INTEGRITY FAILED" /tmp/sf7.out || { echo "✗ ATTACK 7: rejected but not via Phase 0"; cat /tmp/sf7.out; exit 1; } +restore +echo "✓ attack 7 rejected (Phase 0 model-byte integrity — a hand-edited model cannot compile)" + +# ── Attack 8: deleted manifest row (round-4 F1 set half) ──────────────────── +save Proofs/Audit.lean +python3 - <<'PY' +import re +a = open("Proofs/Audit.lean").read() +new, n = re.subn(r'\n *\(`fips205\.to_int_loop_eq,[^\n]*\),', '', a) +assert n == 1, f"removed {n}" +open("Proofs/Audit.lean","w").write(new) +PY +if ./check.sh > /tmp/sf8.out 2>&1; then echo "✗ ATTACK 8 SUCCEEDED: a deleted manifest row passed (set unbound)"; exit 1; fi +grep -q "manifest fingerprint mismatch" /tmp/sf8.out || { echo "✗ ATTACK 8: rejected but not via the manifest-fingerprint binding"; cat /tmp/sf8.out; exit 1; } +restore; rm -f Proofs/Audit.olean +echo "✓ attack 8 rejected (manifest fingerprint — a silently-dropped cert cannot pass)" echo -echo "SELFTEST GREEN: the audit genuinely rejects extra axioms, dropped oracles," -echo "vanished certificates, and dead proof files." +echo "SELFTEST GREEN: the gate rejects dead files, extra axioms, dropped oracles," +echo "vanished certs, un-manifested False theorems, gutted statements, hand-edited" +echo "models, and deleted manifest rows." diff --git a/verification/check.sh b/verification/check.sh index 7731323..c53759c 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -3,14 +3,19 @@ # Green output == the full claim. This script is the ONLY source of the # word "proven" for this repo. # +# Phase 0 — model-byte integrity: every gen/SlhVerify/*.lean must sha256-match +# PROVENANCE.json (a hand-edited model fails BEFORE it is compiled; +# round-4 review F3). # Phase 1 — compile the extracted Lean model (gen/SlhVerify). # Phase 2 — compile the proof files (Proofs/). -# 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. +# Phase 3 — the in-Lean audit (Proofs/Audit.lean): each certificate's cone +# (via `collectAxioms`) must EQUAL its expected set exactly AND its +# statement fingerprint must match the committed manifest, EVERY +# theorem in the eight cert modules must have a cone within the +# boundary (so an un-manifested `: False := cheat _` cannot pass — +# round-4 F1), and this script binds to the printed MANIFEST +# fingerprint (round-4 F2/F1). Any mismatch → non-zero exit → +# fail-closed. No text parsing of axiom cones. set -euo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" @@ -55,6 +60,27 @@ CERTS=( echo "fips205-slhdsa-verified — check" echo "===============================" +# ── Phase 0: model-byte integrity (gen/ == PROVENANCE.json) ────────────────── +echo "=== Phase 0: model-byte integrity (gen/ pinned to PROVENANCE.json) ===" +python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "MODEL INTEGRITY FAILED (a gen/ file differs from PROVENANCE.json — hand-edited model?)"; exit 1; } +import json, sys, hashlib, os +prov = json.load(open(sys.argv[1])); here = sys.argv[2] +files = {k: v for k, v in prov.get("model_integrity_sha256", {}).items() if k.startswith("gen/")} +if not files: + print(" no model_integrity_sha256 in PROVENANCE.json (fail-closed)"); sys.exit(1) +bad = 0 +for rel, want in sorted(files.items()): + p = os.path.join(here, rel) + if not os.path.exists(p): + print(f" ✗ {rel} MISSING"); bad = 1; continue + got = hashlib.sha256(open(p, 'rb').read()).hexdigest() + if got != want: + print(f" ✗ {rel}: sha256 {got[:12]} ≠ pinned {want[:12]}"); bad = 1 + else: + print(f" ✓ {rel}") +sys.exit(1 if bad else 0) +PY + # ── Phase 1: model ────────────────────────────────────────────────────────── echo "=== Phase 1: compile the extracted model ===" cd "$AENEAS_LEAN" @@ -80,22 +106,32 @@ lake env bash -c " done " -# ── Phase 3: axiom audit (exact cone per certificate, inside Lean) ─────────── -echo "=== Phase 3: axiom audit (exact cone per certificate — inside Lean) ===" +# ── Phase 3: in-Lean audit (cones + statements + full-module enumeration) ──── +echo "=== Phase 3: in-Lean audit (cones + statement fingerprints + enumeration) ===" cd "$AENEAS_LEAN" -# 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. +# Proofs/Audit.lean checks: per-cert exact cone + statement fingerprint; every +# theorem in the eight cert modules has a clean cone (no un-manifested axiom +# smuggle); and it prints a MANIFEST-FINGERPRINT over the whole committed +# manifest. We bind to that EXACT fingerprint below, so deleting/swapping a cert +# row, or editing a cone or a statement fingerprint, changes the printed value +# and fails HERE even if Lean itself exits 0 (round-4 F1/F2 set+statement bind). +# To rotate the manifest deliberately, recompute it (compile Audit.lean, read the +# printed value) and update EXPECTED_MANIFEST_FP in the same reviewable commit. +EXPECTED_MANIFEST_FP="MANIFEST-FINGERPRINT: 13660980750615609973" 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; } + echo "AUDIT FAILED (Audit.lean did not compile — cone/statement mismatch, missing cert, sham, or un-audited theorem)"; 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 + echo "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" +if ! grep -qF "$EXPECTED_MANIFEST_FP" <<<"$AUD_OUT"; then + echo "$AUD_OUT" | sed 's/^/ /' + echo "AUDIT FAILED — manifest fingerprint mismatch." + echo " expected: $EXPECTED_MANIFEST_FP" + echo " the certificate set / a cone / a statement fingerprint changed without a reviewed manifest rotation."; exit 1 +fi +echo " ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1) ($EXPECTED_MANIFEST_FP)" echo echo "ALL GREEN — model compiles, proofs compile, and every certificate cone"