diff --git a/README.md b/README.md index cb29a5b..12ce726 100644 --- a/README.md +++ b/README.md @@ -5,22 +5,53 @@ 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: THE APEX IS PROVEN — the verify-path pyramid is complete (11 certificates) +## STATUS: eleven certificates over the extracted verify model (external review round 1 applied) `verification/check.sh` is **green** (exit 0): the model compiles, the -proofs compile, and the axiom audit passes. **Eleven theorems across seven -layers — chain (5), WOTS+ (8), XMSS (10), hypertree (12), FORS (17), -input-prep (2/3/4), and the apex (20): `fips205.slh_verify_128s_accepts_iff` -— the deployed SLH-DSA-SHA2-128s verifier returns `ok true` if and only if -the recomputed hypertree root byte-equals the pinned public-key root. Its -`#print axioms` cone is exactly `[propext, Classical.choice, Quot.sound]` -plus the five SHA-2 oracles, nothing else. Honest scope: the apex is an -acceptance characterization (accept = root equality over the extracted -recomputation, whose every loop is individually fidelity-certified by the -ten preceding theorems); it does not restate the recomputation as a -closed-form mathematical hypertree value. After de-plumbing rounds 1+2 the -model carries no plumbing axioms on the verify path — its external surface -is exactly the five SHA-2 oracles (plus off-path zeroize impls).** +proofs compile, and the axiom audit passes (the Phase-3 parser was rewritten +to be fail-closed and wrap-safe after external review round 1, 2026-07-24). + +**What is actually established** — eleven Lean theorems about the +Aeneas-generated model of the **monomorphic `verify_mono` compatibility +verify path** (an additive, `#![allow(dead_code)]` re-expression of the +deployed generic verifier, using named hash oracles because Charon/Aeneas +cannot translate the deployed `Hashers` function-pointer struct): + +- **Ten loop-fidelity theorems** (chain 5, WOTS+ 8, XMSS 10, hypertree 12, + FORS-inner/outer 17, and the input-prep helpers to_int/to_byte/checksum/ + base_2b-outer, Alg 2/3/4). Each equates one *generated* Aeneas loop with an + explicit hand-written recursive fold — a local control-flow correspondence, + not an Algorithm-level mathematical specification. +- **The apex, `fips205.slh_verify_128s_accepts_iff`** — the extracted + `verify_mono::slh_verify_128s` returns `ok true` **iff** the recomputed + hypertree root byte-equals `pk.pk_root`. This is an *acceptance + characterization*: there is no acceptance path other than root equality + over the extracted recomputation. Its `#print axioms` cone is exactly + `[propext, Classical.choice, Quot.sound]` + the five SHA-2 oracles. + +**What is NOT (yet) established — do not overclaim:** +- **The apex proof does not compose the ten loop theorems.** It is a + *structural factorization* of the extracted verifier around its final + equality check; it references none of the ten (it would remain provable if + one were deleted). The ten are independent local-fidelity lemmas, not links + in the apex's proof chain. +- **Not "every loop":** `base_2b`'s inner accumulation loop + (`helpers.base_2b_loop0_loop0`) is threaded *opaquely* and has no + certificate — and it determines the FORS indices / WOTS digits, so a defect + there could change the recomputed root while all eleven theorems still hold. +- **Not the deployed public verifier:** the proved subject is the private + `verify_mono` facade; the bridge to upstream's generic `pk.verify()` is the + finite in-snapshot **differential test**, not a machine-checked refinement. +- **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. + +This is a real **intermediate** verification layer, not an end-to-end +formal verification of the deployed verifier. After de-plumbing rounds 1+2 +the model carries no plumbing axioms on the verify path — its external +surface is exactly the five SHA-2 oracles (plus off-path zeroize impls). +The trust base and residual assumptions are stated in +[TRUSTED-BASE.md](TRUSTED-BASE.md). - **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the extracted `chain_free` loop equals the explicit s-fold hash chain, with diff --git a/verification/Proofs/ApexSpec.lean b/verification/Proofs/ApexSpec.lean index ed05e85..8d9cf1d 100644 --- a/verification/Proofs/ApexSpec.lean +++ b/verification/Proofs/ApexSpec.lean @@ -1,19 +1,34 @@ /- Proofs/ApexSpec.lean — the APEX certificate. - THEOREM slh_verify_128s_accepts_iff: the extracted top-level verifier - slh_verify_128s returns `ok true` if and only if the recomputed hypertree - root byte-equals the pinned public-key root pk.pk_root. Everything the - verifier does after recomputing the root is exactly that byte comparison — - there is no other acceptance path. The recomputation `slhVerifyRoot` is the - extracted pipeline (H_msg digest → md/idx_tree/idx_leaf split via to_int and - masks → fors_pk_from_sig → ht recompute over xmss over wots over chain), - whose every loop is individually fidelity-certified by the ten preceding - theorems. #print axioms = kernel + the five SHA-2 oracles, nothing else. + THEOREM slh_verify_128s_accepts_iff: the extracted verifier + `verify_mono::slh_verify_128s` (a private, additive, `#![allow(dead_code)]` + monomorphic re-expression of the deployed generic verify path — NOT the + public `pk.verify()`, which it is not called by) returns `ok true` if and + only if the recomputed hypertree root byte-equals the pinned public-key root + pk.pk_root. Everything the verifier does after recomputing the root is + exactly that byte comparison — there is no other acceptance path. The + recomputation `slhVerifyRoot` is the extracted pipeline (H_msg digest → + md/idx_tree/idx_leaf split → fors_pk_from_sig → ht recompute over xmss over + wots over chain). #print axioms = kernel-3 + the five SHA-2 oracles. + + SCOPE — what this does NOT establish (external review round 1, 2026-07-24): + • This proof is a STRUCTURAL FACTORIZATION, not a composition. It does NOT + invoke any of the ten loop-fidelity theorems (chain_free_loop_eq, …, + base2b_outer_loop_eq); it would remain provable if one were deleted. Those + ten are independent local-fidelity lemmas, not links in this proof chain. + • NOT "every loop": `base_2b`'s inner accumulation loop is threaded opaquely + and has no certificate — yet it determines the FORS indices / WOTS digits, + so a defect there could change the recomputed root while this theorem holds. + • NOT the deployed public verifier: the bridge from `verify_mono` to the + generic `pk.verify()` is the finite in-snapshot differential test, not a + machine-checked refinement. + • NOT closed-form FIPS 205 correctness: the folds are transliterations of the + extracted loops with the hash primitives opaque. The one real lemma is arrayEqU8_spec: the library array equality `PartialEqArray.eq PartialEqU8` on two Array U8 N returns exactly the decidable byte-equality of their underlying lists (a List.allM induction). - Everything else is unfolding the straight-line composition and threading the + Everything else is unfolding the extracted verifier and threading the recomputation identically on both sides with bind_congr. -/ import Proofs.InputPrepSpec @@ -184,9 +199,12 @@ theorem slh_verify_internal_accepts_iff {A D HP K LEN N : Std.Usize} (H M : Std. -- (no whnf of the nested ht_verify_free_loop — the ForsOuter lesson). simp only [ht_verify_free_split, bind_assoc] -/-- **APEX (deployed SHA2-128s entry).** slh_verify_128s accepts iff the - recomputed root byte-equals pk.pk_root. Composes all ten loop-fidelity - certificates through the extracted pipeline. -/ +/-- **APEX (SHA2-128s facade entry).** The extracted `verify_mono::slh_verify_128s` + accepts iff the recomputed root byte-equals pk.pk_root. Acceptance + characterization only — see the file header for the four explicit + non-claims (this is a structural factorization, NOT a composition of the + ten loop certs; NOT the deployed public verifier; base_2b inner uncertified; + NOT closed-form FIPS-205 correctness). -/ theorem slh_verify_128s_accepts_iff (mprime : Slice Std.U8) (sig : types.SlhDsaSig 12#usize 7#usize 9#usize 14#usize 35#usize 16#usize) diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index 83e8234..fe827d6 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -1,18 +1,24 @@ #!/usr/bin/env bash # Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit -# that cannot fail is theater). Two attacks, both MUST make check.sh fail: +# that cannot fail is theater). Three attacks, all MUST make check.sh fail: # # 1. DEAD FILE — a stray Proofs/*.lean not in the manifest. -# 2. SMUGGLED AXIOM — a certificate whose cone contains an axiom outside -# {kernel-3} ∪ {the five SHA-2 oracles}. +# 2. SMUGGLED AXIOM (short cone) — an axiom outside {kernel-3} ∪ {5 oracles}, +# on the FIRST line of the cone. +# 3. SMUGGLED AXIOM (WRAPPED cone) — an axiom on a CONTINUATION line of a +# cone that wraps (the exact fail-open exploit external review found on +# 2026-07-24: the old single-line parser saw only line 1). This attack +# guards the flattened-parse fix; a self-test that only plants short cones +# cannot detect a wrapped-cone parser regression. # -# Green here means: the gates genuinely reject both. Self-cleaning. +# Green here means: the gates genuinely reject all three. Self-cleaning. set -euo pipefail HERE="$(cd "$(dirname "$0")" && pwd)" cd "$HERE" cleanup() { rm -f Proofs/Stray.lean Proofs/Stray.olean Proofs/EvilSpec.lean \ - Proofs/EvilSpec.olean check-evil-tmp.sh; } + Proofs/EvilSpec.olean Proofs/EvilWrapSpec.lean \ + Proofs/EvilWrapSpec.olean check-evil-tmp.sh check-evilwrap-tmp.sh; } trap cleanup EXIT echo "check-selftest: attacking the gates" @@ -54,7 +60,46 @@ if ./check-evil-tmp.sh > /tmp/selftest-evil.out 2>&1; then fi grep -q "DISALLOWED" /tmp/selftest-evil.out \ || { echo "✗ ATTACK 2: failed, but not via the axiom gate"; exit 1; } +rm -f Proofs/EvilSpec.lean Proofs/EvilSpec.olean check-evil-tmp.sh echo "✓ attack 2 rejected (axiom gate works)" +# ── Attack 3: smuggled axiom on a WRAPPED cone (the fail-open exploit) ─────── +# evil_wrapped_thm bundles a disallowed axiom with the apex theorem, so its cone +# is 9 axioms and WRAPS across physical lines with review_evil_ax on a +# continuation line — exactly what the old single-line parser missed. +cat > Proofs/EvilWrapSpec.lean <<'EOF' +import Proofs.ApexSpec +open Aeneas Aeneas.Std Result +open fips205 +axiom review_evil_ax : True +theorem evil_wrapped_thm + (mprime : Slice Std.U8) + (sig : types.SlhDsaSig 12#usize 7#usize 9#usize 14#usize 35#usize 16#usize) + (pk : types.SlhPublicKey 16#usize) : + True ∧ (verify_mono.slh_verify_128s mprime sig pk + = (do let root ← slhVerifyRoot 63#usize 30#usize mprime sig pk + ok (decide (root.val = pk.pk_root.val)))) := + ⟨review_evil_ax, slh_verify_128s_accepts_iff mprime sig pk⟩ +EOF +python3 - <<'PY' +s = open("check.sh").read() +assert 'PROOFS=(\n' in s and 'CERTS=(\n' in s, "check.sh array shape changed" +s = s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilWrapSpec"\n', 1) +s = s.replace('CERTS=(\n', 'CERTS=(\n "evil_wrapped_thm"\n', 1) +assert '{ echo "import Proofs.ChainSpec"' in s, "check.sh audit import shape changed" +s = s.replace('{ echo "import Proofs.ChainSpec"', + '{ echo "import Proofs.EvilWrapSpec"; echo "import Proofs.ChainSpec"', 1) +open("check-evilwrap-tmp.sh","w").write(s) +PY +chmod +x check-evilwrap-tmp.sh +if ./check-evilwrap-tmp.sh > /tmp/selftest-evilwrap.out 2>&1; then + echo "✗ ATTACK 3 SUCCEEDED: audit passed a smuggled axiom on a WRAPPED cone (fail-open!)"; exit 1 +fi +grep -q "DISALLOWED" /tmp/selftest-evilwrap.out \ + || { echo "✗ ATTACK 3: failed, but not via the axiom gate (wrapped-cone parse?)"; exit 1; } +grep -q "review_evil_ax" /tmp/selftest-evilwrap.out \ + || { echo "✗ ATTACK 3: rejected, but the audit did not name the continuation-line axiom"; exit 1; } +echo "✓ attack 3 rejected (wrapped-cone axiom gate works — the continuation-line axiom was seen)" + echo -echo "SELFTEST GREEN: both gates genuinely reject their attacks." +echo "SELFTEST GREEN: all three gates genuinely reject their attacks." diff --git a/verification/check.sh b/verification/check.sh index 95f92e0..4ef6d44 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -90,20 +90,29 @@ AUD="$HERE/Proofs/.audit.lean" } > "$AUD" OUT=$(lake env bash -c "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' 'Proofs/.audit.lean'" 2>&1) rm -f "$AUD" +# CRITICAL: Lean WRAPS long axiom cones across physical lines. A per-line parse +# silently drops continuation-line axioms (fail-OPEN — external review round 1, +# 2026-07-24, demonstrated a smuggled axiom on line 2 passing). FLATTEN the whole +# report first, then extract each cert's complete bracketed cone with a +# literal-string (regex-safe) scan and subset-check it. Missing/empty report => +# fail-CLOSED. +FLAT=$(echo "$OUT" | tr '\n' ' ' | tr -s ' ') fail=0 for c in "${CERTS[@]}"; do - line=$(echo "$OUT" | grep -F "'$c' depends on axioms:" || true) - if [ -z "$line" ]; then echo " ✗ $c — no axiom report"; fail=1; continue; fi - cone=$(echo "$line" | sed "s/.*depends on axioms: //") - # every axiom in the cone must be in ALLOWED - bad=$(echo "$cone" | tr -d '[]' | tr ',' '\n' | sed 's/^ *//;s/ *$//' | while read -r ax; do + marker="'$c' depends on axioms: [" + if ! grep -qF "$marker" <<<"$FLAT"; then + echo " ✗ $c — no axiom report (fail-closed)"; fail=1; continue + fi + # full cone between this cert's '[' and the next ']' (literal index, not regex) + cone=$(awk -v m="$marker" '{ i=index($0,m); if(i>0){ r=substr($0,i+length(m)); j=index(r,"]"); if(j>0) print substr(r,1,j-1) } }' <<<"$FLAT") + bad=$(echo "$cone" | tr ',' '\n' | sed 's/^ *//;s/ *$//' | while read -r ax; do [ -z "$ax" ] && continue case " propext Classical.choice Quot.sound verify_mono.oracle.f verify_mono.oracle.h verify_mono.oracle.t_l verify_mono.oracle.t_len verify_mono.oracle.h_msg " in *" $ax "*) ;; *) echo "$ax" ;; esac done) - if [ -n "$bad" ]; then echo " ✗ $c — DISALLOWED axioms: $bad"; fail=1 - else echo " ✓ $c cone ⊆ allowed"; fi + if [ -n "$bad" ]; then echo " ✗ $c — DISALLOWED axioms: $(echo $bad | tr '\n' ' ')"; fail=1 + else echo " ✓ $c cone ⊆ allowed ($(echo "$cone" | tr ',' '\n' | grep -c .) axioms audited)"; fi done [ "$fail" = 0 ] || { echo "AXIOM AUDIT FAILED"; exit 1; } diff --git a/verification/gen/SlhVerify/FunsExternal.lean b/verification/gen/SlhVerify/FunsExternal.lean index 526d8fd..d1b7646 100644 --- a/verification/gen/SlhVerify/FunsExternal.lean +++ b/verification/gen/SlhVerify/FunsExternal.lean @@ -23,11 +23,14 @@ Debug-fmt axioms were ELIMINATED at source level by the fips205-source de-plumbing patch (8 sites, semantics identical, differential-test-validated) and their declarations deleted here - (dead-stub rule, 2026-07-23). Remaining as axioms: the Take - iterator machinery used by helpers::to_int (slh_verify_internal's - digest split — the apex round's de-plumbing item) and the zeroize - blanket impls (never on the verify path). The #print axioms audit - confirms only class (1) survives in any certificate cone. + (dead-stub rule, 2026-07-23). De-plumbing round 2 (2026-07-24) then + removed the LAST iterator adapters: helpers::to_int's Take and base_2b's + 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. ────────────────────────────────────────────────────────────────────────────── -/ -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. import Aeneas