mirror of
https://github.com/saymrwulf/fips205-slhdsa-verified.git
synced 2026-09-03 19:53:49 +00:00
mrwulf
eb1d9f108a
External review (both standing reviewers, 2026-07-24) returned DO NOT ATTEST.
The eleven Lean theorems compile with genuinely clean cones (both reviewers
independently reconstructed them), but two real defects were found and are
fixed here.
FIX 1 — the axiom audit was FAIL-OPEN (the critical blocker). check.sh Phase 3
grepped a single physical line of each `#print axioms` report; Lean WRAPS long
cones across lines, so for ht/fors_outer/APEX the audit checked only `[propext,`
and silently ignored the continuation lines — a disallowed axiom on line 2+
passed (the GPT reviewer demonstrated `review_evil_ax` passing). Since check.sh
is the sole source of the word "proven", this is unacceptable.
- New parser: FLATTEN the whole report (join newlines) BEFORE parsing, then
extract each certificate's complete bracketed cone with a literal-string
(regex-safe) scan and subset-check every axiom. Missing/empty report => FAIL
CLOSED. The audit now prints the count of axioms actually audited per cert
(apex: 8, previously 1).
- check-selftest.sh gains ATTACK 3: a smuggled axiom bundled with the apex so
its cone WRAPS with the evil axiom on a continuation line — the exact
exploit. Verified: all three attacks now rejected, attack 3 via the axiom
gate naming the continuation-line axiom. (Also fixed attack 2's leftover
EvilSpec.lean tripping attack 3's dead-file gate.)
FIX 2 — remove the overclaimed framing (refuted by both reviewers). Corrected
in README, the ApexSpec header + apex docstring, and (separately) the control
MANIFEST:
- "composes all ten loop-fidelity certificates" — FALSE. The apex proof is a
STRUCTURAL FACTORIZATION; it references NONE of the ten (grep: 0) and would
remain provable if one were deleted. They are independent local-fidelity
lemmas, not links in the apex proof.
- "every loop is individually fidelity-certified" — FALSE. base_2b's inner
accumulation loop is threaded opaquely and uncertified — and it determines
the FORS indices / WOTS digits, so a defect there could change the recomputed
root while all eleven theorems still hold.
- "the deployed verifier" — the proved subject is verify_mono, a private
#![allow(dead_code)] monomorphic facade NOT called by the public API; the
bridge to the deployed generic verifier is the finite differential test,
not a machine-checked refinement.
- "verify-path pyramid complete" — replaced with "intermediate verification
layer"; the apex is an ACCEPTANCE CHARACTERIZATION, not closed-form FIPS-205
correctness.
Also: FunsExternal header noted the Take axiom "remains" (stale — deleted in
de-plumbing round 2); corrected.
check.sh green over all eleven certificates under the fixed fail-closed parser
(exit 0, 8 axioms audited for the apex). Nothing about the theorems changed —
they were and are sound; only the audit tool and the claims about them are fixed.
NOT DONE (remaining reviewer blockers, tracked): reproducible extract tuple
(pin commits, de-hard-code extract.sh) + Cargo.lock / toolchain pin. Attestation
remains gated behind review round 2 + the operator halt + the appeal.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
218 lines
10 KiB
Text
218 lines
10 KiB
Text
/- Proofs/ApexSpec.lean — the APEX certificate.
|
||
|
||
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 extracted verifier and threading the
|
||
recomputation identically on both sides with bind_congr.
|
||
-/
|
||
import Proofs.InputPrepSpec
|
||
open Aeneas Aeneas.Std Result
|
||
open fips205
|
||
|
||
set_option maxHeartbeats 4000000
|
||
|
||
namespace fips205
|
||
|
||
/- ── the array-equality spec ───────────────────────────────────────────────── -/
|
||
|
||
/-- The `PartialEqU8` instance's `eq` reduces to decidable byte equality (both
|
||
`impls.PartialEqU8.eq` and `liftFun2` are `@[reducible]`). -/
|
||
theorem byteEq (a b : Std.U8) :
|
||
(core.cmp.PartialEqU8).eq a b = ok (decide (a = b)) := rfl
|
||
|
||
/-- allM of the byte-eq predicate over a zip = the decidable list equality,
|
||
when the two lists have equal length. -/
|
||
theorem allM_byteEq : ∀ (l1 l2 : List Std.U8), l1.length = l2.length →
|
||
List.allM (fun p : Std.U8 × Std.U8 => (core.cmp.PartialEqU8).eq p.1 p.2) (l1.zip l2)
|
||
= ok (decide (l1 = l2)) := by
|
||
intro l1
|
||
induction l1 with
|
||
| nil =>
|
||
intro l2 h
|
||
cases l2 with
|
||
| nil => rfl
|
||
| cons y ys => simp at h
|
||
| cons x xs ih =>
|
||
intro l2 h
|
||
cases l2 with
|
||
| nil => simp at h
|
||
| cons y ys =>
|
||
have hlen : xs.length = ys.length := by simp only [List.length_cons] at h; omega
|
||
simp only [List.zip_cons_cons]
|
||
by_cases hxy : x = y
|
||
· subst hxy
|
||
simp only [List.allM, core.cmp.PartialEqU8, core.cmp.impls.PartialEqU8.eq, liftFun2,
|
||
decide_true, bind_ok, reduceIte]
|
||
rw [ih ys hlen]; congr 1; simp [List.cons.injEq]
|
||
· have hp : (pure false : Result Bool) = ok false := rfl
|
||
simp [List.allM, core.cmp.impls.PartialEqU8.eq, liftFun2, hxy, List.cons.injEq, hp]
|
||
|
||
/-- **The library array equality on `Array U8 N` is byte equality.** -/
|
||
theorem arrayEqU8_spec {N : Std.Usize} (a b : Array Std.U8 N) :
|
||
core.array.equality.PartialEqArray.eq core.cmp.PartialEqU8 a b
|
||
= ok (decide (a.val = b.val)) := by
|
||
unfold core.array.equality.PartialEqArray.eq
|
||
have hlen : a.length = b.length := by
|
||
simp only [Array.length, a.property, b.property]
|
||
simp only [hlen, if_true]
|
||
exact allM_byteEq a.val b.val (by simpa only [Array.length] using hlen)
|
||
|
||
/- ── the composition: factor the final root comparison out of ht_verify ─────── -/
|
||
|
||
/-- ht_verify_free's recomputation up to (but excluding) the final root
|
||
comparison: the XMSS node then the hypertree layer walk. -/
|
||
noncomputable def htVerifyRoot {D HP LEN N : Std.Usize}
|
||
(m : Slice Std.U8) (sig_ht : types.HtSig D HP LEN N) (pk_seed : Slice Std.U8)
|
||
(idx_tree : Std.U64) (idx_leaf : Std.U32) : Result (Array Std.U8 N) := do
|
||
let d32 ← lift (UScalar.cast .U32 D)
|
||
let hp32 ← lift (UScalar.cast .U32 HP)
|
||
let adrs ← types.Adrs.Insts.CoreDefaultDefault.default
|
||
let adrs1 ← helpers.Adrs.set_tree_address adrs idx_tree
|
||
let xs ← Array.index_usize sig_ht.xmss_sigs 0#usize
|
||
let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs
|
||
let node ← verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp m pk_seed adrs1
|
||
verify_mono.ht_verify_free_loop { start := 1#u32, «end» := d32 }
|
||
sig_ht.xmss_sigs pk_seed idx_tree hp32 adrs1 node
|
||
|
||
/-- ht_verify_free = recompute the root, then accept iff it byte-equals pk_root. -/
|
||
theorem ht_verify_free_split {D HP LEN N : Std.Usize}
|
||
(m : Slice Std.U8) (sig_ht : types.HtSig D HP LEN N) (pk_seed : Slice Std.U8)
|
||
(idx_tree : Std.U64) (idx_leaf : Std.U32) (pk_root : Array Std.U8 N) :
|
||
verify_mono.ht_verify_free m sig_ht pk_seed idx_tree idx_leaf pk_root
|
||
= (do let node ← htVerifyRoot m sig_ht pk_seed idx_tree idx_leaf
|
||
ok (decide (node.val = pk_root.val))) := by
|
||
unfold verify_mono.ht_verify_free htVerifyRoot
|
||
simp only [bind_assoc]
|
||
apply bind_congr; intro d32
|
||
apply bind_congr; intro hp32
|
||
apply bind_congr; intro adrs
|
||
apply bind_congr; intro adrs1
|
||
apply bind_congr; intro xs
|
||
apply bind_congr; intro sig_tmp
|
||
apply bind_congr; intro node
|
||
apply bind_congr; intro node1
|
||
exact arrayEqU8_spec node1 pk_root
|
||
|
||
/-- The full SLH-DSA recomputation up to the hypertree root: H_msg digest,
|
||
the md/idx_tree/idx_leaf split, FORS pk, then the hypertree recompute.
|
||
Byte-for-byte the extracted slh_verify_internal_free, with only the final
|
||
ht_verify_free replaced by htVerifyRoot (comparison factored out). -/
|
||
noncomputable def slhVerifyRoot {A D HP K LEN N : Std.Usize} (H M : Std.Usize)
|
||
(mprime : Slice Std.U8) (sig : types.SlhDsaSig A D HP K LEN N) (pk : types.SlhPublicKey N) :
|
||
Result (Array Std.U8 N) := do
|
||
let d32 ← lift (UScalar.cast .U32 D)
|
||
let h32 ← lift (UScalar.cast .U32 H)
|
||
let adrs ← types.Adrs.Insts.CoreDefaultDefault.default
|
||
let s ← lift (Array.to_slice sig.randomness)
|
||
let s1 ← lift (Array.to_slice pk.pk_seed)
|
||
let s2 ← lift (Array.to_slice pk.pk_root)
|
||
let digest ← verify_mono.oracle.h_msg M s s1 s2 mprime
|
||
let i ← K * A
|
||
let i1 ← i + 7#usize
|
||
let index1 ← i1 / 8#usize
|
||
let md ←
|
||
core.array.Array.index (core.ops.index.IndexSlice
|
||
(core.slice.index.SliceIndexRangeUsizeSlice Std.U8)) digest
|
||
{ start := 0#usize, «end» := index1 }
|
||
let i2 ← H / D
|
||
let i3 ← H - i2
|
||
let i4 ← i3 + 7#usize
|
||
let i5 ← i4 / 8#usize
|
||
let index2 ← index1 + i5
|
||
let tmp_idx_tree ←
|
||
core.array.Array.index (core.ops.index.IndexSlice
|
||
(core.slice.index.SliceIndexRangeUsizeSlice Std.U8)) digest
|
||
{ start := index1, «end» := index2 }
|
||
let i6 ← 8#usize * D
|
||
let i7 ← H + i6
|
||
let i8 ← i7 - 1#usize
|
||
let i9 ← i8 / i6
|
||
let index3 ← index2 + i9
|
||
let tmp_idx_leaf ←
|
||
core.array.Array.index (core.ops.index.IndexSlice
|
||
(core.slice.index.SliceIndexRangeUsizeSlice Std.U8)) digest
|
||
{ start := index2, «end» := index3 }
|
||
let i10 ← h32 / d32
|
||
let i11 ← h32 - i10
|
||
let i12 ← i11 + 7#u32
|
||
let i13 ← i12 / 8#u32
|
||
let i14 ← helpers.to_int tmp_idx_tree i13
|
||
let i15 ← h32 - i10
|
||
let i16 ← 64#u32 - i15
|
||
let i17 ← core.num.U64.MAX >>> i16
|
||
let idx_tree ← lift (i14 &&& i17)
|
||
let i18 ← 8#u32 * d32
|
||
let i19 ← h32 + i18
|
||
let i20 ← i19 - 1#u32
|
||
let i21 ← i20 / i18
|
||
let i22 ← helpers.to_int tmp_idx_leaf i21
|
||
let i23 ← 64#u32 - i10
|
||
let i24 ← core.num.U64.MAX >>> i23
|
||
let idx_leaf ← lift (i22 &&& i24)
|
||
let adrs1 ← helpers.Adrs.set_tree_address adrs idx_tree
|
||
let adrs2 ← helpers.Adrs.set_type_and_clear adrs1 types.FORS_TREE
|
||
let idx_leaf_u32 ← lift (UScalar.cast .U32 idx_leaf)
|
||
let adrs3 ← helpers.Adrs.set_key_pair_address adrs2 idx_leaf_u32
|
||
let s3 ← lift (Array.to_slice pk.pk_seed)
|
||
let pk_fors ← verify_mono.fors_pk_from_sig_free sig.fors_sig md s3 adrs3
|
||
let s4 ← lift (Array.to_slice pk_fors.key)
|
||
let s5 ← lift (Array.to_slice pk.pk_seed)
|
||
htVerifyRoot s4 sig.ht_sig s5 idx_tree idx_leaf_u32
|
||
|
||
/-- **APEX (generic).** slh_verify_internal_free returns `ok true` iff the
|
||
recomputed hypertree root byte-equals the pinned public-key root — there is
|
||
no acceptance path other than root equality. -/
|
||
theorem slh_verify_internal_accepts_iff {A D HP K LEN N : Std.Usize} (H M : Std.Usize)
|
||
(mprime : Slice Std.U8) (sig : types.SlhDsaSig A D HP K LEN N) (pk : types.SlhPublicKey N) :
|
||
verify_mono.slh_verify_internal_free H M mprime sig pk
|
||
= (do let root ← slhVerifyRoot H M mprime sig pk
|
||
ok (decide (root.val = pk.pk_root.val))) := by
|
||
unfold verify_mono.slh_verify_internal_free slhVerifyRoot
|
||
-- rewriting ht_verify_free's tail into (recompute >>= compare) and flattening
|
||
-- makes both sides the identical do-block; simp closes it structurally
|
||
-- (no whnf of the nested ht_verify_free_loop — the ForsOuter lesson).
|
||
simp only [ht_verify_free_split, bind_assoc]
|
||
|
||
/-- **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)
|
||
(pk : types.SlhPublicKey 16#usize) :
|
||
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))) := by
|
||
unfold verify_mono.slh_verify_128s
|
||
exact slh_verify_internal_accepts_iff 63#usize 30#usize mprime sig pk
|
||
|
||
end fips205
|