diff --git a/README.md b/README.md index a5a38cc..0900655 100644 --- a/README.md +++ b/README.md @@ -5,16 +5,35 @@ 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 2 applied) +## STATUS: eleven certificates over the extracted verify model (external review rounds 1–5 applied) -`verification/check.sh` is **green** (exit 0): the model compiles, the -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). +`verification/check.sh` is **green** (exit 0): the model compiles, the proofs +compile, and the audit passes. The audit runs **inside Lean** +(`verification/Proofs/Audit.lean`) and binds four things, each added because an +external reviewer *demonstrated* the button going green without it: + +- **axiom cones** — each certificate's cone is read from the kernel via + `collectAxioms` and must equal its expected set EXACTLY, so an added axiom + and a silently dropped oracle both fail (round 2 retired a text parser that + could fail open on an empty or truncated report); +- **coverage** — EVERY declaration in the eight certificate modules, of every + kind, and in `Audit.lean` itself, must stay inside the axiom boundary (rounds + 4–5: an un-manifested `theorem : False`, then a `def : False`, then one inside + the auditor, each passed a gate that checked only the listed certificates); +- **statements and specifications** — `check.sh` binds to the **SHA-256** of a + canonical block containing the policy constants, every certificate's + fully-elaborated statement, and every reference fold's fully-elaborated + *body*. Round 5 showed why the last part is essential: redefining a fold to + *be* the extracted loop left every earlier fingerprint bit-identical while the + certificate degenerated to "the loop equals the loop"; +- **bytes** — Phase 0 sha256-pins the four model files and the compiler harness + `lean-guard`, purges stale `.olean`s, and forbids stray `.lean` files, so the + verdict depends on committed bytes rather than build-directory state. + +What the button still does **not** bind is stated plainly in +[TRUSTED-BASE.md](TRUSTED-BASE.md) item 11 — `check.sh` itself, the toolchain +env, and `$AENEAS_HOME`. `verification/check-selftest.sh` runs the reviewers' +own exploits back against the gate; all are rejected. **What is actually established** — eleven Lean theorems about the Aeneas-generated model of the **monomorphic `verify_mono` compatibility @@ -50,6 +69,17 @@ cannot translate the deployed `Hashers` function-pointer struct): - **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. +- **Read every loop certificate as "visible", not "correct".** This follows + from the previous point but is worth stating on its own, because the per- + certificate descriptions below are easy to over-read. Each reference fold is + built from the *same* extracted primitives the loop calls, so any defect in + the extracted code is faithfully copied into the fold and the theorem still + holds. What is machine-checked is the loop's *scaffolding* — trip count, + index arithmetic, state threading, argument order, branch structure. Whether + the address schedule, the Merkle sibling order, or the FORS leaf index match + FIPS 205 is a **human reading step**, not a proved one. (Round-5 review makes + this sharper: the certificates are individually meaningful only to the extent + someone has read each fold against the standard — see TRUSTED-BASE item 12.) This is a real **intermediate** verification layer, not an end-to-end formal verification of the deployed verifier. After de-plumbing rounds 1+2 @@ -91,10 +121,16 @@ The trust base and residual assumptions are stated in `xmss_pk_from_sig_free_loop` equals the fold that, at step k, sets the tree height to k+1, tests bit k of the leaf index, and on an even bit halves the tree index and hashes H(node ∥ auth[k]), on an odd bit sets - the tree index to (i−1)/2 and hashes H(auth[k] ∥ node). This pins the + the tree index to (i−1)/2 and hashes H(auth[k] ∥ node). This makes the Merkle sibling ORDER (the even/odd rule), the tree-height/tree-index - address schedule, and the auth-path indexing — the heart of Merkle-path - verification. Cone: kernel three + `verify_mono.oracle.h` (the first + address schedule, and the auth-path indexing VISIBLE in the certificate — + **it does not establish them as correct.** `xmssFoldN` calls the same + extracted `set_tree_height`/`get_tree_index`/`oracle.h` that the loop body + calls, so a swapped sibling order would be copied into the fold and the + theorem would still hold. Read that as: the certificate pins what the + extracted code *does* at each step; whether that matches FIPS 205 + Algorithm 10 is a human reading step. Cone: kernel three + + `verify_mono.oracle.h` (the first certificate where H enters; F does not — the loop runs above the WOTS+ computation). @@ -103,8 +139,9 @@ The trust base and residual assumptions are stated in at layer j, splits the tree index (idx_leaf = idx_tree mod 2^h' by mask+cast, then idx_tree >>= h'), sets the layer address to j and the tree address to the shifted index, and recomputes the node through - `xmss_pk_from_sig` on the j-th XMSS signature. This pins the layer - schedule of hypertree verification; the final node = pk_root comparison + `xmss_pk_from_sig` on the j-th XMSS signature. This makes the layer + schedule of hypertree verification visible in the certificate (same + transliteration caveat as above); the final node = pk_root comparison sits one bind above, in `ht_verify_free`, and belongs to the apex composition. Cone: kernel three + `verify_mono.oracle.{f, h, t_l}` — the full WOTS+/XMSS machinery referenced through the fold, and nothing @@ -124,9 +161,9 @@ 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. - The inner one pins the auth-path Merkle fold for a single FORS tree (bit + The inner one equates the auth-path Merkle fold for a single FORS tree (bit source `indices[i] >> j`, `H` in the even/odd sibling order) — cone - kernel-3 + `oracle.h`. The outer one pins the K-tree fold: for each tree + kernel-3 + `oracle.h`. The outer one equates the K-tree fold: for each tree compute the leaf with `F` at index `(i< - s!"{n}|{String.intercalate "," ((sortName cone).map toString)}|{fp}")) - String.hash ser +/-- Deterministic name ordering for the canonical serialization. -/ +def sortNames (l : List Name) : List Name := + ((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName) + +/-- Whitespace-canonical: every whitespace run collapses to one space, so the + pretty-printer's line wrapping cannot perturb the digest. -/ +def normWs (s : String) : String := + (s.foldl (fun (acc : String × Bool) c => + let c := if c.isWhitespace then ' ' else c + if c == ' ' then (if acc.2 then acc else (acc.1.push ' ', true)) + else (acc.1.push c, false)) + ("", true)).1 + +/-- Is `n` a hand-written declaration living in one of the certificate modules? + These are the SPECIFICATION side — the folds the certificates are stated + against — as opposed to the extracted model in `gen/` (pinned by Phase 0). -/ +def isSpecConst (env : Environment) (n : Name) : Bool := + match env.getModuleIdxFor? n with + | some idx => certModules.contains env.header.moduleNames[idx.toNat]! + | none => false + +/-- Transitive closure over specification constants, starting from a + certificate's STATEMENT and following DEFINITION bodies (a theorem + contributes its statement only). This discovers the reference folds — and + any future one — automatically, so a new specification definition cannot be + introduced without moving the digest. -/ +partial def closureOf (env : Environment) (seen : NameSet) (work : List Name) : NameSet := + match work with + | [] => seen + | n :: rest => + if seen.contains n || !isSpecConst env n then closureOf env seen rest + else + let seen := seen.insert n + let more := match env.find? n with + | some (.defnInfo v) => v.value.getUsedConstants.toList ++ v.type.getUsedConstants.toList + | some ci => ci.type.getUsedConstants.toList + | none => [] + closureOf env seen (more ++ rest) + +/-- Fully-explicit (`pp.all`) rendering, whitespace-canonicalized. -/ +def ppAll (e : Expr) : CommandElabM String := do + let s ← Command.liftCoreM <| Meta.MetaM.run' <| + withOptions (fun o => o.setBool `pp.all true) do + return (← Meta.ppExpr e).pretty + return normWs s elab "auditCones" : command => do let env ← getEnv let mut errs : Array String := #[] - -- (0) the manifest's expected cones may reference nothing outside the boundary + + -- (0) the manifest's expected cones may reference nothing outside the policy. 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 + + -- (1) NAMED CERTS: exists ∧ is a theorem ∧ exact cone ∧ statement diagnostic. for (cert, expected, expFp) in manifest do match env.find? cert with - | none => errs := errs.push s!"{cert}: NOT FOUND (renamed/deleted?)" - | some (.thmInfo ci) => + | none => errs := errs.push s!"{cert}: NOT FOUND (renamed/deleted?)" + | 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) @@ -114,35 +161,79 @@ elab "auditCones" : command => do 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 _`. + | 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) ENUMERATION over EVERY declaration kind — not just theorems (a + -- `def : False` passed the round-4 gate) — in the eight certificate + -- modules, AND over this file's own declarations (module index is `none` + -- during its own elaboration), so the auditor is not exempt (round-5 R1). let manifestNames := manifest.map (·.1) - let mut nModuleThms := 0 + let mut nEnum := 0 let mut certsSeen : Array Name := #[] for (nm, ci) in env.constants.toList do - match ci with - | .thmInfo _ => + let scope : Option String := 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 m := env.header.moduleNames[idx.toNat]! + if certModules.contains m then some (toString m) else none + | none => if nm.isInternal then none else some "Proofs.Audit (this file)" + match scope with + | none => pure () + | some where_ => + nEnum := nEnum + 1 + if manifestNames.contains nm then certsSeen := certsSeen.push nm + match ci with + | .axiomInfo _ => + -- the five oracle axioms live in gen/ (Phase-0 pinned); an axiom + -- DECLARED inside an audited module is never acceptable. + errs := errs.push s!"AXIOM DECLARED in audited scope: {nm} ({where_})" + | _ => 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 + errs := errs.push s!"UN-AUDITED declaration {nm} ({where_}) has disallowed axioms {bad}" 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" + errs := errs.push s!"manifest cert {cert} not found in any certificate module" + unless errs.isEmpty do 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}" + + -- (3) CANONICAL BLOCK: policy + statements + specification bodies. check.sh + -- binds to the SHA-256 of everything between the markers. + let mut lines : Array String := #[] + lines := lines.push + s!"policy|allowedBoundary={String.intercalate "," ((sortNames allowedBoundary).map toString)}|certModules={String.intercalate "," ((sortNames certModules).map toString)}" + let mut specs : NameSet := {} + for (cert, cone, _) in manifest do + let ci := (env.find? cert).get! + specs := (closureOf env {} ci.type.getUsedConstants.toList).toList.foldl (·.insert ·) specs + lines := lines.push + s!"cert|{cert}|cone={String.intercalate "," ((sortNames cone).map toString)}|type={← ppAll ci.type}" + for nm in sortNames specs.toList do + match env.find? nm with + | none => errs := errs.push s!"specification constant vanished: {nm}" + | some ci => + let isProp ← Command.liftCoreM <| Meta.MetaM.run' <| Meta.isProp ci.type + -- proof irrelevance: a Prop-valued constant contributes its STATEMENT; + -- a data definition contributes its BODY — that is where fidelity lives. + if isProp then + lines := lines.push s!"spec|{nm}|prop|type={← ppAll ci.type}" + else + match ci with + | .defnInfo v => lines := lines.push s!"spec|{nm}|def|value={← ppAll v.value}" + | _ => lines := lines.push s!"spec|{nm}|other|type={← ppAll ci.type}" + unless errs.isEmpty do + throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}" + + logInfo ("AUDIT-MANIFEST-BEGIN\n" ++ String.intercalate "\n" lines.toList ++ "\nAUDIT-MANIFEST-END") + -- check.sh prints the certificate list it gets from HERE, not from a hand-kept + -- bash array (drill finding: the one authoritative claim string was the one + -- thing nothing bound — adding a name to it printed a cert that never existed). + logInfo s!"CERTIFICATES: {String.intercalate " " (manifestNames.map toString)}" + logInfo s!"exact-cone audit PASSED: {manifest.length} certificates (cones + statements), {specs.toList.length} specification constants pinned, {nEnum} declarations enumerated clean" end SlhVerify.Audit diff --git a/verification/RECORDED-RUN.md b/verification/RECORDED-RUN.md index 37998b6..a156549 100644 --- a/verification/RECORDED-RUN.md +++ b/verification/RECORDED-RUN.md @@ -142,14 +142,14 @@ Certificates proven: fips205.chain_free_loop_eq fips205.wots_loop1_eq fips205.xm hand-maintained TypesExternal.lean / FunsExternal.lean are NOT overwritten once they exist) [Info ] Imported: SlhVerify.llbc -[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋ Applied prepasses: [------------------------------------------------] 1/142 ⠋ Applied prepasses: [###---------------------------------------------] 11/142 ⠋ Applied prepasses: [#################-------------------------------] 52/142 ⠙ Applied prepasses: [########################################--------] 120/142 ⠙ Applied prepasses: [################################################] 142/142 ✔️ -[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋ Translated globals: [#################################################] 10/10 ✔️ -[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋ Translated opaque functions: [########################################] 76/76 ✔️ -[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋ Translated transparent functions: [-----------------------------------] 1/42 ⠙ Translated transparent functions: [#######----------------------------] 9/42 ⠹ Translated transparent functions: [########---------------------------] 10/42 ⠹ Translated transparent functions: [##########-------------------------] 12/42 ⠹ Translated transparent functions: [##########-------------------------] 13/42 ⠹ Translated transparent functions: [###########------------------------] 14/42 ⠸ Translated transparent functions: [############-----------------------] 15/42 ⠸ Translated transparent functions: [##############---------------------] 17/42 ⠸ Translated transparent functions: [###############--------------------] 19/42 ⠸ Translated transparent functions: [################-------------------] 20/42 ⠼ Translated transparent functions: [##################-----------------] 22/42 ⠼ Translated transparent functions: [####################---------------] 24/42 ⠼ Translated transparent functions: [#####################--------------] 26/42 ⠴ Translated transparent functions: [######################-------------] 27/42 ⠴ Translated transparent functions: [#######################------------] 28/42 ⠦ Translated transparent functions: [########################-----------] 29/42 ⠦ Translated transparent functions: [#########################----------] 30/42 ⠦ Translated transparent functions: [#########################----------] 31/42 ⠧ Translated transparent functions: [###########################--------] 33/42 ⠇ Translated transparent functions: [#############################------] 35/42 ⠏ Translated transparent functions: [##############################-----] 36/42 ⠏ Translated transparent functions: [##############################-----] 37/42 ⠋ Translated transparent functions: [###############################----] 38/42 ⠙ Translated transparent functions: [################################---] 39/42 ⠹ Translated transparent functions: [#################################--] 40/42 ⠸ Translated transparent functions: [##################################-] 41/42 ⠸ Translated transparent functions: [###################################] 42/42 ⠼ Translated transparent functions: [###################################] 42/42 ✔️ -[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋ Translated trait declarations: [##############------------------------] 13/33 ✔️ -[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋ Translated trait impls: [######################-----------------------] 25/50 ✔️ -[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋ Post-processed translated opaque functions: [-------------------------] 1/76 ⠙ Post-processed translated opaque functions: [#########################] 76/76 ✔️ -[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋ Post-processed translated transparent functions: [--------------------] 1/42 ⠙ Post-processed translated transparent functions: [###-----------------] 7/42 ⠙ Post-processed translated transparent functions: [####----------------] 9/42 ⠙ Post-processed translated transparent functions: [####----------------] 10/42 ⠹ Post-processed translated transparent functions: [#####---------------] 11/42 ⠹ Post-processed translated transparent functions: [#####---------------] 12/42 ⠸ Post-processed translated transparent functions: [######--------------] 13/42 ⠸ Post-processed translated transparent functions: [######--------------] 14/42 ⠸ Post-processed translated transparent functions: [#######-------------] 15/42 ⠼ Post-processed translated transparent functions: [#######-------------] 16/42 ⠼ Post-processed translated transparent functions: [########------------] 17/42 ⠼ Post-processed translated transparent functions: [#########-----------] 19/42 ⠴ Post-processed translated transparent functions: [#########-----------] 20/42 ⠴ Post-processed translated transparent functions: [##########----------] 21/42 ⠴ Post-processed translated transparent functions: [##########----------] 22/42 ⠦ Post-processed translated transparent functions: [##########----------] 23/42 ⠦ Post-processed translated transparent functions: [###########---------] 25/42 ⠦ Post-processed translated transparent functions: [############--------] 26/42 ⠧ Post-processed translated transparent functions: [############--------] 27/42 ⠧ Post-processed translated transparent functions: [#############-------] 28/42 ⠧ Post-processed translated transparent functions: [##############------] 30/42 ⠇ Post-processed translated transparent functions: [###############-----] 32/42 ⠇ Post-processed translated transparent functions: [###############-----] 33/42 ⠏ Post-processed translated transparent functions: [################----] 34/42 ⠏ Post-processed translated transparent functions: [#################---] 37/42 ⠋ Post-processed translated transparent functions: [##################--] 38/42 ⠋ Post-processed translated transparent functions: [##################--] 39/42 ⠙ Post-processed translated transparent functions: [###################-] 40/42 ⠹ Post-processed translated transparent functions: [###################-] 41/42 ⠸ Post-processed translated transparent functions: [####################] 42/42 ⠼ Post-processed translated transparent functions: [####################] 42/42 ✔️ +[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋ Applied prepasses: [------------------------------------------------] 1/142 ⠋ Applied prepasses: [###---------------------------------------------] 11/142 ⠋ Applied prepasses: [#################-------------------------------] 52/142 ⠙ Applied prepasses: [########################################--------] 120/142 ⠙ Applied prepasses: [################################################] 142/142 ✔️ +[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋ Translated globals: [#################################################] 10/10 ✔️ +[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋ Translated opaque functions: [########################################] 76/76 ✔️ +[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋ Translated transparent functions: [-----------------------------------] 1/42 ⠙ Translated transparent functions: [#######----------------------------] 9/42 ⠹ Translated transparent functions: [########---------------------------] 10/42 ⠹ Translated transparent functions: [##########-------------------------] 12/42 ⠹ Translated transparent functions: [##########-------------------------] 13/42 ⠹ Translated transparent functions: [###########------------------------] 14/42 ⠸ Translated transparent functions: [############-----------------------] 15/42 ⠸ Translated transparent functions: [##############---------------------] 17/42 ⠸ Translated transparent functions: [###############--------------------] 19/42 ⠸ Translated transparent functions: [################-------------------] 20/42 ⠼ Translated transparent functions: [##################-----------------] 22/42 ⠼ Translated transparent functions: [####################---------------] 24/42 ⠼ Translated transparent functions: [#####################--------------] 26/42 ⠴ Translated transparent functions: [######################-------------] 27/42 ⠴ Translated transparent functions: [#######################------------] 28/42 ⠦ Translated transparent functions: [########################-----------] 29/42 ⠦ Translated transparent functions: [#########################----------] 30/42 ⠦ Translated transparent functions: [#########################----------] 31/42 ⠧ Translated transparent functions: [###########################--------] 33/42 ⠇ Translated transparent functions: [#############################------] 35/42 ⠏ Translated transparent functions: [##############################-----] 36/42 ⠏ Translated transparent functions: [##############################-----] 37/42 ⠋ Translated transparent functions: [###############################----] 38/42 ⠙ Translated transparent functions: [################################---] 39/42 ⠹ Translated transparent functions: [#################################--] 40/42 ⠸ Translated transparent functions: [##################################-] 41/42 ⠸ Translated transparent functions: [###################################] 42/42 ⠼ Translated transparent functions: [###################################] 42/42 ✔️ +[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋ Translated trait declarations: [##############------------------------] 13/33 ✔️ +[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋ Translated trait impls: [######################-----------------------] 25/50 ✔️ +[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋ Post-processed translated opaque functions: [-------------------------] 1/76 ⠙ Post-processed translated opaque functions: [#########################] 76/76 ✔️ +[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋ Post-processed translated transparent functions: [--------------------] 1/42 ⠙ Post-processed translated transparent functions: [###-----------------] 7/42 ⠙ Post-processed translated transparent functions: [####----------------] 9/42 ⠙ Post-processed translated transparent functions: [####----------------] 10/42 ⠹ Post-processed translated transparent functions: [#####---------------] 11/42 ⠹ Post-processed translated transparent functions: [#####---------------] 12/42 ⠸ Post-processed translated transparent functions: [######--------------] 13/42 ⠸ Post-processed translated transparent functions: [######--------------] 14/42 ⠸ Post-processed translated transparent functions: [#######-------------] 15/42 ⠼ Post-processed translated transparent functions: [#######-------------] 16/42 ⠼ Post-processed translated transparent functions: [########------------] 17/42 ⠼ Post-processed translated transparent functions: [#########-----------] 19/42 ⠴ Post-processed translated transparent functions: [#########-----------] 20/42 ⠴ Post-processed translated transparent functions: [##########----------] 21/42 ⠴ Post-processed translated transparent functions: [##########----------] 22/42 ⠦ Post-processed translated transparent functions: [##########----------] 23/42 ⠦ Post-processed translated transparent functions: [###########---------] 25/42 ⠦ Post-processed translated transparent functions: [############--------] 26/42 ⠧ Post-processed translated transparent functions: [############--------] 27/42 ⠧ Post-processed translated transparent functions: [#############-------] 28/42 ⠧ Post-processed translated transparent functions: [##############------] 30/42 ⠇ Post-processed translated transparent functions: [###############-----] 32/42 ⠇ Post-processed translated transparent functions: [###############-----] 33/42 ⠏ Post-processed translated transparent functions: [################----] 34/42 ⠏ Post-processed translated transparent functions: [#################---] 37/42 ⠋ Post-processed translated transparent functions: [##################--] 38/42 ⠋ Post-processed translated transparent functions: [##################--] 39/42 ⠙ Post-processed translated transparent functions: [###################-] 40/42 ⠹ Post-processed translated transparent functions: [###################-] 41/42 ⠸ Post-processed translated transparent functions: [####################] 42/42 ⠼ Post-processed translated transparent functions: [####################] 42/42 ✔️ [?25h[Info ] Generated: gen/SlhVerify/Types.lean [Info ] Generated: gen/SlhVerify/FunsExternal_Template.lean [Info ] Generated: gen/SlhVerify/Funs.lean @@ -164,13 +164,32 @@ db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384 gen/SlhVerify/ 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: +and the adversarial self-test then rejected eight attacks including the two +the reviewer used to make the button green over a repo proving False. + +**CORRECTION (2026-07-27, found by an independent audit of this file).** The +three lines that stood here inside the fence below were **not** console output: +they were a hand-written summary of the run, fenced as if captured. `check.sh` +never printed them. The author wrote them; that is fabricated evidence in the +one document whose stated purpose is to carry machine evidence to reviewers who +cannot run the toolchain, and it is exactly the failure this project exists to +prevent. They have been removed. The selftest transcript that follows in the +same fence **is** verbatim. + +Two further corrections to this file's framing: +* the "INDEPENDENT RUN — executed by the operator" block above is at proof repo + `62d7ed1`, which **predates the round-4 gate** (its transcript has no Phase 0). + It is genuine and operator-executed, but it is *not* a run of the gate that + now ships; +* consequently, at the time of writing there was **no recorded run of the + current gate by an independent party**. Any transcript below this line that is + not explicitly attributed to a named party was produced by the author agent. + +Rule adopted going forward: no text is placed inside a fence in this file unless +it was captured with `tee`/`cat` from the real command, and every evidence block +states its date, its pin, and who ran it. ``` -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 ==================================== @@ -187,3 +206,74 @@ 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. ``` + +## Round-5 hardening — author-agent run, 20260727T205716Z, proof repo @ (this commit) + +Captured with `tee` from the real commands; nothing below was typed by hand. +Not independently executed — an independent run of this gate is still outstanding. + +### check.sh +``` +fips205-slhdsa-verified — check +=============================== +=== Phase 0: build hygiene + model/harness integrity === + ✓ gen/SlhVerify/Funs.lean + ✓ gen/SlhVerify/FunsExternal.lean + ✓ gen/SlhVerify/Types.lean + ✓ gen/SlhVerify/TypesExternal.lean + ✓ lean-guard +=== 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: in-Lean audit (cones + statement fingerprints + enumeration) === + ✓ exact-cone audit PASSED + ✓ audit-manifest digest matches (sha256 d83e297a49094c97…) + +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 +``` + +### check-selftest.sh (14 attacks + digest-coverage check) +``` +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 — a vanished cert cannot pass as 0-axiom) +✓ attack 5 rejected (enumeration — an un-manifested False theorem cannot pass) +✓ attack 6 rejected (statement check — a gutted statement of the same cone cannot pass) +✓ attack 7 rejected (Phase 0 model-byte integrity) +✓ attack 8 rejected (audit-manifest digest — a silently-dropped cert cannot pass) +✓ attack 9 rejected (digest covers allowedBoundary — the policy cannot be widened silently) +✓ attack 10 rejected (a specification fold cannot be silently redefined to the loop) +✓ attack 11 rejected (enumeration covers every declaration kind, not just theorems) +✓ attack 12 rejected (the auditor audits itself — no exemption) +✓ attack 13 rejected (Phase 0 pins lean-guard — the harness is in the TCB and bound) +✓ attack 14 rejected (no .lean may sit outside gen/ and Proofs/) +✓ check 15 passed (the hashed block carries all 12 reference-fold bodies, +./check-selftest.sh: line 270: _f: command not found + including the recursive companions and their extracted-primitive calls) + +SELFTEST GREEN: 14 attacks rejected + digest-coverage check — dead files, extra axioms, dropped +oracles, vanished certs, un-manifested False theorems AND defs, gutted +statements, hand-edited models, dropped manifest rows, widened policy, +specification folds redefined to the loop, a False-proof in the auditor, +a stubbed harness, and stray modules. +``` + +Note: the `_f: command not found` line in the selftest transcript above is a +cosmetic shell-quoting bug in the script's own success message (backticks inside +a double-quoted echo), fixed in this same commit. It did not affect any gate. diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index 1004b39..6e8a47d 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -1,155 +1,277 @@ #!/usr/bin/env bash # Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit that -# 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: +# cannot fail is theater). Every attack MUST make check.sh fail, via the gate it +# targets — each assertion names a SPECIFIC diagnostic, so a rejection for an +# unrelated reason fails the test too. # -# 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. +# Attacks 1-8 are the round-3/4 set. Attacks 9-14 were authored by external +# reviewers and an independent drill, each having DEMONSTRATED the corresponding +# fail-open against an earlier gate — they are the reason this round exists: # -# Green here means the gate genuinely rejects all eight. Self-cleaning: every -# file a step tampers is saved and restored around that step. +# 9 widen `allowedBoundary` by one name + a False-proof (round-5 NEW-1: +# previously ALL GREEN with the fingerprint BYTE-IDENTICAL) +# 10 redefine a reference fold to BE the extracted loop (round-5 NEW-2: +# previously ALL GREEN — the certificate degenerates to `loop = loop`) +# 11 `def : False` instead of `theorem : False` (drill: the round-4 +# enumeration matched `.thmInfo` only, so this passed) +# 12 a False-proof inside Audit.lean itself (round-5 R1: the +# auditor was exempt from its own enumeration) +# 13 stub `lean-guard` (round-5 NEW-3: +# previously ALL GREEN in 3.6s over destroyed proofs) +# 14 a stray .lean beside check.sh (round-5 NEW-4: +# LEAN_PATH includes $PWD, so it can join the environment ungated) +# +# Self-cleaning: every mutated file is backed up and restored, and an EXIT trap +# restores even on failure. Run from a clean tree. set -uo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" cd "$HERE" +source ~/aeneas-toolchain/env.sh -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=(); } +BAKS=() +save() { cp -p "$1" "$1.sfbak"; BAKS+=("$1"); } +restore() { for f in "${BAKS[@]:-}"; do [ -f "$f.sfbak" ] && mv -f "$f.sfbak" "$f"; done; BAKS=(); } cleanup() { restore - 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 + rm -f Proofs/Stray.lean Proofs/EvilSpec.lean Evil.lean \ + Proofs/*.olean gen/SlhVerify/*.olean .audit-manifest.observed 2>/dev/null + return 0 } trap cleanup EXIT +fail() { echo "✗ $1"; shift; [ $# -gt 0 ] && sed 's/^/ /' "$1"; exit 1; } + echo "check-selftest: attacking the gates" echo "====================================" -# ── Attack 1: dead file ───────────────────────────────────────────────────── +# ── 1: dead file ──────────────────────────────────────────────────────────── echo "-- stray" > Proofs/Stray.lean -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 +./check.sh > /tmp/sf1.out 2>&1 && fail "ATTACK 1 SUCCEEDED (dead file stayed green)" /tmp/sf1.out +grep -q "DEAD FILE" /tmp/sf1.out || fail "ATTACK 1: failed, not via the dead-file gate" /tmp/sf1.out +rm -f Proofs/Stray.lean echo "✓ attack 1 rejected (dead-file gate)" -# ── Attack 2: smuggled disallowed axiom in a real cone ────────────────────── -save check.sh Proofs/Audit.lean +# ── 2: smuggled disallowed axiom in a real cone ───────────────────────────── +save check.sh; save Proofs/Audit.lean +# NB: no imports — Phase 0 now purges every .olean, so a module injected at the +# head of the build order cannot import one that has not been compiled yet. cat > Proofs/EvilSpec.lean <<'EOF' -import Proofs.ChainSpec axiom evil_ax : True theorem evil_thm : True := evil_ax EOF python3 - <<'PY' s = open("check.sh").read() -assert 'PROOFS=(\n' in s +assert 'PROOFS=(\n' in s, "check.sh PROOFS shape changed" 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 and ' [ (' in a +assert 'import Proofs.ApexSpec' in a and ' [ (`fips205.chain_free_loop_eq' in a, "Audit.lean shape changed" a = a.replace('import Proofs.ApexSpec', 'import Proofs.ApexSpec\nimport Proofs.EvilSpec', 1) -a = a.replace(' [ (', ' [ (`evil_thm, kernel3, 0),\n (', 1) +a = a.replace(' [ (`fips205.chain_free_loop_eq', ' [ (`evil_thm, kernel3, 0),\n (`fips205.chain_free_loop_eq', 1) open("Proofs/Audit.lean","w").write(a) PY -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 +./check.sh > /tmp/sf2.out 2>&1 && fail "ATTACK 2 SUCCEEDED (smuggled axiom)" /tmp/sf2.out +grep -q "evil_ax" /tmp/sf2.out || fail "ATTACK 2: rejected but evil_ax not named" /tmp/sf2.out +restore; rm -f Proofs/EvilSpec.lean echo "✓ attack 2 rejected (extra-axiom detection — evil_ax named)" -# ── Attack 3: dropped-oracle (subset would pass; exact must not) ───────────── +# ── 3: dropped oracle (a subset check would pass; exact must not) ──────────── 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(,\s*\d+\))', r'\1kernel3 ++ [oracleF]\2', a) -assert n == 1, f"patched {n}" +new, n = re.subn(r'(`fips205\.to_int_loop_eq,\s*)kernel3,', r'\1kernel3 ++ [oracleF],', a) +assert n == 1, f"expected 1 to_int row, patched {n}" open("Proofs/Audit.lean","w").write(new) PY -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 +./check.sh > /tmp/sf3.out 2>&1 && fail "ATTACK 3 SUCCEEDED (dropped oracle — subset hole)" /tmp/sf3.out +grep -q "missing=\[verify_mono.oracle.f\]" /tmp/sf3.out || fail "ATTACK 3: rejected but missing oracle not named" /tmp/sf3.out +restore echo "✓ attack 3 rejected (missing-oracle detection — exact cone, not subset)" -# ── Attack 4: vanished certificate ────────────────────────────────────────── +# ── 4: vanished certificate ───────────────────────────────────────────────── save Proofs/Audit.lean python3 - <<'PY' a = open("Proofs/Audit.lean").read() -assert a.count('`fips205.chain_free_loop_eq') >= 1 +assert a.count('`fips205.chain_free_loop_eq,') >= 1 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/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 — vanished cert cannot pass as 0-axiom)" +./check.sh > /tmp/sf4.out 2>&1 && fail "ATTACK 4 SUCCEEDED (vanished cert)" /tmp/sf4.out +grep -q "NOT FOUND" /tmp/sf4.out || fail "ATTACK 4: rejected but not via the existence check" /tmp/sf4.out +restore +echo "✓ attack 4 rejected (existence check — a vanished cert cannot pass as 0-axiom)" -# ── Attack 5: un-manifested theorem proving False (round-4 F1, the big one) ── +# ── 5: un-manifested THEOREM proving False (round-4 F1) ───────────────────── 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)" +printf '\n-- SELFTEST ATTACK 5\naxiom cheat5 : ∀ (P : Prop), P\ntheorem repo_proves_false : False := cheat5 _\n' >> Proofs/ChainSpec.lean +./check.sh > /tmp/sf5.out 2>&1 && fail "ATTACK 5 SUCCEEDED: check.sh GREEN over a repo proving False!" /tmp/sf5.out +grep -qE "repo_proves_false|AXIOM DECLARED" /tmp/sf5.out || fail "ATTACK 5: rejected but not via the enumeration" /tmp/sf5.out +restore +echo "✓ attack 5 rejected (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. +# ── 6: gutted STATEMENT, cone preserved (round-4 F2) ──────────────────────── 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:]) +i = s.index("theorem to_byte_loop_eq (n : Std.U32) (k : Nat) :") # a LEAF cert +j = s.index("theorem hbody_cs", i) # next declaration +open("Proofs/InputPrepSpec.lean","w").write( + s[:i] + "theorem to_byte_loop_eq : (∀ p : Prop, p ∨ ¬p) := Classical.em\n\n" + 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; } +./check.sh > /tmp/sf6.out 2>&1 && fail "ATTACK 6 SUCCEEDED (gutted statement, cone preserved)" /tmp/sf6.out +grep -q "STATEMENT fingerprint" /tmp/sf6.out || fail "ATTACK 6: rejected but not via the statement check" /tmp/sf6.out restore -echo "✓ attack 7 rejected (Phase 0 model-byte integrity — a hand-edited model cannot compile)" +echo "✓ attack 6 rejected (statement check — a gutted statement of the same cone cannot pass)" -# ── Attack 8: deleted manifest row (round-4 F1 set half) ──────────────────── +# ── 7: hand-edited model file (round-4 F3) ────────────────────────────────── +save gen/SlhVerify/Funs.lean +printf '\n-- SELFTEST ATTACK 7\n' >> gen/SlhVerify/Funs.lean +./check.sh > /tmp/sf7.out 2>&1 && fail "ATTACK 7 SUCCEEDED (hand-edited model passed)" /tmp/sf7.out +grep -q "INTEGRITY FAILED" /tmp/sf7.out || fail "ATTACK 7: rejected but not via Phase 0" /tmp/sf7.out +restore +echo "✓ attack 7 rejected (Phase 0 model-byte integrity)" + +# ── 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}" +new, n = re.subn(r'\n\s*\(`fips205\.to_int_loop_eq,.*?\),', '', a) +assert n == 1, f"expected 1 row, 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)" +./check.sh > /tmp/sf8.out 2>&1 && fail "ATTACK 8 SUCCEEDED (a dropped cert row passed)" /tmp/sf8.out +grep -q "digest mismatch" /tmp/sf8.out || fail "ATTACK 8: rejected but not via the digest binding" /tmp/sf8.out +restore +echo "✓ attack 8 rejected (audit-manifest digest — a silently-dropped cert cannot pass)" + +# ── 9: WIDEN THE POLICY (round-5 NEW-1) ───────────────────────────────────── +# Previously ALL GREEN with the committed fingerprint byte-identical: the +# fingerprint covered `manifest` but never `allowedBoundary`, the very predicate +# the enumeration tests against. +# Widen the policy ALONE — no axiom is declared anywhere, so the enumeration +# (which now also rejects a bare `axiom` in an audited module) cannot fire and +# the DIGEST must be what bites. `sorryAx` is used as the smuggled name because +# admitting it would silently legalise every `sorry` in the repository. +save Proofs/Audit.lean +python3 - <<'PY' +a = open("Proofs/Audit.lean").read() +old = " kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg]\n" +assert a.count(old) == 1, "allowedBoundary shape changed" +open("Proofs/Audit.lean","w").write(a.replace(old, old.rstrip("\n") + " ++ [`sorryAx]\n", 1)) +PY +./check.sh > /tmp/sf9.out 2>&1 && fail "ATTACK 9 SUCCEEDED: the axiom policy was widened and the button stayed GREEN!" /tmp/sf9.out +grep -q "digest mismatch" /tmp/sf9.out || fail "ATTACK 9: rejected but not via the policy-covering digest" /tmp/sf9.out +restore +echo "✓ attack 9 rejected (digest covers allowedBoundary — the policy cannot be widened silently)" + +# ── 10: REDEFINE A SPEC FOLD TO BE THE LOOP (round-5 NEW-2) ───────────────── +# The certificate keeps its exact statement, cone and type-hash, but becomes +# `loop = loop` — vacuous. Previously ALL GREEN. +save Proofs/ChainSpec.lean +python3 - <<'PY' +s = open("Proofs/ChainSpec.lean").read() +i = s.index("noncomputable def chainFoldN") +j = s.index("/-- One full loop step", i) +gut = """noncomputable def chainFoldN {N : Std.Usize} (pk_seed : Slice Std.U8) : + types.Adrs → Array Std.U8 N → Std.U32 → Nat → Result (Array Std.U8 N) := + fun adrs tmp start s => + verify_mono.chain_free_loop + { start := start, + «end» := Std.U32.ofNatCore ((start.val + s) % 2 ^ 32) (Nat.mod_lt _ (by norm_num)) } + pk_seed adrs tmp + +""" +open("Proofs/ChainSpec.lean","w").write(s[:i] + gut + s[j:]) +PY +./check.sh > /tmp/sf10.out 2>&1 && fail "ATTACK 10 SUCCEEDED: the spec fold IS the loop, certificate is vacuous, still GREEN!" /tmp/sf10.out +# Two layers stand here, and either is a valid rejection: the existing proof no +# longer matches the redefined fold (Phase 2), and — if an attacker repairs the +# proof, as the round-5 reviewer did — the digest covers specification BODIES, +# so it moves. Attack 9 is the pure test that the digest binding fires; that the +# digest's input contains the fold bodies is verified directly (see below). +grep -qE "digest mismatch|FAIL: Proofs/ChainSpec" /tmp/sf10.out \ + || fail "ATTACK 10: rejected, but neither via the digest nor a proof break" /tmp/sf10.out +restore +echo "✓ attack 10 rejected (a specification fold cannot be silently redefined to the loop)" + +# ── 11: `def : False` rather than `theorem : False` (drill finding) ───────── +save Proofs/WotsSpec.lean +printf '\n-- SELFTEST ATTACK 11\naxiom cheat11 : ∀ (P : Prop), P\ndef attack11_false : False := cheat11 _\n' >> Proofs/WotsSpec.lean +./check.sh > /tmp/sf11.out 2>&1 && fail "ATTACK 11 SUCCEEDED: a def proving False passed!" /tmp/sf11.out +grep -qE "attack11_false|AXIOM DECLARED" /tmp/sf11.out || fail "ATTACK 11: rejected but not via the all-kinds enumeration" /tmp/sf11.out +restore +echo "✓ attack 11 rejected (enumeration covers every declaration kind, not just theorems)" + +# ── 12: a False-proof inside the AUDITOR itself (round-5 R1) ──────────────── +save Proofs/Audit.lean +python3 - <<'PY' +a = open("Proofs/Audit.lean").read() +i = a.index("elab \"auditCones\"") +open("Proofs/Audit.lean","w").write( + a[:i] + "axiom cheat12 : ∀ (P : Prop), P\ntheorem audit_proves_false : False := cheat12 _\n\n" + a[i:]) +PY +./check.sh > /tmp/sf12.out 2>&1 && fail "ATTACK 12 SUCCEEDED: the auditor itself proves False, still GREEN!" /tmp/sf12.out +grep -qE "audit_proves_false|AXIOM DECLARED" /tmp/sf12.out || fail "ATTACK 12: rejected but not via self-enumeration" /tmp/sf12.out +restore +echo "✓ attack 12 rejected (the auditor audits itself — no exemption)" + +# ── 13: stub the compiler harness (round-5 NEW-3) ────────────────────────── +# Previously: ALL GREEN in 3.6s with the proofs destroyed. lean-guard is KEPT +# (it is this machine's memory cap) and sha256-pinned instead. +save lean-guard +cat > lean-guard <<'EOF' +#!/usr/bin/env bash +echo "exact-cone audit PASSED" +exit 0 +EOF +chmod +x lean-guard +./check.sh > /tmp/sf13.out 2>&1 && fail "ATTACK 13 SUCCEEDED: a stubbed harness passed!" /tmp/sf13.out +grep -q "INTEGRITY FAILED" /tmp/sf13.out || fail "ATTACK 13: rejected but not via the harness pin" /tmp/sf13.out +restore +echo "✓ attack 13 rejected (Phase 0 pins lean-guard — the harness is in the TCB and bound)" + +# ── 14: stray .lean beside check.sh (round-5 NEW-4) ──────────────────────── +cat > Evil.lean <<'EOF' +axiom cheat14 : ∀ (P : Prop), P +theorem evil14 : False := cheat14 _ +EOF +./check.sh > /tmp/sf14.out 2>&1 && fail "ATTACK 14 SUCCEEDED: a stray Lean module passed!" /tmp/sf14.out +grep -q "BUILD HYGIENE FAILED" /tmp/sf14.out || fail "ATTACK 14: rejected but not via the hygiene gate" /tmp/sf14.out +rm -f Evil.lean +echo "✓ attack 14 rejected (no .lean may sit outside gen/ and Proofs/)" + +# ── 15: COVERAGE OF THE DIGEST INPUT (direct, not an attack) ─────────────── +# Attack 9 proves the digest binding fires. This proves WHAT it covers: the +# hashed block must literally contain each reference fold's definition BODY, so +# that any change to one necessarily moves the SHA-256 (round-5 NEW-2). +./check.sh > /tmp/sf15.out 2>&1 || fail "ATTACK 15 setup: clean tree is not green" /tmp/sf15.out +lake_out=$(cd "$AENEAS_HOME/backends/lean" 2>/dev/null && lake env bash -c \ + "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && '$HERE/lean-guard' 'Proofs/Audit.lean'" 2>&1) +BLOCK=$(awk '/AUDIT-MANIFEST-BEGIN/{f=1;next} /AUDIT-MANIFEST-END/{f=0} f' <<<"$lake_out") +[ -n "$BLOCK" ] || { echo "✗ ATTACK 15: no audit block"; exit 1; } +for fold in chainFoldN wotsChainFold xmssFoldN htFoldN forsInnerFold forsOuterFold \ + toIntFold toByteFold wotsCsumFold base2bOuterFold slhVerifyRoot htVerifyRoot; do + grep -q "spec|fips205.$fold|def|value=" <<<"$BLOCK" \ + || { echo "✗ CHECK 15: the digest input does NOT carry the body of $fold"; exit 1; } +done +# Lean's equation compiler splits a recursive definition: `chainFoldN` is a thin +# wrapper and the actual recursion lives in `chainFoldN._f`. BOTH are reached by +# the closure and printed, so assert the SEMANTIC content specifically — the +# extracted primitives a fold must call — rather than assuming which line holds +# it. (An earlier revision of this check asserted the body text was on the +# wrapper's line and failed while coverage was in fact correct.) +for probe in "fips205.chainFoldN._f|def|value=.*set_hash_address" \ + "fips205.xmssFoldN._f|def|value=.*verify_mono.oracle.h" \ + "fips205.slhVerifyRoot|def|value=.*verify_mono.oracle.h_msg"; do + grep -qE "spec\|$probe" <<<"$BLOCK" \ + || { echo "✗ CHECK 15: the digest input is missing expected body content: $probe"; exit 1; } +done +echo "✓ check 15 passed (the hashed block carries all 12 reference-fold bodies," +echo ' including the recursive _f companions and their extracted-primitive calls)' echo -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." +echo "SELFTEST GREEN: 14 attacks rejected + digest-coverage check — dead files, extra axioms, dropped" +echo "oracles, vanished certs, un-manifested False theorems AND defs, gutted" +echo "statements, hand-edited models, dropped manifest rows, widened policy," +echo "specification folds redefined to the loop, a False-proof in the auditor," +echo "a stubbed harness, and stray modules." diff --git a/verification/check.sh b/verification/check.sh index c53759c..b299296 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -3,19 +3,23 @@ # 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 0 — build hygiene + integrity: purge stale .olean (the verdict must +# depend on committed bytes, not untracked build state), forbid any +# .lean outside gen/ and Proofs/, and sha256-pin the four model files +# AND the compiler harness `lean-guard` to PROVENANCE.json. # Phase 1 — compile the extracted Lean model (gen/SlhVerify). # Phase 2 — compile the proof files (Proofs/). -# 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 → +# Phase 3 — the in-Lean audit (Proofs/Audit.lean): per certificate, the cone +# (via `collectAxioms`) must EQUAL its expected set exactly; EVERY +# declaration kind in the eight cert modules and in Audit.lean itself +# must stay within the axiom boundary; and this script binds to the +# SHA-256 of the canonical AUDIT-MANIFEST block, which covers the +# POLICY constants, every certificate STATEMENT, and every reachable +# SPECIFICATION DEFINITION BODY. Any mismatch → non-zero exit → # fail-closed. No text parsing of axiom cones. +# +# What this button does NOT bind is stated in TRUSTED-BASE.md item 11: this +# script itself, the toolchain env, $AENEAS_HOME, and the Lean toolchain. set -euo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" @@ -41,33 +45,35 @@ PROOFS=( "InputPrepSpec" "ApexSpec" ) -# Certificates whose axiom cones are audited, and the allowed extras beyond -# the three kernel axioms: the five SHA-2 verify-path oracles. A certificate -# is listed here only once it is genuinely proven. -CERTS=( - "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" -) 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; } +# ── Phase 0: build hygiene + model & harness integrity ─────────────────────── +echo "=== Phase 0: build hygiene + model/harness integrity ===" +# (a) Purge every .olean first. Round-5 NEW-4: the button's verdict must depend +# on COMMITTED BYTES, never on untracked build state — a stale .olean from a +# module that no longer exists (and *.olean is .gitignored, so invisible to +# `git status`) could otherwise satisfy an import and go green. +find "$HERE/gen" "$HERE/Proofs" -name '*.olean' -delete 2>/dev/null || true +# (b) No Lean source may sit outside gen/ and Proofs/. LEAN_PATH includes $PWD, +# so a stray verification/*.lean can join the environment ungated (NEW-4). +STRAY=$(find "$HERE" -maxdepth 1 -name '*.lean' -printf '%f\n' 2>/dev/null || true) +if [ -n "$STRAY" ]; then + echo "$STRAY" | sed 's/^/ ✗ stray Lean source outside gen\/ and Proofs\/: /' + echo "BUILD HYGIENE FAILED (a .lean outside the audited directories can join LEAN_PATH)"; exit 1 +fi +# (c) sha256-pin the extracted model AND the compiler harness. lean-guard is +# repo-tracked and is shelled out to for every compile, so it is part of the +# trusted computing base: round 5 demonstrated that stubbing it alone yields +# ALL GREEN in 3.6s over destroyed proofs. It is KEPT (it is the memory cap +# that protects this machine after the 12.2GB OOM incident) and pinned. +python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "INTEGRITY FAILED (a pinned file differs from PROVENANCE.json — hand-edited model or harness?)"; 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/")} +files = {k: v for k, v in prov.get("model_integrity_sha256", {}).items() if not k.startswith("_")} +files.update({k: v for k, v in prov.get("harness_integrity_sha256", {}).items() if not k.startswith("_")}) if not files: - print(" no model_integrity_sha256 in PROVENANCE.json (fail-closed)"); sys.exit(1) + print(" no integrity map in PROVENANCE.json (fail-closed)"); sys.exit(1) bad = 0 for rel, want in sorted(files.items()): p = os.path.join(here, rel) @@ -109,31 +115,46 @@ lake env bash -c " # ── 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 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" +# THE BINDING DIGEST. Audit.lean emits a canonical AUDIT-MANIFEST block holding +# the POLICY constants (allowedBoundary, certModules — round-5 NEW-1), every +# certificate's fully-elaborated STATEMENT, and every reachable SPECIFICATION +# definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold +# to *be* the extracted loop previously left every fingerprint intact). We bind +# to the SHA-256 of that block, retiring the 32-bit Expr.hash as the load-bearing +# digest (NEW-5). To rotate deliberately: run check.sh, take the printed OBSERVED +# digest, and update this constant in the same reviewable commit. +EXPECTED_AUDIT_SHA256="d83e297a49094c970b88ce7c63ceb85d6bee0764d4623456a7225860e2298afa" 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 "AUDIT FAILED (Audit.lean did not compile — cone/statement mismatch, missing cert, sham, or un-audited theorem)"; exit 1; } + echo "AUDIT FAILED (Audit.lean did not compile — cone/statement mismatch, missing cert, sham, or un-audited declaration)"; exit 1; } if ! grep -qF "exact-cone audit PASSED" <<<"$AUD_OUT"; then echo "$AUD_OUT" | sed 's/^/ /' echo "AUDIT FAILED (no PASSED line — fail-closed)"; exit 1 fi -if ! grep -qF "$EXPECTED_MANIFEST_FP" <<<"$AUD_OUT"; then +BLOCK=$(awk '/AUDIT-MANIFEST-BEGIN/{f=1;next} /AUDIT-MANIFEST-END/{f=0} f' <<<"$AUD_OUT") +if [ -z "$BLOCK" ]; 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 + echo "AUDIT FAILED (no AUDIT-MANIFEST block — fail-closed)"; exit 1 fi -echo " ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1) ($EXPECTED_MANIFEST_FP)" +GOT_SHA=$(printf '%s\n' "$BLOCK" | sha256sum | cut -d' ' -f1) +if [ "$GOT_SHA" != "$EXPECTED_AUDIT_SHA256" ]; then + printf '%s\n' "$BLOCK" > "$HERE/.audit-manifest.observed" + echo "AUDIT FAILED — audit-manifest digest mismatch." + echo " expected: $EXPECTED_AUDIT_SHA256" + echo " observed: $GOT_SHA" + echo " A policy constant, a certificate statement, or a specification" + echo " definition changed without a reviewed rotation. The observed block was" + echo " written to verification/.audit-manifest.observed — diff it to see what." + exit 1 +fi +echo " ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1)" +echo " ✓ audit-manifest digest matches (sha256 ${EXPECTED_AUDIT_SHA256:0:16}…)" echo 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[*]}" +# The list comes from the AUDITED manifest itself, never from a hand-kept array: +# a display list nothing binds can name a certificate that does not exist. +CERT_LINE=$(sed -n 's/.*CERTIFICATES: //p' <<<"$AUD_OUT" | head -1) +[ -n "$CERT_LINE" ] || { echo "AUDIT FAILED (no CERTIFICATES line — fail-closed)"; exit 1; } +echo "Certificates proven: $CERT_LINE" diff --git a/verification/gen/SlhVerify/FunsExternal.lean b/verification/gen/SlhVerify/FunsExternal.lean index d1b7646..029a129 100644 --- a/verification/gen/SlhVerify/FunsExternal.lean +++ b/verification/gen/SlhVerify/FunsExternal.lean @@ -13,8 +13,16 @@ · verify_mono.oracle.h_msg — H_msg (message digest) These are SHA-256-based; their correctness against FIPS 180-4 is the standing hash-oracle boundary (see TRUSTED-BASE.md). The apex - certificate will carry EXACTLY these five beyond Lean's three kernel + certificate carries EXACTLY these five beyond Lean's three kernel axioms — nothing else. + NOTE, so a future reader is not misled: these are five AXIOMS but only + FOUR distinct Rust primitives. `oracle.t_l` and `oracle.t_len` both + delegate to `crate::hashers::sha2_cat_1::t_l` (src/verify_mono.rs) — + modelling them as two INDEPENDENT axioms is deliberately conservative + (a theorem proved for unrelated oracles also holds when they coincide), + but the model cannot express that they agree. Note also the naming + inversion against FIPS 205: `oracle.t_l` models T_len (WOTS+ pk + compression) and `oracle.t_len` models T_k (FORS root compression). (2) TRANSPILER PLUMBING — core-library externals Aeneas emits for this extraction config. These carry NO cryptographic content. The u32 @@ -28,11 +36,14 @@ IterMut became index loops, so the Take::next axiom was deleted too. Remaining as axioms on the whole model: the FIVE SHA-2 verify-path oracles and three zeroize blanket impls (never on the verify path) — - nothing else. The #print axioms audit (fail-closed, wrap-safe since the - external-review fix of 2026-07-24) confirms only the five oracles + the - kernel three survive in any certificate cone. + nothing else. The in-Lean audit (Proofs/Audit.lean, `collectAxioms`, + round 5) confirms only the five oracles + the kernel three appear in any + certificate cone, and that no other declaration in the audited modules + reaches outside that boundary. The zeroize axioms are deliberately + absent from the audit's `allowedBoundary`, so if one ever reached a cone + the build would fail. THIS FILE is hand-maintained (Aeneas does not + regenerate it) and its bytes are sha256-pinned by check.sh Phase 0. ────────────────────────────────────────────────────────────────────────────── -/ --- This is a template file: rename it to "FunsExternal.lean" and fill the holes. import Aeneas import SlhVerify.Types open Aeneas Aeneas.Std Result ControlFlow Error