mirror of
https://github.com/saymrwulf/fips205-slhdsa-verified.git
synced 2026-09-04 20:03:44 +00:00
review round 5: bind the policy, the specification bodies, and the harness
The third reviewer demonstrated that the round-4 gate was closed at the EXPLOITS, not the MECHANISMS: it bound the manifest rows while the things he moved sat outside the binding. Three fail-opens, each executed end-to-end with the button printing ALL GREEN. No theorem, proof, fold, or model body changed. NEW-1 — the policy constant was unbound. `manifestFingerprint` covered `manifest` but never `allowedBoundary`, the sole predicate the enumeration tests against; adding one name re-opened the False-proof with the committed fingerprint BYTE-IDENTICAL. NEW-2 — the specification bodies were unbound. The statement fingerprint pinned each certificate's TYPE, which names its reference fold; redefining that fold to *be* the extracted loop left cone and type-hash identical while the certificate degenerated to `loop = loop`. 100% of the fidelity content lives in those defs. NEW-3 — the harness was unbound. Stubbing verification/lean-guard alone, without touching check.sh or the proofs, gave ALL GREEN in 3.6s over destroyed proofs. FIX — one mechanism rather than three patches. Audit.lean now emits a canonical AUDIT-MANIFEST block and check.sh binds to its SHA-256. The block covers the POLICY constants, every certificate's fully-elaborated statement, and every specification constant transitively reachable from those statements with its fully-elaborated BODY (41 constants; the closure is computed, so a new fold cannot appear without moving the digest; Prop-valued constants contribute their statement, by proof irrelevance). This also retires the 32-bit Expr.hash as the binding (NEW-5) — it survives only as a per-certificate diagnostic. Enumeration now covers EVERY declaration kind (a `def : False` passed before) in the eight certificate modules AND in Audit.lean itself — the auditor is no longer exempt (round-5 R1). A bare `axiom` in audited scope is now an error. Phase 0 purges stale .olean (the verdict must depend on committed bytes, not .gitignored build state — NEW-4), forbids any .lean outside gen/ and Proofs/, and sha256-pins the four model files AND lean-guard. lean-guard is KEPT rather than removed (the reviewer's portability advice is declined by operator decision): it is the memory cap and machine-wide lock that protect the build machine after a 12.2GB OOM took the host down. That trade-off is documented. check.sh's "Certificates proven:" line now comes from the audited manifest; the hand-kept CERTS array — the one authoritative claim string nothing bound — is deleted. check-selftest.sh: 14 attacks, all rejected, plus a check that the hashed block literally carries the twelve fold bodies. Attacks 9-14 are the reviewers' and an independent drill's own exploits, turned into regression tests. DOCS. TRUSTED-BASE gains item 11 (the REAL trusted computing base — lean-guard pinned; check.sh, the toolchain env, $AENEAS_HOME, python3 and Lean still trusted) and item 12 (the apex does not compose the ten). README: the audit description rewritten; the XMSS sibling-order claim downgraded from "pins" to "makes visible", with a new blanket non-claim covering all ten loop certificates; the de-plumbing file claim corrected (round 1 touched only verify_mono.rs, round 2 only helpers.rs — which is ON the deployed verify AND sign paths, now disclosed; wots.rs was never patched). RECORDED-RUN: three lines that stood inside a fence were a hand-written summary, not console output — fabricated evidence in the file whose purpose is machine evidence. They are removed and the fabrication is named in place, together with the correction that the "INDEPENDENT RUN" block predates this gate. New rule: nothing goes in a fence unless captured with tee/cat, and every block states its date, pin, and who ran it. The transcripts added here follow it. Also disclosed rather than buried: three bugs in my own test harness this round (an olean-purge build-order break, an attack rejected by the wrong rule, and a coverage assertion looking on the wrong line) — each would have let an attack pass or fail for an unrelated reason. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
parent
45a2f65a2d
commit
dce0473013
8 changed files with 669 additions and 255 deletions
83
README.md
83
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<<a)+indices[i]`, run the inner
|
||||
Merkle loop, write `root[i]` — cone kernel-3 + `oracle.{f, h}`. Split into
|
||||
two files under the memory discipline; the outer step lemma closes by
|
||||
|
|
@ -233,10 +270,16 @@ this repository was created:
|
|||
model from the mono root; charon + aeneas both exit 0, and
|
||||
`verification/check.sh` compiles the result. At this compat-patch commit
|
||||
the only change to pre-existing code was two lines wiring the new module;
|
||||
the generic paths and all twelve parameter sets stayed untouched. (The
|
||||
later de-plumbing commits — rounds 1 and 2 — then made further local edits
|
||||
to `helpers.rs`/`wots.rs`, each documented and differential-tested; see the
|
||||
snapshot history at head `797b4ef`.)
|
||||
the generic paths and all twelve parameter sets stayed untouched. **That
|
||||
scoping does not extend to the later de-plumbing commits, and the difference
|
||||
matters:** round 1 (`6f6a9d6`) touched only the private `verify_mono.rs`, but
|
||||
round 2 (`bea1051`) rewrote `to_int` and `base_2b` in **`src/helpers.rs`,
|
||||
which the DEPLOYED generic verify path and the SIGNING path also call**
|
||||
(`slh.rs`, `wots.rs`, `fors.rs`). So the snapshot's deployed verifier — the
|
||||
one the differential test compares against — is itself patched relative to
|
||||
upstream `30bac08`. `src/wots.rs` was never modified by any patch commit (an
|
||||
earlier revision of this README wrongly named it). See the snapshot history
|
||||
at head `797b4ef` and TRUSTED-BASE.md item 7.
|
||||
|
||||
## What is claimed (the button is green)
|
||||
|
||||
|
|
|
|||
|
|
@ -55,3 +55,30 @@ proceeds and is part of every claim.
|
|||
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.
|
||||
**Concretely, so the consequence is not left to the reader:** that byte is
|
||||
the *only* thing separating the pure and prehash variants. If it were wrong
|
||||
or dropped, a signature issued over the pure M′ would verify as a prehash
|
||||
signature and vice versa — cross-variant signature confusion, a forgery
|
||||
primitive. No certificate in this repository would change.
|
||||
11. **The verification harness itself.** The certificates are statements
|
||||
checked by the Lean kernel, but the *button* that reports them is a shell
|
||||
script. Round-5 review demonstrated that stubbing `verification/lean-guard`
|
||||
alone — one repo-tracked file, without touching `check.sh`, the manifest, or
|
||||
the proofs — yields ALL GREEN in 3.6 seconds over deliberately destroyed
|
||||
proofs. `lean-guard` is therefore **sha256-pinned** by check.sh Phase 0
|
||||
(`PROVENANCE.json → harness_integrity_sha256`); it is kept rather than
|
||||
removed because it is the memory cap and machine-wide lock that protect the
|
||||
build machine (a Lean elaboration once reached 12.2 GB and took the host
|
||||
down). Still trusted, and NOT bound by anything the button can check:
|
||||
`check.sh` itself, `~/aeneas-toolchain/env.sh`, the `$AENEAS_HOME` tree
|
||||
(i.e. *which* Aeneas/Lean library the proofs are checked against), `python3`,
|
||||
and the Lean toolchain. An audit executed by a harness cannot defend against
|
||||
an author who edits that harness; the consumer defense is the pinned commit,
|
||||
reviewed at the pin.
|
||||
12. **Composition.** The apex does **not** compose the ten loop-fidelity
|
||||
theorems — it is a structural factorization of the extracted verifier around
|
||||
its final equality check and references none of them (it would remain
|
||||
provable if one were deleted). The ten are independent, individually
|
||||
human-reviewed lemmas. Round-5 review makes this worth stating here rather
|
||||
than only in the README: each of the ten is individually meaningful only to
|
||||
the extent a human has read its reference fold against FIPS 205.
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
{
|
||||
"_comment": "Single machine-readable pin set to reproduce the extracted Lean model in gen/SlhVerify from source. External review round 2 (2026-07-24). Running verification/extract.sh against the pinned source tree with the pinned Charon/Aeneas toolchain reproduces the two aeneas-generated files byte-identically (sha256 below). The *External*.lean files are hand-maintained (not regenerated) and are NOT part of this reproducibility claim.",
|
||||
"_comment": "Single machine-readable pin set to reproduce the extracted Lean model in gen/SlhVerify from source. External review rounds 2-5 (2026-07-24 .. 2026-07-27). Running verification/extract.sh against the pinned source tree with the pinned Charon/Aeneas toolchain reproduces the two aeneas-generated files byte-identically (generated_artifacts_sha256 below). The *External*.lean files are hand-maintained (not regenerated) and are NOT part of that reproducibility claim — but they ARE byte-pinned for integrity in model_integrity_sha256, since they carry the five oracle axioms and the discharged Step definitions. NOTE: SlhVerify.llbc is an intermediate artifact and is .gitignored, so its hash here can only be checked by a party who re-runs extract.sh.",
|
||||
"parameter_set": "SLH-DSA-SHA2-128s",
|
||||
"source": {
|
||||
"repo": "github.com/saymrwulf/fips205-source",
|
||||
|
|
@ -10,8 +10,13 @@
|
|||
"rust_toolchain_toml": "nightly-2026-06-01"
|
||||
},
|
||||
"transpiler": {
|
||||
"charon": { "commit": "9dd7f23c", "toolchain_channel": "nightly-2026-06-01" },
|
||||
"aeneas": { "commit": "bf13c42e" }
|
||||
"charon": {
|
||||
"commit": "9dd7f23c",
|
||||
"toolchain_channel": "nightly-2026-06-01"
|
||||
},
|
||||
"aeneas": {
|
||||
"commit": "bf13c42e"
|
||||
}
|
||||
},
|
||||
"proof_env": {
|
||||
"lean": "v4.30.0-rc2 (3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc)",
|
||||
|
|
@ -33,11 +38,15 @@
|
|||
],
|
||||
"byte_identical_regeneration_verified": "2026-07-24",
|
||||
"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).",
|
||||
"_comment": "All four Lean model files check.sh Phase 0 pins before compiling anything \u2014 the two aeneas-generated files AND the two hand-maintained *External files (which carry the five oracle axioms and the Step defs). A hand-edit of the model fails the build here (round-4 reviewer F3).",
|
||||
"gen/SlhVerify/TypesExternal.lean": "37958beb7c90b649497a20b0802f98f0fb2d975c245eca956d7396af74d7759f",
|
||||
"gen/SlhVerify/FunsExternal.lean": "73fa2a7d14b35bb6b6746534e88cba527d0e17f154f7a7d841a9c519befeea47",
|
||||
"gen/SlhVerify/FunsExternal.lean": "5efe551c35969c9da28b2f3eaed4a6a67c410c62a1926aab390e3abf010390f8",
|
||||
"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."
|
||||
"harness_integrity_sha256": {
|
||||
"_comment": "The compiler harness is part of the trusted computing base: check.sh shells out to lean-guard for every compile, and round-5 review demonstrated that stubbing it alone yields ALL GREEN in 3.6s over destroyed proofs. lean-guard is KEPT (it is the memory cap and machine-wide lock that protect this machine after the 12.2GB OOM incident) and sha256-pinned by Phase 0. NOT covered, and disclosed as trusted in TRUSTED-BASE.md item 11: check.sh itself, ~/aeneas-toolchain/env.sh, $AENEAS_HOME, python3, and the Lean toolchain.",
|
||||
"lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f"
|
||||
},
|
||||
"audit_gate": "verification/Proofs/Audit.lean \u2014 in-Lean audit (round 5). Per certificate: exact cone equality (collectAxioms) + elaborated-statement check. Enumeration: EVERY declaration kind (def/theorem/opaque/axiom \u2014 round 4 matched theorems only, so a `def : False` passed) in the eight certificate modules AND in Audit.lean itself (the auditor is not exempt). Binding digest: check.sh binds to the SHA-256 of a canonical AUDIT-MANIFEST block covering the POLICY constants (allowedBoundary + certModules \u2014 round-5 NEW-1: widening allowedBoundary previously re-opened the False-proof with the fingerprint byte-identical), 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 cone and fingerprint intact while the certificate degenerated to `loop = loop`). The 32-bit Expr.hash is retained only as a per-certificate diagnostic, not as the binding. Fail-closed; adversarially exercised by check-selftest.sh. check.sh Phase 0 additionally purges stale .olean files, forbids stray .lean outside gen/ and Proofs/, and pins model + harness bytes."
|
||||
}
|
||||
|
|
@ -1,37 +1,47 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────────
|
||||
Proofs/Audit.lean — the axiom-cone + statement + coverage audit, in Lean.
|
||||
Proofs/Audit.lean — the axiom / statement / specification / coverage audit.
|
||||
|
||||
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.
|
||||
ROUND 5 (third reviewer, 2026-07-27) demonstrated that the round-4 gate was
|
||||
closed at the EXPLOITS but not at the MECHANISMS. Three fail-opens, each
|
||||
executed end-to-end with the button printing ALL GREEN:
|
||||
|
||||
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).
|
||||
NEW-1 `manifestFingerprint` covered `manifest` only — never
|
||||
`allowedBoundary`, the sole predicate the enumeration tests against.
|
||||
Adding one name to that list re-opened the `False`-proof completely,
|
||||
with the committed fingerprint BYTE-IDENTICAL.
|
||||
NEW-2 the statement fingerprint pinned each certificate's TYPE, which
|
||||
references its hand-written reference fold BY NAME. Redefining that
|
||||
fold to *be* the extracted loop left cone and type-hash identical
|
||||
while the certificate degenerated to "the loop equals the loop" —
|
||||
100% of the fidelity content lives in those definitions.
|
||||
(drill) layer-2 enumeration matched `.thmInfo` only, so a `def : False`
|
||||
passed; and this file's own declarations were enumerated by nothing.
|
||||
|
||||
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.
|
||||
The fix binds the WHOLE audited object, not the parts an attacker happened to
|
||||
touch. This file emits a canonical AUDIT-MANIFEST block covering:
|
||||
|
||||
· the POLICY constants (`allowedBoundary`, `certModules`) — NEW-1;
|
||||
· every certificate's fully-elaborated STATEMENT (`pp.all`) — F2 properly;
|
||||
· every hand-written SPECIFICATION constant transitively reachable from
|
||||
those statements, with its fully-elaborated DEFINITION BODY — NEW-2.
|
||||
(Proof-valued constants contribute their statement, not their proof term:
|
||||
proof irrelevance makes the term semantically immaterial.)
|
||||
|
||||
`check.sh` binds to the **SHA-256** of that block. This also retires the
|
||||
32-bit `Expr.hash` as the load-bearing digest (NEW-5): the per-certificate
|
||||
type hashes below remain, but only as fast, human-legible DIAGNOSTICS that
|
||||
name which certificate moved — the cryptographic binding is the SHA-256.
|
||||
|
||||
Enumeration now covers EVERY declaration kind (`def`, `theorem`, `opaque`,
|
||||
`axiom`, …) in the eight certificate modules AND every declaration of this
|
||||
file itself (the auditor is no longer exempt from its own audit — round-5 R1).
|
||||
|
||||
Standing limit, stated accurately (see TRUSTED-BASE.md item 11 for the full
|
||||
trusted computing base): an audit executed by a harness cannot defend against
|
||||
an author who edits that harness. `verification/lean-guard` is therefore
|
||||
sha256-pinned by check.sh Phase 0, but `check.sh` itself, the toolchain env,
|
||||
and `$AENEAS_HOME` remain trusted. The consumer defense is, and always was,
|
||||
the pinned commit reviewed at the pin.
|
||||
────────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.ChainSpec
|
||||
import Proofs.WotsSpec
|
||||
|
|
@ -54,23 +64,22 @@ 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 only axioms permitted in ANY cone in the certificate modules: kernel-3
|
||||
plus the five SHA-2 oracles. -/
|
||||
/-- The ONLY axioms permitted in any cone anywhere in the audited modules.
|
||||
POLICY CONSTANT — folded into the SHA-256 digest (round-5 NEW-1): widening
|
||||
this list changes the digest and fails the build. -/
|
||||
def allowedBoundary : List Name :=
|
||||
kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg]
|
||||
|
||||
/-- The eight certificate-bearing proof modules. Every `theorem` defined in
|
||||
these must have a cone ⊆ allowedBoundary (layer 2). -/
|
||||
/-- The eight certificate-bearing proof modules. POLICY CONSTANT — also folded
|
||||
into the digest. (It is additionally cross-checked by `certsSeen` below:
|
||||
every manifest certificate must be found inside one of these modules.) -/
|
||||
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. -/
|
||||
/-- Per-certificate expected cone + a 32-bit `Expr.hash` of the elaborated
|
||||
statement. The hash is a DIAGNOSTIC ONLY (it names which certificate moved);
|
||||
the binding digest is the SHA-256 over the canonical block. -/
|
||||
def manifest : List (Name × List Name × UInt64) :=
|
||||
[ (`fips205.chain_free_loop_eq, kernel3 ++ [oracleF], 2535491171),
|
||||
(`fips205.wots_loop1_eq, kernel3 ++ [oracleF], 2968777228),
|
||||
|
|
@ -84,25 +93,63 @@ def manifest : List (Name × List Name × UInt64) :=
|
|||
(`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 :=
|
||||
/-- Deterministic name ordering for the canonical serialization. -/
|
||||
def sortNames (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
|
||||
|
||||
/-- 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?)"
|
||||
|
|
@ -117,32 +164,76 @@ elab "auditCones" : command => do
|
|||
| 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 _`.
|
||||
|
||||
-- (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
|
||||
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
|
||||
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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."
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue