saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-04 20:03:44 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
fips205-slhdsa-verified/verification/gen/SlhVerify/FunsExternal.lean
mrwulf dce0473013 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>
2026-07-27 22:57:46 +02:00

171 lines
9 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/- ──────────────────────────────────────────────────────────────────────────────
gen/SlhVerify/FunsExternal.lean — hand-maintained external functions.
TWO CLASSES of external, per honesty invariants H4/H5:
(1) THE CRYPTOGRAPHIC BOUNDARY — the deliberate opaque axioms.
The five SLH-DSA-SHA2-128s hash primitives, reached by name from the
monomorphic verify path (verify_mono::oracle):
· verify_mono.oracle.f — F (chain / FORS leaf)
· verify_mono.oracle.h — H (Merkle node)
· verify_mono.oracle.t_l — T_len (WOTS+ pk compression)
· verify_mono.oracle.t_len — T_k (FORS root compression)
· 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 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
range Step machinery is DISCHARGED below with real definitions
(2026-07-22). The try_from / is_err / &u32-Sub / wots-Take /
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). 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 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.
────────────────────────────────────────────────────────────────────────────── -/
import Aeneas
import SlhVerify.Types
open Aeneas Aeneas.Std Result ControlFlow Error
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false
/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
set_option maxHeartbeats 1000000
/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
set_option maxRecDepth 2048
open fips205
-- (the core::iter::adapters::take::Take::next axiom was here; DELETED
-- 2026-07-24 after de-plumbing round 2 removed the last Take iterator on the
-- verify path — to_int/base_2b now index-loop. dead-stub hygiene rule.)
/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
Visibility: public -/
-- DISCHARGED (2026-07-22, proof phase): Aeneas.Std ships a real `Step`
-- instance only for `usize` (StepUsize); u32 ranges therefore extracted as
-- opaque axioms. These are the FAITHFUL models of Rust's `impl Step for u32`
-- (core/src/iter/range.rs), mirroring StepUsize: forward/backward via
-- u32::try_from(n)-then-checked_{add,sub}; steps_between = saturating
-- difference. Real defs, axiom-clean — so the range-loop cones (chain, and
-- every layer above) carry no plumbing axiom, only the kernel three + the
-- five hash oracles. NOT the deployed hash boundary; ordinary loop control.
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
def U32.Insts.CoreIterRangeStep.backward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32) :=
fun start n =>
if h : n.val < 2 ^ 32 then
ok (Std.U32.checked_sub start (Std.U32.ofNatCore n.val (by omega)))
else ok none
/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_checked]
Visibility: public -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
def U32.Insts.CoreIterRangeStep.forward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32) :=
fun start n =>
if h : n.val < 2 ^ 32 then
ok (Std.U32.checked_add start (Std.U32.ofNatCore n.val (by omega)))
else ok none
/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
Visibility: public -/
@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
def U32.Insts.CoreIterRangeStep.steps_between
: Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize)) :=
fun start end_ =>
if h : start.val > end_.val then ok (0#usize, none)
else
let steps := Std.Usize.ofNatCore (end_.val - start.val) (by scalar_tac)
ok (steps, some steps)
/-- [zeroize::{impl zeroize::Zeroize for Z}::zeroize]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 274:4-274:25
Name pattern: [zeroize::{zeroize::Zeroize<@Z>}::zeroize]
Visibility: public -/
@[rust_fun "zeroize::{zeroize::Zeroize<@Z>}::zeroize"]
axiom zeroize.Zeroize.Blanket.zeroize
{Z : Type} (DefaultIsZeroesInst : zeroize.DefaultIsZeroes Z) : Z → Result Z
/-- [zeroize::{impl zeroize::Zeroize for [Z; N]}::zeroize]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 346:4-346:25
Name pattern: [zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize]
Visibility: public -/
@[rust_fun "zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize"]
axiom Array.Insts.ZeroizeZeroize.zeroize
{Z : Type} {N : Std.Usize} (ZeroizeInst : zeroize.Zeroize Z) :
Array Z N → Result (Array Z N)
/-- [zeroize::__internal::{impl zeroize::__internal::AssertZeroize for T}::zeroize_or_on_drop]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 846:8-846:40
Name pattern: [zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop]
Visibility: public -/
@[rust_fun
"zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop"]
axiom zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
{T : Type} (ZeroizeInst : zeroize.Zeroize T) : T → Result T
/-- [fips205::verify_mono::oracle::f]:
Source: 'src/verify_mono.rs', lines 49:4-51:5 -/
axiom verify_mono.oracle.f
(N : Std.Usize) :
Slice Std.U8 → types.Adrs → Slice Std.U8 → Result (Array Std.U8 N)
/-- [fips205::verify_mono::oracle::h]:
Source: 'src/verify_mono.rs', lines 54:4-56:5 -/
axiom verify_mono.oracle.h
(N : Std.Usize) :
Slice Std.U8 → types.Adrs → Slice Std.U8 → Slice Std.U8 → Result
(Array Std.U8 N)
/-- [fips205::verify_mono::oracle::t_l]:
Source: 'src/verify_mono.rs', lines 60:4-64:5 -/
axiom verify_mono.oracle.t_l
{X : Std.Usize} {N : Std.Usize} :
Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
Std.U8 N)
/-- [fips205::verify_mono::oracle::t_len]:
Source: 'src/verify_mono.rs', lines 69:4-73:5 -/
axiom verify_mono.oracle.t_len
{X : Std.Usize} {N : Std.Usize} :
Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
Std.U8 N)
/-- [fips205::verify_mono::oracle::h_msg]:
Source: 'src/verify_mono.rs', lines 81:4-85:5 -/
axiom verify_mono.oracle.h_msg
(M : Std.Usize) :
Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result
(Array Std.U8 M)
Reference in a new issue View git blame Copy permalink