diff --git a/ATTESTATION-BASIS.md b/ATTESTATION-BASIS.md new file mode 100644 index 0000000..8d4d47b --- /dev/null +++ b/ATTESTATION-BASIS.md @@ -0,0 +1,105 @@ +# Attestation basis — independent technical review + +This file records the **reviewer's own words**, verbatim, as the conditions +attached to any attestation of this repository. It is committed here so that the +limits travel with the artifact rather than living in a review document the +consumer never sees. + +Nothing in this file is a decision to attest. The signing-key halt and the +paper-appeal gate are the operator's, and an attest verdict from a reviewer is a +technical input to that decision, not the decision. + +--- + +## Verdict + +**Round 8, third reviewer, 2026-07-28: ATTEST, with the conditions below.** + +Basis the reviewer performed on hardware, an OS and a toolchain build that are +not the author's: `check.sh` ALL GREEN at `1bc4f39` with six pins verified and +the audit digest `d83e297a…`; `check-selftest.sh` green (17 attacks + the +digest-coverage check); the audit digest recomputed *outside* `check.sh` from a +bare `lean Proofs/Audit.lean` and matched byte-for-byte against the committed +`AUDIT-MANIFEST.txt`; NEW-13 attacked five ways; the NIST vector file +independently re-derived from the official 30.7 MB upstream file and found +byte-identical; the full empirical bridge executed on stable Rust; and the ACVP +harness mutation-tested (a flipped bit in a valid vector and a deleted NIST test +both correctly fail). + +Not performed by any reviewer: `verification/extract.sh`. See condition 9. + +--- + +## Conditions, verbatim from the reviewer + +> What is established: eleven Lean 4 theorems over the Charon/Aeneas-extracted +> model of `verify_mono::slh_verify_128s`, the private monomorphic re-expression +> of the SLH-DSA-SHA2-128s verify path. Ten are loop-fidelity theorems; the apex, +> `fips205.slh_verify_128s_accepts_iff`, characterises acceptance — the extracted +> verifier returns `ok true` if and only if the recomputed hypertree root +> byte-equals the pinned public-key root. Every certificate's axiom cone is +> exactly Lean's three kernel axioms plus the named SHA-2 oracles that layer +> reaches, machine-checked inside Lean and bound by a SHA-256 digest over the +> policy constants, the elaborated statements and the specification bodies. +> +> This attestation carries the following limits, all of which are stated in the +> repository's own `TRUSTED-BASE.md` and all of which I verified are accurate: +> +> 1. **The five SHA-2 hash oracles are opaque assumptions.** Their conformance to +> FIPS 180-4 is not proven here. `oracle.t_l` and `oracle.t_len` are two +> independent axioms over one Rust primitive — conservative, but the model +> cannot express that they agree. +> 2. **The ten loop certificates are transliteration-fidelity results, not +> conformance results.** Each equates a generated loop with a hand-written +> reference fold built from the *same* extracted primitives, so it pins what +> the extracted code does at each index and makes it visible; it does not +> exclude a wrong ADRS field or a wrong schedule relative to FIPS 205. Mapping +> each fold onto the standard remains a human reading step. +> 3. **The apex does not compose the ten.** 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. +> 4. **`base_2b`'s inner accumulation loop has no certificate.** It determines +> the FORS indices and WOTS+ digits, so a defect there could change the +> recomputed root while all eleven theorems still hold. +> 5. **Everything above the extraction root is uncovered:** M′ assembly, the +> pure-versus-prehash domain-separator byte, the `ctx.len() > 255` bound, and +> signature/public-key deserialization. +> 6. **The bridge from the proved `verify_mono` facade to the deployed generic +> `pk.verify()` is empirical, not a machine-checked refinement:** 137 evaluated +> input/verdict cases on the proved path, of which 20 are NIST ACVP +> known-answer tests and 127 compare mono against the deployed verifier. A +> passing differential test is evidence, not a proof. +> 7. **Trusted and unbound by anything the button can check:** the Lean kernel and +> its three axioms; the Charon/Aeneas transpilation pair; `verification/check.sh` +> itself; `~/aeneas-toolchain/env.sh`; the `$AENEAS_HOME` Aeneas/Lean library +> the proofs are checked against; `python3`; and the Lean toolchain. +> `lean-guard` and `Proofs/Audit.lean` are sha256-pinned, so tampering with +> either is a build failure rather than a silent green; an author who edits one +> *and* rotates its pin in the same commit is caught only by reading the diff +> at the pin. +> 8. **Scope is SLH-DSA-SHA2-128s only**, verify path only. Key generation and +> signing are out of scope. No reproducible-builds claim: the proof is about +> the pinned source, not any compiled binary. +> 9. **`verification/extract.sh`'s byte-identical regeneration of the Lean model +> from the pinned Rust source has never been observed by any party other than +> the author.** Every other load-bearing claim in this repository has been +> reproduced by an independent reviewer on different hardware; this one has +> not, and it is the claim that ties the Lean model to the Rust source. Until a +> third party re-runs `extract.sh` at the pinned Charon/Aeneas commits and +> obtains the four `model_integrity_sha256` hashes, the correspondence between +> `fips205-source@c945821` and `verification/gen/SlhVerify/*.lean` rests on the +> author's attestation alone. + +The reviewer's instruction on condition 9: if a third party later succeeds at +`extract.sh`, sentence 9 is to be **replaced with a statement of what was +reproduced, by whom, on what platform and at which commits — not deleted.** + +--- + +## Status of condition 9 as of 2026-07-28 + +Still open. Two independent reviewers have now been unable to close it for +different environmental reasons: one sandbox blocks `static.rust-lang.org` and +`opam.ocaml.org` so Charon and Aeneas cannot be built there; the other declined +the task of building the two pinned tools from source. The claim therefore +remains author-attested only, exactly as condition 9 states. diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json index b576c48..2cbb2e1 100644 --- a/verification/PROVENANCE.json +++ b/verification/PROVENANCE.json @@ -45,9 +45,12 @@ "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f" }, "harness_integrity_sha256": { - "_comment": "The harness is part of the trusted computing base. check.sh shells out to lean-guard for every compile (round-5 NEW-3: stubbing it alone yielded ALL GREEN in 3.6s over destroyed proofs), and Proofs/Audit.lean is the program that COMPUTES the digest it is judged by (round-6 NEW-7: flipping two fail-closed guards to `unless true` let a repo proving False pass with the digest BYTE-IDENTICAL \u2014 the digest binds the audit's DATA, never its LOGIC). Both are sha256-pinned by Phase 0, so tampering with either is a build failure rather than a silent green, and any legitimate change is a reviewable pin rotation. STILL trusted and unbound, disclosed in TRUSTED-BASE.md item 11: check.sh itself, ~/aeneas-toolchain/env.sh, $AENEAS_HOME, python3, and the Lean toolchain.", + "_comment": "The harness is part of the trusted computing base and its membership is now SELF-DERIVING: check.sh requires every executable file in verification/ to appear here (round-8 review \u2014 a hardcoded list was itself a second thing to keep in sync), plus Proofs/Audit.lean, which is not executable but computes the digest it is judged by. check.sh itself is excluded: it cannot pin itself, and is disclosed as trusted-unbound in TRUSTED-BASE.md item 11. Pinning check-selftest.sh matters beyond the button: it is the only artifact demonstrating the gates work, and its assertions have been defective in four consecutive rounds, so weakening it is now a reviewable pin rotation rather than an unnoticed edit.", "lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f", - "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e" + "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e", + "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a", + "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e", + "extract.sh": "2829b863301e1e6677376dd2c948673341e934c81dd55a19ff764f563ff22665" }, "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." } diff --git a/verification/RECORDED-RUN.md b/verification/RECORDED-RUN.md index b0add11..b515704 100644 --- a/verification/RECORDED-RUN.md +++ b/verification/RECORDED-RUN.md @@ -450,3 +450,82 @@ statements, hand-edited models, dropped manifest rows, widened policy, specification folds redefined to the loop, a False-proof in the auditor, a stubbed harness, stray modules, and a shortened pin map. ``` + +## Round-8 — author-agent run, 20260728T124039Z, proof repo @ (this commit) + +Captured with `tee`. The third reviewer independently ran check.sh and +check-selftest.sh to green at 1bc4f39 on its own hardware and toolchain, and +recomputed the audit digest outside check.sh — see ATTESTATION-BASIS.md. +PIN ROTATIONS: harness_integrity_sha256 GAINS check-selftest.sh, drill.sh and +extract.sh (the harness set is now self-derived from the executable bit); +check-selftest.sh re-pinned twice during this round as it was edited. No model +pin rotated; the audit digest is unchanged at d83e297a…. + +### check.sh +``` +fips205-slhdsa-verified — check +=============================== +=== Phase 0: build hygiene + model/harness integrity === + ✓ Proofs/Audit.lean + ✓ check-selftest.sh + ✓ drill.sh + ✓ extract.sh + ✓ 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 (17 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/) +✓ attack 16 rejected (Phase 0 purges every .olean under verification/, so an + orphan compiled module with no source cannot satisfy an import) +✓ attack 17 rejected (Phase 0 pins Audit.lean — its LOGIC cannot be silently switched off) +✓ attack 18 rejected (the pin map cannot be silently shortened — required names are in check.sh) +✓ check 15 passed (the hashed block carries all 12 reference-fold bodies, + including the recursive _f companions and their extracted-primitive calls) + +SELFTEST GREEN: 17 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, stray modules, and a shortened pin map. +``` diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index 88c1a50..074606b 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -36,9 +36,18 @@ HERE="$(cd "$(dirname "$0")" && pwd)" cd "$HERE" source ~/aeneas-toolchain/env.sh +# Backups live OUTSIDE verification/. Round-8 added a self-deriving harness rule: +# every executable file in this directory must be pinned. `cp -p` preserves the +# executable bit, so an in-tree `check.sh.sfbak` would look like an unpinned +# harness file and fail the run for a reason unrelated to the attack — the +# defect class this suite exists to catch. +SFBAK="$(mktemp -d)" 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=(); } +save() { cp -p "$1" "$SFBAK/$(printf %s "$1" | tr / _)"; BAKS+=("$1"); } +restore() { for f in "${BAKS[@]:-}"; do + b="$SFBAK/$(printf %s "$f" | tr / _)" + [ -f "$b" ] && cp -p "$b" "$f" && rm -f "$b" + done; BAKS=(); } # Proofs/Audit.lean is sha256-pinned by Phase 0 since round 6 (NEW-7). An attack # that mutates the audit's DATA must therefore ALSO rotate that pin, otherwise it # is stopped by the byte pin and never reaches the mechanism it means to test — @@ -56,6 +65,7 @@ PY } cleanup() { restore + rm -rf "$SFBAK" 2>/dev/null rm -f Proofs/Stray.lean Proofs/EvilSpec.lean Evil.lean Evil.olean \ Proofs/*.olean gen/SlhVerify/*.olean *.olean .audit-manifest.observed 2>/dev/null return 0 @@ -342,8 +352,12 @@ del d["harness_integrity_sha256"] json.dump(d, open(p, "w"), indent=2); open(p, "a").write("\n") PY ./check.sh > /tmp/sf18.out 2>&1 && fail "ATTACK 18 SUCCEEDED: the harness pins were deleted and the button stayed GREEN!" /tmp/sf18.out -grep -q "pin map INCOMPLETE" /tmp/sf18.out || fail "ATTACK 18: rejected but not via the pin-map completeness check" /tmp/sf18.out -grep -q "Proofs/Audit.lean" /tmp/sf18.out || fail "ATTACK 18: rejected but did not name the missing pin" /tmp/sf18.out +# The diagnostic is "UNPINNED harness file" since round 8, when the required set +# became self-deriving from the executable bit: deleting the map now reports ALL +# five harness entries as unpinned, not just the two that used to be hardcoded. +grep -q "UNPINNED harness file" /tmp/sf18.out || fail "ATTACK 18: rejected but not via the pin-map completeness check" /tmp/sf18.out +grep -q "Proofs/Audit.lean" /tmp/sf18.out || fail "ATTACK 18: rejected but did not name the audit driver" /tmp/sf18.out +grep -q "lean-guard" /tmp/sf18.out || fail "ATTACK 18: rejected but did not name lean-guard" /tmp/sf18.out restore echo "✓ attack 18 rejected (the pin map cannot be silently shortened — required names are in check.sh)" diff --git a/verification/check.sh b/verification/check.sh index 4ced28a..e39f617 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -75,7 +75,7 @@ fi # 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; } +python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "INTEGRITY FAILED (a pinned file differs from PROVENANCE.json, or a required file is unpinned — see the specific line above)"; 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 not k.startswith("_")} @@ -92,15 +92,27 @@ bad = 0 # proving False, digest byte-identical. The model side self-protected only # because the gen/ set assertion below derives its requirement from the # filesystem; the harness side had no such cross-check. -REQUIRED = { - "lean-guard", "Proofs/Audit.lean", - "gen/SlhVerify/Types.lean", "gen/SlhVerify/Funs.lean", - "gen/SlhVerify/TypesExternal.lean", "gen/SlhVerify/FunsExternal.lean", +# SELF-DERIVING, so a NEW harness file cannot be forgotten. Round-8 review +# observed that a hardcoded list is itself a second thing to keep in sync, and +# supplied the natural boundary the harness does have: THE EXECUTABLE BIT. Every +# executable file in verification/ is something this script can shell out to, so +# every one must be pinned; a new script therefore fails closed until it is. +# check.sh is excluded because it cannot pin itself — it is the root of trust, +# and TRUSTED-BASE.md item 11 says so. Proofs/Audit.lean is added explicitly: it +# is not executable but it computes the digest it is judged by. +# Backup files are excluded by extension only because check-selftest.sh keeps its +# backups OUTSIDE this directory now; nothing here is expected to match. +harness = { + f for f in os.listdir(here) + if os.path.isfile(os.path.join(here, f)) + and os.access(os.path.join(here, f), os.X_OK) + and f != "check.sh" } -missing = REQUIRED - set(files) +harness.add("Proofs/Audit.lean") +missing = harness - set(files) if missing: for m in sorted(missing): - print(f" ✗ pin map INCOMPLETE — no entry for {m}") + print(f" ✗ UNPINNED harness file (executable, or the audit driver): {m}") bad = 1 for rel, want in sorted(files.items()): p = os.path.join(here, rel)