mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-03 20:13:48 +00:00
Compare commits
2 commits
93d62703f3
...
18e8753a62
| Author | SHA1 | Date | |
|---|---|---|---|
| 18e8753a62 | |||
| 18abd45edb |
9 changed files with 995 additions and 5 deletions
|
|
@ -54,3 +54,59 @@ running Rust code. Everything else is machine-checked.
|
||||||
theorem says what its name — or this document — suggests it says. A
|
theorem says what its name — or this document — suggests it says. A
|
||||||
theorem gutted to a tautology with the same axiom cone would pass every
|
theorem gutted to a tautology with the same axiom cone would pass every
|
||||||
phase. Reading the statements remains a human act.
|
phase. Reading the statements remains a human act.
|
||||||
|
8. **What the statement binding covers.** `check.sh` Phase 3c compiles
|
||||||
|
`Proofs/Audit.lean`, which emits a canonical block containing the policy
|
||||||
|
constants, every certificate's fully-elaborated statement (`pp.all`, so
|
||||||
|
implicit arguments, instances and universe levels are all visible), and the
|
||||||
|
fully-elaborated body of every specification constant transitively
|
||||||
|
reachable from those statements. The SHA-256 of that block is pinned in
|
||||||
|
`check.sh` and the block itself is committed as `AUDIT-MANIFEST.txt`, so a
|
||||||
|
mismatch is diffed rather than merely reported. This is what makes a
|
||||||
|
certificate gutted to a tautology of the same axiom cone fail, and what
|
||||||
|
makes a reference definition redefined to BE the extracted code fail — two
|
||||||
|
attacks that move no cone at all. Phase 0b separately pins the bytes of
|
||||||
|
every extracted-model file under `gen/`, with membership derived from the
|
||||||
|
filesystem so a new model file fails closed.
|
||||||
|
|
||||||
|
**The residue you must still supply yourself.** Three things, stated
|
||||||
|
plainly because a reader would otherwise assume them:
|
||||||
|
|
||||||
|
· *A digest binds identity, not meaning.* The audit proves the statements
|
||||||
|
are the ones that were reviewed. Whether those statements say something
|
||||||
|
worth believing about ed25519 is a question only a human reading them
|
||||||
|
answers. `AUDIT-MANIFEST.txt` is committed precisely so that reading is
|
||||||
|
possible without re-running anything.
|
||||||
|
|
||||||
|
· *An author can rotate the pins.* Editing a statement and refreshing the
|
||||||
|
digest in the same commit passes every phase. The defence is that both
|
||||||
|
changes are visible in the diff, reviewed at the pinned commit — not that
|
||||||
|
the script prevents it. No harness audits its own author.
|
||||||
|
|
||||||
|
· *Phase 0b pins the model; it does not verify the translation.* That the
|
||||||
|
bytes under `gen/` are the reviewed bytes says nothing about whether
|
||||||
|
Charon and Aeneas translated the Rust faithfully. That assumption is
|
||||||
|
item 3 above and is unchanged.
|
||||||
|
|
||||||
|
9. **The harness is pinned, and what that is worth.** `check.sh` Phase 0c
|
||||||
|
requires every executable file under `verification/` — plus the audit
|
||||||
|
driver, the committed manifests and the policy tables, which are not
|
||||||
|
executable and are therefore listed explicitly in the script — to match
|
||||||
|
`HARNESS.sha256`. Membership is derived from the executable bit, so a new
|
||||||
|
script fails the build until someone pins it deliberately, and the required
|
||||||
|
set is computed from the filesystem rather than read out of the pin file,
|
||||||
|
so deleting an entry is a failure rather than a silent un-pinning.
|
||||||
|
`lean-guard` is inside that set: stubbing the memory-capped compiler
|
||||||
|
wrapper is the cheapest known route to a false green, demonstrated
|
||||||
|
elsewhere in this estate as ALL GREEN in 3.6 seconds over deliberately
|
||||||
|
destroyed proofs. `selftest-harness.sh` replays that attack and four
|
||||||
|
others.
|
||||||
|
|
||||||
|
**What it does NOT buy, stated plainly.** Pinning a harness from inside
|
||||||
|
that harness is circular, and no amount of engineering removes the
|
||||||
|
circularity. An author who edits `check.sh` — or `lean-guard`, or the
|
||||||
|
audit driver — and refreshes its pin in the SAME commit passes every
|
||||||
|
phase. What the pin changes is that the edit can no longer be silent: it
|
||||||
|
must appear in the diff, at the commit you are reviewing. That is why the
|
||||||
|
consumer's protection is, and has always been, *review at the pinned
|
||||||
|
commit* rather than the button's own verdict. A green button says "this is
|
||||||
|
the apparatus that was reviewed", never "this apparatus is trustworthy".
|
||||||
|
|
|
||||||
100
verification/AUDIT-MANIFEST.txt
Normal file
100
verification/AUDIT-MANIFEST.txt
Normal file
File diff suppressed because one or more lines are too long
12
verification/GEN-MODEL.sha256
Normal file
12
verification/GEN-MODEL.sha256
Normal file
|
|
@ -0,0 +1,12 @@
|
||||||
|
56f9a263591fa407af38325601f8f090fdeb3d3715a83763f74afc3e9522b612 CurveField/FunsExternal.lean
|
||||||
|
f23af27f3148e8ac6181d077e558d30e73936fc54a1cb3928d70687c1d37c644 CurveField/FunsExternal_Template.lean
|
||||||
|
0b7b818978e3a0274d547d1bcf25634be98c55d813950dc4a541bd7adef60b21 CurveField/Funs.lean
|
||||||
|
d197d7b9fe515863784eeee59a2fbb69735d10ebcf5cc4e03feb3afbeb53a2b7 CurveField/TypesExternal.lean
|
||||||
|
4560fc87c6156df16c34117db0817dc0926709f884728d9ca907985cbf931c6c CurveField/TypesExternal_Template.lean
|
||||||
|
b4bbcff308d2626b37c2cda0c17afb97d95b19fd158fe4842af942f0bbb5b6ad CurveField/Types.lean
|
||||||
|
621111b9d6b946ddc73ed13fbc14a861f6df94ba85eab8338cb5b7e823a2cd72 CurveSig/FunsExternal.lean
|
||||||
|
ee04a32c9f5a5032622ae0d20c6a764eba36a016af21a8ebc1db3740d35d0ccc CurveSig/FunsExternal_Template.lean
|
||||||
|
64fadb72dfce4e64a988b544c4a2182b5240fe95057815e31da93d54bb676ac3 CurveSig/Funs.lean
|
||||||
|
4e2468f2ab255d3e9065d5ad179b412cffd1d7251e716cbe704c36916267c069 CurveSig/TypesExternal.lean
|
||||||
|
16df7ed5eadb054bf78c4abb537adbc03c17f504babfca69a0e0bb7fb81314f0 CurveSig/TypesExternal_Template.lean
|
||||||
|
e6dcaaa1a5d832ea54f4eecff55aa4dabc653f55b3a56cddaaed5feabe671fb9 CurveSig/Types.lean
|
||||||
10
verification/HARNESS.sha256
Normal file
10
verification/HARNESS.sha256
Normal file
|
|
@ -0,0 +1,10 @@
|
||||||
|
c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4 AUDIT-MANIFEST.txt
|
||||||
|
64df281594fd38ac42aa06623839608a7fba74b0d91994c114b55e25a9233a33 check-scalar.sh
|
||||||
|
3259a791ce6996023909e7ea1033d55f73fc2881128787f383daa606c83fb2f1 check.sh
|
||||||
|
c0fd4ba1fdec8a6f37b28b5fbe3fc7e93a54f1365443d365ca44c48c117c56b7 extract.sh
|
||||||
|
d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4 GEN-MODEL.sha256
|
||||||
|
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
||||||
|
79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8 Proofs/Audit.lean
|
||||||
|
79611f9689ba714fb8d3f57aee86ad9655509303445beaad766bf8b049de8c44 selftest-axgate.sh
|
||||||
|
3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh
|
||||||
|
a14acaafe914aabb9df44fcd05fd50d475804280fab9e332fdb5ea0b0d35f164 selftest-statements.sh
|
||||||
236
verification/Proofs/Audit.lean
Normal file
236
verification/Proofs/Audit.lean
Normal file
|
|
@ -0,0 +1,236 @@
|
||||||
|
/- ──────────────────────────────────────────────────────────────────────────
|
||||||
|
Proofs/Audit.lean — statement + specification binding (P1-a).
|
||||||
|
|
||||||
|
WHAT THIS ADDS over check.sh Phases 2b/3/3b. Those establish that each
|
||||||
|
certificate is a theorem and rests on exactly the declared axioms. None
|
||||||
|
of them establishes WHAT THE THEOREM SAYS. A certificate gutted to a
|
||||||
|
tautology keeps its name, its kind, and its axiom cone, and passes every
|
||||||
|
one of them. Worse, the reference definitions the statements are stated
|
||||||
|
AGAINST can be redefined to be the extracted code itself, at which point
|
||||||
|
the certificate says `loop = loop` and every cone is unchanged.
|
||||||
|
|
||||||
|
So this file emits a canonical AUDIT-MANIFEST block covering:
|
||||||
|
· the POLICY constants (both cone tiers, and the module prefix that
|
||||||
|
defines what counts as a specification);
|
||||||
|
· every certificate's fully-elaborated STATEMENT (`pp.all`);
|
||||||
|
· every specification constant transitively reachable from those
|
||||||
|
statements, with its fully-elaborated DEFINITION BODY. A Prop-valued
|
||||||
|
constant contributes its statement rather than its proof term, by
|
||||||
|
proof irrelevance — the proof term is not what fidelity lives in.
|
||||||
|
|
||||||
|
check.sh binds the SHA-256 of that block, and the block itself is
|
||||||
|
committed, so a mismatch can be DIFFED against a reference rather than
|
||||||
|
merely reported.
|
||||||
|
|
||||||
|
TWO TIERS, NOT ONE. This repository has an arithmetic tier that must
|
||||||
|
stay oracle-free and an apex tier that legitimately carries this fork's
|
||||||
|
hash and wire-format axioms. The boundary differs BETWEEN FORKS. A
|
||||||
|
single global allowed-axiom list would silently widen the arithmetic
|
||||||
|
tier to accept hash oracles, which is the most valuable property these
|
||||||
|
repositories have. Hence a per-certificate expected cone below.
|
||||||
|
|
||||||
|
NO HAND-KEPT STATEMENT FINGERPRINTS. The companion SLH-DSA auditor pins
|
||||||
|
a 32-bit `Expr.hash` per certificate as a diagnostic. That table is one
|
||||||
|
more thing that can fall out of sync, and the canonical block already
|
||||||
|
covers every statement at full fidelity — a diff of the block says more
|
||||||
|
than a changed integer does. Membership is derived, not listed.
|
||||||
|
|
||||||
|
STANDING LIMIT: an audit executed by a harness cannot defend against an
|
||||||
|
author who edits that harness. The consumer defence is, and remains, the
|
||||||
|
pinned commit reviewed at the pin.
|
||||||
|
────────────────────────────────────────────────────────────────────────── -/
|
||||||
|
import Proofs.FieldMain
|
||||||
|
import Proofs.EdMain
|
||||||
|
import Proofs.DsmTableSpec
|
||||||
|
import Proofs.DsmStepSpec
|
||||||
|
import Proofs.DsmLoopSpec
|
||||||
|
import Proofs.DsmNafLoadSpec
|
||||||
|
import Proofs.DsmNafMath
|
||||||
|
import Proofs.DsmNafSpec
|
||||||
|
import Proofs.DsmMulSpec
|
||||||
|
import Proofs.ToBytesSpec
|
||||||
|
import Proofs.CompressSpec
|
||||||
|
import Proofs.ScalarPackSpec
|
||||||
|
import Proofs.SigApexSpec
|
||||||
|
import Proofs.PointLiftSpec
|
||||||
|
import Proofs.PointEqSpec
|
||||||
|
import Proofs.DecompressSpec
|
||||||
|
import Proofs.FromBytesSpec
|
||||||
|
import Proofs.DecompressMain
|
||||||
|
import Lean
|
||||||
|
open Lean Elab Command
|
||||||
|
|
||||||
|
namespace Ed25519Audit
|
||||||
|
|
||||||
|
/-- Lean's three kernel axioms. -/
|
||||||
|
def kernel3 : List Name := [`propext, `Classical.choice, `Quot.sound]
|
||||||
|
|
||||||
|
/-- This fork's apex boundary: the hash oracle and wire-format symbols the
|
||||||
|
signature-level certificates are permitted to rest on, and nothing else.
|
||||||
|
POLICY CONSTANT — folded into the digest, so widening it moves the hash
|
||||||
|
and fails the build. -/
|
||||||
|
def apexExtra : List Name :=
|
||||||
|
[`ed25519.Signature, `sha2.Sha512, `verifying.sha512_finalize_bytes, `verifying.sha512_new, `verifying.sha512_update, `ed25519.Signature.to_bytes, `signature.error.Error, `signature.error.Error.new]
|
||||||
|
|
||||||
|
def apexBoundary : List Name := kernel3 ++ apexExtra
|
||||||
|
|
||||||
|
/-- A constant counts as SPECIFICATION if it was declared in a `Proofs.`
|
||||||
|
module — i.e. hand-written by us, as opposed to the extracted model in
|
||||||
|
`gen/` (pinned separately by Phase 0). Derived from the environment, not
|
||||||
|
from a list, so a new specification module cannot appear unnoticed. -/
|
||||||
|
def specPrefix : String := "Proofs."
|
||||||
|
|
||||||
|
/-- Per-certificate expected cone. Arithmetic tier first, apex tier last. -/
|
||||||
|
def manifest : List (Name × List Name) :=
|
||||||
|
[ (`CurveFieldProofs.fieldImplementation, kernel3)
|
||||||
|
, (`CurveFieldProofs.edwardsImplementation, kernel3)
|
||||||
|
, (`CurveFieldProofs.naf_table_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.naf_select_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.proj_double_law, kernel3)
|
||||||
|
, (`CurveFieldProofs.compl_as_projective_law, kernel3)
|
||||||
|
, (`CurveFieldProofs.dsm_step_p_law, kernel3)
|
||||||
|
, (`CurveFieldProofs.dsm_step_b_law, kernel3)
|
||||||
|
, (`CurveFieldProofs.dsm_loop_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.naf_load_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.naf_exit, kernel3)
|
||||||
|
, (`CurveFieldProofs.naf_digit_loop_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.non_adjacent_form_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.run_basepoint, kernel3)
|
||||||
|
, (`CurveFieldProofs.vartime_double_base_mul_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.verify_loop_full, kernel3)
|
||||||
|
, (`CurveFieldProofs.to_bytes_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.ed_compress_spec, kernel3)
|
||||||
|
, (`ScalarProofs.from_bytes_mod_order_wide_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.vartime_dsm_basepoint_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.enc_point_inj, kernel3)
|
||||||
|
, (`CurveFieldProofs.pow_p58_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.fe_ct_eq_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.sqrt_core, kernel3)
|
||||||
|
, (`CurveFieldProofs.sqrt_ratio_i_sq_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.from_bytes_spec, kernel3)
|
||||||
|
, (`CurveFieldProofs.decompress_of_canonical, kernel3)
|
||||||
|
, (`CurveFieldProofs.verify_accepts_iff, apexBoundary)
|
||||||
|
, (`CurveFieldProofs.verify_accepts_iff_point, apexBoundary)
|
||||||
|
, (`CurveFieldProofs.verify_accepts_iff_point_eq, apexBoundary)
|
||||||
|
, (`CurveFieldProofs.verify_accepts_iff_decompress, apexBoundary)
|
||||||
|
]
|
||||||
|
|
||||||
|
/-- Deterministic name ordering for the canonical serialization. -/
|
||||||
|
def sortNames (l : List Name) : List Name :=
|
||||||
|
((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName)
|
||||||
|
|
||||||
|
/-- 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
|
||||||
|
|
||||||
|
/-- Was `n` hand-written by us, in a `Proofs.` module? -/
|
||||||
|
def isSpecConst (env : Environment) (n : Name) : Bool :=
|
||||||
|
match env.getModuleIdxFor? n with
|
||||||
|
| some idx => (toString env.header.moduleNames[idx.toNat]!).startsWith specPrefix
|
||||||
|
| 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 definitions —
|
||||||
|
and any future one — automatically, so a new specification cannot be
|
||||||
|
introduced, or an existing one redefined, 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. Implicit
|
||||||
|
arguments, instances and universe levels are all made visible, so two
|
||||||
|
statements that merely LOOK alike cannot share a rendering. -/
|
||||||
|
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 "auditStatements" : command => do
|
||||||
|
let env ← getEnv
|
||||||
|
let mut errs : Array String := #[]
|
||||||
|
|
||||||
|
-- (0) The manifest may not permit an axiom outside the two declared tiers.
|
||||||
|
-- Without this, widening a cone in the manifest would be invisible.
|
||||||
|
for (cert, cone) in manifest do
|
||||||
|
for a in cone do
|
||||||
|
unless apexBoundary.contains a do
|
||||||
|
errs := errs.push s!"manifest permits {a} for {cert}, which is outside every declared tier"
|
||||||
|
|
||||||
|
-- (1) Each certificate must EXIST, be a THEOREM, and have EXACTLY its cone.
|
||||||
|
-- Exact, not subset: a certificate that stopped depending on the hash
|
||||||
|
-- oracle is as wrong as one that acquired a new axiom.
|
||||||
|
for (cert, expected) in manifest do
|
||||||
|
match env.find? cert with
|
||||||
|
| none => errs := errs.push s!"{cert}: NOT FOUND (renamed or deleted?)"
|
||||||
|
| some (.thmInfo _) =>
|
||||||
|
let got := (← collectAxioms cert).toList
|
||||||
|
let extras := got.filter (fun a => !expected.contains a)
|
||||||
|
let missing := expected.filter (fun a => !got.contains a)
|
||||||
|
unless extras.isEmpty && missing.isEmpty do
|
||||||
|
errs := errs.push s!"{cert}: cone extra={extras} missing={missing}"
|
||||||
|
| 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}: is not a theorem"
|
||||||
|
|
||||||
|
unless errs.isEmpty do
|
||||||
|
throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"
|
||||||
|
|
||||||
|
-- (2) CANONICAL BLOCK: policy, then statements, then specification bodies.
|
||||||
|
let mut lines : Array String := #[]
|
||||||
|
lines := lines.push
|
||||||
|
s!"policy|kernel3={String.intercalate "," ((sortNames kernel3).map toString)}|apexExtra={String.intercalate "," ((sortNames apexExtra).map toString)}|specPrefix={specPrefix}"
|
||||||
|
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 mid-audit: {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, which 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}"
|
||||||
|
|
||||||
|
-- FAIL CLOSED ON ABSENCE: a manifest that somehow produced no specification
|
||||||
|
-- constants would emit a block that binds statements only. That is a weaker
|
||||||
|
-- claim than this file advertises, so it is an error, not a quiet pass.
|
||||||
|
if specs.toList.isEmpty then
|
||||||
|
throwError "AUDIT FAILED: statements reached ZERO specification constants — the closure is not doing its job"
|
||||||
|
|
||||||
|
logInfo ("AUDIT-MANIFEST-BEGIN\n" ++ String.intercalate "\n" lines.toList ++ "\nAUDIT-MANIFEST-END")
|
||||||
|
-- check.sh cross-checks its own CERTS array against THIS line, so the two
|
||||||
|
-- cannot drift apart without the build noticing.
|
||||||
|
logInfo s!"AUDITED-CERTIFICATES: {String.intercalate " " ((manifest.map (·.1)).map toString)}"
|
||||||
|
logInfo s!"statement audit PASSED: {manifest.length} certificates (exact cones + elaborated statements), {specs.toList.length} specification constants pinned"
|
||||||
|
|
||||||
|
end Ed25519Audit
|
||||||
|
|
||||||
|
open Ed25519Audit in
|
||||||
|
auditStatements
|
||||||
|
|
@ -19,6 +19,15 @@
|
||||||
# set of compiled modules does not match the set of shipped sources.
|
# set of compiled modules does not match the set of shipped sources.
|
||||||
# 3. axiom audit: #print axioms for every certificate in CERTS; each must
|
# 3. axiom audit: #print axioms for every certificate in CERTS; each must
|
||||||
# report exactly [propext, Classical.choice, Quot.sound]
|
# report exactly [propext, Classical.choice, Quot.sound]
|
||||||
|
# 3b. signature-apex audit: the four apex certificates against this fork's
|
||||||
|
# documented SHA-512 + wire-format boundary, exactly.
|
||||||
|
# 3c. statement + specification binding: Proofs/Audit.lean emits a canonical
|
||||||
|
# block of the policy constants, every certificate's fully-elaborated
|
||||||
|
# statement, and the body of every specification constant reachable from
|
||||||
|
# those statements. Its SHA-256 is pinned here and the block itself is
|
||||||
|
# committed, so a mismatch is diffable. This is the phase that makes a
|
||||||
|
# gutted statement, or a reference definition redefined to BE the
|
||||||
|
# extracted code, fail — neither moves any axiom cone.
|
||||||
# ─────────────────────────────────────────────────────────────────────────────
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
set -euo pipefail
|
set -euo pipefail
|
||||||
source ~/aeneas-toolchain/env.sh
|
source ~/aeneas-toolchain/env.sh
|
||||||
|
|
@ -79,6 +88,7 @@ PROOFS=(
|
||||||
DecompressSpec
|
DecompressSpec
|
||||||
FromBytesSpec
|
FromBytesSpec
|
||||||
DecompressMain
|
DecompressMain
|
||||||
|
Audit # LAST: imports the certificate corpus and runs the audit
|
||||||
)
|
)
|
||||||
# Fully-qualified certificate names; each must be axiom-clean.
|
# Fully-qualified certificate names; each must be axiom-clean.
|
||||||
CERTS=(
|
CERTS=(
|
||||||
|
|
@ -144,6 +154,89 @@ for f in "$HERE"/gen/CurveField/*.lean "$HERE"/Proofs/*.lean; do
|
||||||
done
|
done
|
||||||
echo " all sources valid"
|
echo " all sources valid"
|
||||||
|
|
||||||
|
# ── Phase 0b: pin the extracted model ───────────────────────────────────────
|
||||||
|
# WHY. The certificates are stated ABOUT the extracted model in gen/. Phase 3c
|
||||||
|
# binds their statements and the specification definitions those statements are
|
||||||
|
# stated against — but a statement mentions an extracted function BY NAME, so
|
||||||
|
# editing that function's BODY changes what the theorem is about while leaving
|
||||||
|
# every statement, every cone and the audit digest byte-identical.
|
||||||
|
#
|
||||||
|
# This is not hypothetical. On 2026-07-28 the risc0 and betrusted repositories
|
||||||
|
# were observed to produce byte-identical AUDIT-MANIFEST digests despite
|
||||||
|
# shipping demonstrably different extracted models (a different operation order
|
||||||
|
# in the point-doubling routine). The statements could not tell them apart.
|
||||||
|
# Only a byte pin can.
|
||||||
|
#
|
||||||
|
# Membership is derived from the filesystem, not from a list: every .lean under
|
||||||
|
# gen/ must appear in GEN-MODEL.sha256 and vice versa, so adding a model file
|
||||||
|
# fails closed rather than passing unnoticed.
|
||||||
|
echo "=== Phase 0b: extracted-model byte pin ==="
|
||||||
|
if [ ! -s "$HERE/GEN-MODEL.sha256" ]; then
|
||||||
|
echo "FATAL: GEN-MODEL.sha256 is missing or empty — the extracted model is unpinned."
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
GEN_OBSERVED=$(cd "$HERE/gen" && find . -name '*.lean' -type f | sed 's|^\./||' | sort)
|
||||||
|
GEN_PINNED=$(awk '{print $2}' "$HERE/GEN-MODEL.sha256" | sort)
|
||||||
|
if [ "$GEN_OBSERVED" != "$GEN_PINNED" ]; then
|
||||||
|
echo "FATAL: the set of extracted-model files does not match GEN-MODEL.sha256."
|
||||||
|
echo " (< pinned, > present on disk)"
|
||||||
|
diff <(echo "$GEN_PINNED") <(echo "$GEN_OBSERVED") | sed 's/^/ /'
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
if ! ( cd "$HERE/gen" && sha256sum -c --quiet "$HERE/GEN-MODEL.sha256" ) ; then
|
||||||
|
echo "FATAL: an extracted-model file does not match its pin. The proofs are"
|
||||||
|
echo "about a model that is no longer the one that was reviewed."
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
echo " $(wc -l < "$HERE/GEN-MODEL.sha256") extracted-model files match their pins"
|
||||||
|
# ── Phase 0c: harness integrity ─────────────────────────────────────────────
|
||||||
|
# WHY. Every gate in this script is executed by a script that, until now,
|
||||||
|
# nothing pinned. Round-5 review of the companion SLH-DSA repository stubbed
|
||||||
|
# the compiler wrapper alone and the button printed ALL GREEN in 3.6 seconds
|
||||||
|
# over deliberately destroyed proofs; flipping two guards in the audit driver
|
||||||
|
# disabled every check with the digest byte-identical. Depth of checking is
|
||||||
|
# worth nothing if the thing doing the checking is unbound.
|
||||||
|
#
|
||||||
|
# WHICH files must be pinned is POLICY, and policy lives here — in the root of
|
||||||
|
# trust — never inside the map being consulted. If the required set were read
|
||||||
|
# from HARNESS.sha256, deleting an entry would silently un-pin the file rather
|
||||||
|
# than failing the build.
|
||||||
|
#
|
||||||
|
# The set is SELF-DERIVING from the executable bit: anything this script can
|
||||||
|
# shell out to must be pinned, so a NEW script fails closed until someone pins
|
||||||
|
# it deliberately. Non-executable files that are nonetheless load-bearing —
|
||||||
|
# the audit driver, the committed manifests, the policy tables — cannot be
|
||||||
|
# discovered that way and are listed explicitly.
|
||||||
|
HARNESS_EXTRA=(
|
||||||
|
AUDIT-MANIFEST.txt # the statement block Phase 3c's digest is taken over
|
||||||
|
GEN-MODEL.sha256 # the extracted-model pins Phase 0b enforces
|
||||||
|
Proofs/Audit.lean # the audit driver: it computes the digest it is judged by
|
||||||
|
)
|
||||||
|
echo "=== Phase 0c: harness integrity ==="
|
||||||
|
if [ ! -s "$HERE/HARNESS.sha256" ]; then
|
||||||
|
echo "FATAL: HARNESS.sha256 is missing or empty — the harness is unpinned."
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
# NOTE ON check.sh ITSELF: it is pinned like everything else. That catches
|
||||||
|
# drift and accident. It does NOT stop an author who edits this script and
|
||||||
|
# refreshes its pin in the same commit — nothing executed by the harness can.
|
||||||
|
# The defence there is that both changes appear in the diff at the pinned
|
||||||
|
# commit, which is why TRUSTED-BASE.md says the consumer's check is review.
|
||||||
|
HARNESS_REQUIRED=$( { find "$HERE" -type f -executable -not -path '*/.git/*' -printf '%P\n'
|
||||||
|
printf '%s\n' "${HARNESS_EXTRA[@]}"; } | sort -u )
|
||||||
|
HARNESS_PINNED=$(awk '{print $2}' "$HERE/HARNESS.sha256" | sort -u)
|
||||||
|
if [ "$HARNESS_REQUIRED" != "$HARNESS_PINNED" ]; then
|
||||||
|
echo "FATAL: the set of harness files does not match HARNESS.sha256."
|
||||||
|
echo " (< pinned, > present and requiring a pin)"
|
||||||
|
diff <(echo "$HARNESS_PINNED") <(echo "$HARNESS_REQUIRED") | sed 's/^/ /'
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
if ! ( cd "$HERE" && sha256sum -c --quiet HARNESS.sha256 ) ; then
|
||||||
|
echo "FATAL: a harness file does not match its pin. The button you are"
|
||||||
|
echo "running is not the button that was reviewed."
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
echo " $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins"
|
||||||
# ── Phase 1: stub + axiom-smuggling audit ───────────────────────────────────
|
# ── Phase 1: stub + axiom-smuggling audit ───────────────────────────────────
|
||||||
echo "=== Phase 1: stub audit ==="
|
echo "=== Phase 1: stub audit ==="
|
||||||
if grep -rn 'by trivial' "$HERE"/Proofs/*Spec*.lean 2>/dev/null; then
|
if grep -rn 'by trivial' "$HERE"/Proofs/*Spec*.lean 2>/dev/null; then
|
||||||
|
|
@ -314,5 +407,103 @@ lake env bash -c "
|
||||||
fi
|
fi
|
||||||
"
|
"
|
||||||
|
|
||||||
|
echo ""
|
||||||
|
# ── Phase 3c: statement + specification binding ─────────────────────────────
|
||||||
|
# WHAT THE EARLIER PHASES DO NOT ESTABLISH. Phase 3 proves each certificate
|
||||||
|
# rests on exactly the declared axioms; 3b does the same for the apex tier.
|
||||||
|
# Neither says WHAT THE THEOREM SAYS. A certificate gutted to a tautology of
|
||||||
|
# the same cone passes both. So does one whose reference definition has been
|
||||||
|
# redefined to BE the extracted code, at which point the theorem reads
|
||||||
|
# `loop = loop` and every cone is byte-identical.
|
||||||
|
#
|
||||||
|
# Proofs/Audit.lean emits a canonical block holding the policy constants,
|
||||||
|
# every certificate's fully-elaborated statement, and the body of every
|
||||||
|
# specification constant transitively reachable from those statements. This
|
||||||
|
# phase binds the SHA-256 of that block, and the block's INPUT is committed
|
||||||
|
# too, so a mismatch can be DIFFED rather than merely reported.
|
||||||
|
#
|
||||||
|
# To rotate deliberately: run check.sh, take the printed OBSERVED digest, and
|
||||||
|
# update the constant below AND AUDIT-MANIFEST.txt in the same reviewable
|
||||||
|
# commit. That the rotation is visible in review is the whole point — an
|
||||||
|
# author who edits a statement and refreshes the digest in one commit is
|
||||||
|
# caught by reading the diff, not by this script.
|
||||||
|
EXPECTED_AUDIT_SHA256="c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4"
|
||||||
|
echo "=== Phase 3c: statement + specification binding ==="
|
||||||
|
cd "$AENEAS_LEAN"
|
||||||
|
# The compiler's own exit code is the primary signal; the transcript is only
|
||||||
|
# corroboration. A timeout or a memory clamp exits non-zero WITHOUT printing
|
||||||
|
# "error:", so grepping the text alone would let it through.
|
||||||
|
AUD_RC=0
|
||||||
|
AUD_OUT=$(lake env bash -c "
|
||||||
|
set -uo pipefail
|
||||||
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||||
|
cd '$HERE'
|
||||||
|
LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=8192 '$HERE/lean-guard' Proofs/Audit.lean 2>&1
|
||||||
|
" ) || AUD_RC=$?
|
||||||
|
if [ "$AUD_RC" -ne 0 ]; then
|
||||||
|
echo "AUDIT FAILED — Proofs/Audit.lean exited $AUD_RC:"
|
||||||
|
tail -20 <<<"$AUD_OUT" | sed 's/^/ /'
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
if grep -q 'error:' <<<"$AUD_OUT"; then
|
||||||
|
echo "AUDIT FAILED — Proofs/Audit.lean did not elaborate cleanly:"
|
||||||
|
grep 'error:' <<<"$AUD_OUT" | head -20 | sed 's/^/ /'
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
BLOCK=$(awk '/AUDIT-MANIFEST-BEGIN/{f=1;next} /AUDIT-MANIFEST-END/{f=0} f' <<<"$AUD_OUT")
|
||||||
|
# FAIL CLOSED ON ABSENCE: no block and a matching block must not share a path.
|
||||||
|
if [ -z "$BLOCK" ]; then
|
||||||
|
echo "AUDIT FAILED — no AUDIT-MANIFEST block was emitted (fail-closed)."; exit 1
|
||||||
|
fi
|
||||||
|
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 statement, a specification body, or a policy constant changed."
|
||||||
|
echo " First differences against the committed block:"
|
||||||
|
diff -u "$HERE/AUDIT-MANIFEST.txt" "$HERE/.audit-manifest.observed" 2>/dev/null \
|
||||||
|
| head -30 | sed 's/^/ /' || echo " (AUDIT-MANIFEST.txt absent — cannot diff)"
|
||||||
|
rm -f "$HERE/.audit-manifest.observed"
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
# The digest's INPUT must be committed and current, or the diff above would
|
||||||
|
# compare against a stale reference and quietly mislead the next reader.
|
||||||
|
if ! printf '%s\n' "$BLOCK" | cmp -s - "$HERE/AUDIT-MANIFEST.txt"; then
|
||||||
|
echo "AUDIT FAILED — the committed AUDIT-MANIFEST.txt does not match the emitted block."
|
||||||
|
echo " (the digest matched, so the committed copy is stale — refresh it)"; exit 1
|
||||||
|
fi
|
||||||
|
# CROSS-CHECK the certificate list against its OTHER two sources in this file:
|
||||||
|
# the CERTS array (Phase 3) and the apex names Phase 3b actually asks about.
|
||||||
|
# The apex names are read back out of this script rather than retyped, so a
|
||||||
|
# fourth copy cannot drift. Without this, a certificate could be dropped from
|
||||||
|
# the auditor's manifest and nothing would notice.
|
||||||
|
# Match only the QUOTED commands Phase 3b actually emits. An unquoted match
|
||||||
|
# also hits this file's own prose ("#print axioms for every certificate...")
|
||||||
|
# and silently contributes the word "for" as a certificate name.
|
||||||
|
# NOT "$0": this phase runs after `cd "$AENEAS_LEAN"`, and $0 is the relative
|
||||||
|
# path the caller used ("./check.sh"), which no longer resolves from there.
|
||||||
|
# $HERE was resolved absolutely at the top of the script.
|
||||||
|
APEX_FROM_3B=$(grep -oE "'#print axioms [A-Za-z0-9_.]+'" "$HERE/check.sh" | tr -d "'" | awk '{print $3}' | sort -u)
|
||||||
|
if [ -z "$APEX_FROM_3B" ]; then
|
||||||
|
echo "AUDIT FAILED — could not recover the apex certificate names from Phase 3b."; exit 1
|
||||||
|
fi
|
||||||
|
# Every recovered name must be namespace-qualified; a bare word means the
|
||||||
|
# pattern drifted onto prose again rather than onto a command.
|
||||||
|
while read -r n; do
|
||||||
|
case "$n" in *.*) ;; *) echo "AUDIT FAILED — recovered apex name '$n' is not qualified."; exit 1;; esac
|
||||||
|
done <<<"$APEX_FROM_3B"
|
||||||
|
AUD_CERTS=$(grep -o 'AUDITED-CERTIFICATES:.*' <<<"$AUD_OUT" | sed 's/AUDITED-CERTIFICATES: //' | tr ' ' '\n' | sort -u)
|
||||||
|
BASH_CERTS=$(printf '%s\n' "${CERTS[@]}" $APEX_FROM_3B | sort -u)
|
||||||
|
if [ "$AUD_CERTS" != "$BASH_CERTS" ]; then
|
||||||
|
echo "AUDIT FAILED — the auditor's certificate list and this script's have drifted:"
|
||||||
|
diff <(echo "$BASH_CERTS") <(echo "$AUD_CERTS") | sed 's/^/ /'
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
grep -o 'statement audit PASSED:.*' <<<"$AUD_OUT" | sed 's/^/ /'
|
||||||
|
echo " audit-manifest sha256 = $GOT_SHA (matches the committed block byte-for-byte)"
|
||||||
|
|
||||||
echo ""
|
echo ""
|
||||||
echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES."
|
echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES."
|
||||||
|
echo "STATEMENTS AND SPECIFICATIONS BOUND TO THE COMMITTED AUDIT MANIFEST."
|
||||||
|
|
|
||||||
|
|
@ -23,6 +23,9 @@ CORES="${LEAN_MAX_CORES:-0-3}"
|
||||||
ATTACK="$HERE/Proofs/ZZSelftestAttack.lean"
|
ATTACK="$HERE/Proofs/ZZSelftestAttack.lean"
|
||||||
STASH="$(mktemp -d)"
|
STASH="$(mktemp -d)"
|
||||||
FAILURES=0
|
FAILURES=0
|
||||||
|
# Recorded before anything is touched, so the restore check compares against
|
||||||
|
# reality rather than assuming a pristine checkout.
|
||||||
|
TREE_AT_START="$(cd "$(dirname "$0")/.." && git status --porcelain -- verification/Proofs)"
|
||||||
|
|
||||||
cleanup() {
|
cleanup() {
|
||||||
rm -f "$ATTACK" "${ATTACK%.lean}.olean"
|
rm -f "$ATTACK" "${ATTACK%.lean}.olean"
|
||||||
|
|
@ -106,12 +109,21 @@ else
|
||||||
echo " ok no litter left by either the green or the red path"
|
echo " ok no litter left by either the green or the red path"
|
||||||
fi
|
fi
|
||||||
|
|
||||||
# ── 5. Restored: the self-test must leave the working tree exactly as found.
|
# ── 5. Restored: the self-test must leave the working tree exactly as it found
|
||||||
DIRT=$(cd "$HERE/.." && git status --porcelain -- verification/Proofs | wc -l)
|
# it. Compared against the state recorded at START, not against a pristine
|
||||||
if [ "$DIRT" -ne 0 ]; then
|
# checkout — files can be legitimately uncommitted while work is in flight,
|
||||||
echo " FAIL restore: $DIRT file(s) under Proofs/ left modified"; FAILURES=$((FAILURES+1))
|
# and a test that assumes otherwise reports its own premise as a failure.
|
||||||
|
# Compare the two states AS STRINGS. Comparing `echo "$VAR"` against a raw
|
||||||
|
# command substitution is asymmetric: for a clean tree the variable is empty
|
||||||
|
# and `echo` still emits one blank line while the command emits none, so the
|
||||||
|
# check reports a spurious difference exactly when nothing is wrong.
|
||||||
|
TREE_NOW="$(cd "$HERE/.." && git status --porcelain -- verification/Proofs)"
|
||||||
|
if [ "$TREE_AT_START" != "$TREE_NOW" ]; then
|
||||||
|
echo " FAIL restore: Proofs/ differs from how this test found it:"
|
||||||
|
diff <(printf '%s\n' "$TREE_AT_START") <(printf '%s\n' "$TREE_NOW") | sed 's/^/ /'
|
||||||
|
FAILURES=$((FAILURES+1))
|
||||||
else
|
else
|
||||||
echo " ok working tree restored"
|
echo " ok working tree restored to its starting state"
|
||||||
fi
|
fi
|
||||||
|
|
||||||
echo ""
|
echo ""
|
||||||
|
|
|
||||||
108
verification/selftest-harness.sh
Executable file
108
verification/selftest-harness.sh
Executable file
|
|
@ -0,0 +1,108 @@
|
||||||
|
#!/usr/bin/env bash
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
# selftest-harness.sh — adversarial self-test for check.sh Phase 0c.
|
||||||
|
#
|
||||||
|
# Phase 0c pins the scripts and policy files the button itself runs on. The
|
||||||
|
# attack it exists to stop is the cheapest one in the estate: don't touch the
|
||||||
|
# proofs at all, edit the checker. Round-5 review of the companion SLH-DSA
|
||||||
|
# repository stubbed the compiler wrapper alone and got ALL GREEN in 3.6
|
||||||
|
# seconds over deliberately destroyed proofs.
|
||||||
|
#
|
||||||
|
# Cases, each asserting a SPECIFIC diagnostic:
|
||||||
|
# 0 positive control: untouched tree passes
|
||||||
|
# 1 a pinned harness file edited by one byte → does not match its pin
|
||||||
|
# 2 a NEW executable appears, unpinned → set mismatch
|
||||||
|
# 3 an entry DELETED from HARNESS.sha256 → set mismatch, NOT a
|
||||||
|
# silent un-pin (this is the shape of the defect SLH-DSA round-6 found:
|
||||||
|
# dropping a key un-pinned two files with no diagnostic at all)
|
||||||
|
# 4 HARNESS.sha256 itself removed → fail-closed
|
||||||
|
#
|
||||||
|
# Phase 0c is lifted out of check.sh at run time, so the tested logic IS the
|
||||||
|
# shipping logic. Cheap: no Lean, runs in about a second.
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
set -uo pipefail
|
||||||
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||||
|
FAILURES=0
|
||||||
|
STASH="$(mktemp -d)"
|
||||||
|
NEWEXE="$HERE/zz-selftest-helper.sh"
|
||||||
|
|
||||||
|
cleanup() {
|
||||||
|
[ -f "$STASH/HARNESS.sha256" ] && cp "$STASH/HARNESS.sha256" "$HERE/HARNESS.sha256"
|
||||||
|
[ -f "$STASH/victim" ] && cp "$STASH/victim" "$HERE/$VICTIM"
|
||||||
|
rm -f "$NEWEXE"
|
||||||
|
rm -rf "$STASH"
|
||||||
|
}
|
||||||
|
trap cleanup EXIT INT TERM
|
||||||
|
|
||||||
|
cp "$HERE/HARNESS.sha256" "$STASH/HARNESS.sha256"
|
||||||
|
|
||||||
|
# Lift Phase 0c. The two repo families end the phase differently, so accept
|
||||||
|
# either terminator rather than hardcoding one and silently lifting nothing.
|
||||||
|
DRIVER="$STASH/phase0c.sh"
|
||||||
|
{
|
||||||
|
echo 'set -uo pipefail'
|
||||||
|
echo "HERE=\"$HERE\""
|
||||||
|
awk '/^# ── Phase 0c/{f=1} f{print} /^# ── Phase 1|^echo "=== Phase 1/{if(f && !/Phase 0c/) exit}' "$HERE/check.sh" \
|
||||||
|
| sed '/^# ── Phase 1/d; /^echo "=== Phase 1/d'
|
||||||
|
} > "$DRIVER"
|
||||||
|
if [ "$(grep -c . "$DRIVER")" -lt 20 ]; then
|
||||||
|
echo "FATAL: could not lift Phase 0c out of check.sh — the phase markers moved."
|
||||||
|
echo "This self-test must attack the shipping gate; refusing to run against nothing."
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
|
||||||
|
expect() { # expect <label> <want-rc> <want-substring>
|
||||||
|
local label="$1" want_rc="$2" want_txt="$3" out rc
|
||||||
|
out=$(bash "$DRIVER" 2>&1); rc=$?
|
||||||
|
if [ "$rc" -ne "$want_rc" ]; then
|
||||||
|
echo " ✗ $label: exit $rc, expected $want_rc"; echo "$out" | sed 's/^/ /'
|
||||||
|
FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
if ! grep -qF "$want_txt" <<<"$out"; then
|
||||||
|
echo " ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
|
||||||
|
echo " wanted: $want_txt"; echo "$out" | sed 's/^/ /'
|
||||||
|
FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
echo " ✓ $label"
|
||||||
|
}
|
||||||
|
|
||||||
|
echo "=== selftest-harness: attacking check.sh Phase 0c ==="
|
||||||
|
|
||||||
|
# ── 0. positive control ────────────────────────────────────────────────────
|
||||||
|
expect "case 0 control: untouched harness passes" 0 "match their pins"
|
||||||
|
|
||||||
|
# ── 1. edit a pinned file. lean-guard is the pointed choice: it is the memory
|
||||||
|
# cap protecting this machine, and stubbing it is the demonstrated
|
||||||
|
# 3.6-second path to a false green.
|
||||||
|
VICTIM=lean-guard
|
||||||
|
cp "$HERE/$VICTIM" "$STASH/victim"
|
||||||
|
printf '\n# selftest\n' >> "$HERE/$VICTIM"
|
||||||
|
expect "case 1: edited lean-guard caught" 1 "does not match its pin"
|
||||||
|
cp "$STASH/victim" "$HERE/$VICTIM"
|
||||||
|
|
||||||
|
# ── 2. a new executable the button could shell out to ──────────────────────
|
||||||
|
printf '#!/bin/sh\necho "unpinned"\n' > "$NEWEXE"; chmod +x "$NEWEXE"
|
||||||
|
expect "case 2: new unpinned executable caught" 1 "does not match HARNESS.sha256"
|
||||||
|
rm -f "$NEWEXE"
|
||||||
|
|
||||||
|
# ── 3. delete a pin entry: the set must be derived from the filesystem, not
|
||||||
|
# read out of the map being consulted, or this is a silent un-pin.
|
||||||
|
grep -v " ${VICTIM}\$" "$STASH/HARNESS.sha256" > "$HERE/HARNESS.sha256"
|
||||||
|
expect "case 3: deleted pin entry is a failure, not a silent un-pin" 1 "does not match HARNESS.sha256"
|
||||||
|
cp "$STASH/HARNESS.sha256" "$HERE/HARNESS.sha256"
|
||||||
|
|
||||||
|
# ── 4. absence must not pass for cleanliness ───────────────────────────────
|
||||||
|
rm -f "$HERE/HARNESS.sha256"
|
||||||
|
expect "case 4: missing pin file is fail-closed" 1 "the harness is unpinned"
|
||||||
|
cp "$STASH/HARNESS.sha256" "$HERE/HARNESS.sha256"
|
||||||
|
|
||||||
|
# ── 5. restored ────────────────────────────────────────────────────────────
|
||||||
|
expect "case 5: restored to green" 0 "match their pins"
|
||||||
|
|
||||||
|
echo ""
|
||||||
|
if [ "$FAILURES" -eq 0 ]; then
|
||||||
|
echo "SELFTEST PASSED — Phase 0c rejects harness tampering for the stated reason."
|
||||||
|
exit 0
|
||||||
|
fi
|
||||||
|
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
|
||||||
|
exit 1
|
||||||
265
verification/selftest-statements.sh
Executable file
265
verification/selftest-statements.sh
Executable file
|
|
@ -0,0 +1,265 @@
|
||||||
|
#!/usr/bin/env bash
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
# selftest-statements.sh — adversarial self-test for the BINDING phases,
|
||||||
|
# check.sh 0b (the extracted model) and 3c (statements and specifications).
|
||||||
|
#
|
||||||
|
# These phases exist because Phases 2b/3/3b establish what a certificate RESTS
|
||||||
|
# ON and never what it SAYS, nor what it is ABOUT. This script performs the
|
||||||
|
# attacks that move no axiom cone at all, and asserts each is rejected FOR THE
|
||||||
|
# STATED REASON.
|
||||||
|
#
|
||||||
|
# It lifts Phase 3c out of check.sh at run time, so it attacks the shipping
|
||||||
|
# gate rather than a copy that can drift away from it.
|
||||||
|
#
|
||||||
|
# Requires a prior green build (Proofs/*.olean present). The cheap cases each
|
||||||
|
# recompile only Proofs/Audit.lean (~10 s). The gutted-statement case also
|
||||||
|
# recompiles one certificate module and is therefore slower; skip it with
|
||||||
|
# SKIP_SLOW=1 if you only want the fast gates exercised.
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
set -uo pipefail
|
||||||
|
source ~/aeneas-toolchain/env.sh
|
||||||
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||||
|
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
||||||
|
TIMEOUT="${LEAN_TIMEOUT:-900}"
|
||||||
|
export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"
|
||||||
|
CORES="${LEAN_MAX_CORES:-0-3}"
|
||||||
|
SKIP_SLOW="${SKIP_SLOW:-0}"
|
||||||
|
|
||||||
|
STASH="$(mktemp -d)"
|
||||||
|
FAILURES=0
|
||||||
|
# Recorded before anything is touched, so the restore check compares against
|
||||||
|
# reality rather than assuming a pristine checkout.
|
||||||
|
TREE_AT_START="$(cd "$(dirname "$0")/.." && git status --porcelain)"
|
||||||
|
|
||||||
|
cleanup() {
|
||||||
|
[ -f "$STASH/Audit.lean" ] && cp "$STASH/Audit.lean" "$HERE/Proofs/Audit.lean"
|
||||||
|
[ -f "$STASH/AUDIT-MANIFEST.txt" ] && cp "$STASH/AUDIT-MANIFEST.txt" "$HERE/AUDIT-MANIFEST.txt"
|
||||||
|
[ -f "$STASH/check.sh" ] && cp "$STASH/check.sh" "$HERE/check.sh"
|
||||||
|
[ -n "${GUT_MOD:-}" ] && [ -f "$STASH/gut.lean" ] && cp "$STASH/gut.lean" "$HERE/Proofs/$GUT_MOD.lean"
|
||||||
|
[ -n "${GENF:-}" ] && [ -f "$STASH/genfile.bak" ] && cp "$STASH/genfile.bak" "$HERE/gen/$GENF"
|
||||||
|
[ -n "${GENF:-}" ] && rm -f "$HERE/gen/$(dirname "$GENF")/ZZExtra.lean"
|
||||||
|
rm -rf "$STASH"
|
||||||
|
}
|
||||||
|
trap cleanup EXIT INT TERM
|
||||||
|
|
||||||
|
cp "$HERE/Proofs/Audit.lean" "$STASH/Audit.lean"
|
||||||
|
cp "$HERE/AUDIT-MANIFEST.txt" "$STASH/AUDIT-MANIFEST.txt"
|
||||||
|
cp "$HERE/check.sh" "$STASH/check.sh"
|
||||||
|
|
||||||
|
DRIVER0B="$STASH/phase0b.sh"
|
||||||
|
{
|
||||||
|
echo 'set -uo pipefail'
|
||||||
|
echo "HERE=\"$HERE\""
|
||||||
|
sed -n '/^# ── Phase 0b/,/^# ── Phase 1/p' "$HERE/check.sh" | sed '$d'
|
||||||
|
} > "$DRIVER0B"
|
||||||
|
if [ "$(wc -l < "$DRIVER0B")" -lt 20 ]; then
|
||||||
|
echo "FATAL: could not lift Phase 0b out of check.sh."; exit 1
|
||||||
|
fi
|
||||||
|
|
||||||
|
DRIVER="$STASH/phase3c.sh"
|
||||||
|
build_driver() {
|
||||||
|
{
|
||||||
|
echo 'set -uo pipefail'
|
||||||
|
echo 'source ~/aeneas-toolchain/env.sh'
|
||||||
|
echo "HERE=\"$HERE\""
|
||||||
|
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
|
||||||
|
echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
|
||||||
|
# CERTS is referenced by the cross-check inside Phase 3c.
|
||||||
|
sed -n '/^CERTS=(/,/^)/p' "$HERE/check.sh"
|
||||||
|
# `$0` inside Phase 3c must resolve to the shipping check.sh, not to this
|
||||||
|
# driver, or the apex-name recovery would read the wrong file.
|
||||||
|
sed -n '/^# ── Phase 3c/,/^echo ""$/p' "$HERE/check.sh" | sed '$d' \
|
||||||
|
| sed "s|\"\$0\"|\"$HERE/check.sh\"|g"
|
||||||
|
} > "$DRIVER"
|
||||||
|
if [ "$(wc -l < "$DRIVER")" -lt 60 ]; then
|
||||||
|
echo "FATAL: could not lift Phase 3c out of check.sh — the phase markers moved."
|
||||||
|
echo "This self-test must attack the shipping gate; refusing to run against nothing."
|
||||||
|
exit 1
|
||||||
|
fi
|
||||||
|
}
|
||||||
|
build_driver
|
||||||
|
|
||||||
|
recompile_audit() {
|
||||||
|
( cd "$AENEAS_LEAN" && lake env bash -c "
|
||||||
|
set -uo pipefail
|
||||||
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||||
|
cd '$HERE'
|
||||||
|
LEAN_TIMEOUT=$TIMEOUT '$HERE/lean-guard' Proofs/Audit.lean
|
||||||
|
" ) >/dev/null 2>&1
|
||||||
|
}
|
||||||
|
|
||||||
|
expect() { # expect <name> <expected-rc> <required-substring>
|
||||||
|
local name="$1" want_rc="$2" want_txt="$3" out rc
|
||||||
|
out=$(bash "$DRIVER" 2>&1); rc=$?
|
||||||
|
if [ "$rc" -ne "$want_rc" ]; then
|
||||||
|
echo " FAIL $name: exit $rc, expected $want_rc"; FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
if ! grep -qF "$want_txt" <<<"$out"; then
|
||||||
|
echo " FAIL $name: exit code right, diagnostic wrong (rejected for the wrong reason)"
|
||||||
|
echo " wanted: $want_txt"
|
||||||
|
echo " got: $(tr '\n' '|' <<<"$out" | cut -c1-260)"
|
||||||
|
FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
echo " ok $name"
|
||||||
|
}
|
||||||
|
|
||||||
|
echo "=== selftest-statements: attacking check.sh Phases 0b and 3c ==="
|
||||||
|
|
||||||
|
# ── 0. THE SUBJECT. The certificates are stated ABOUT the extracted model in
|
||||||
|
# gen/. A statement names an extracted function; editing that function's
|
||||||
|
# BODY changes what the theorem is about while leaving every statement,
|
||||||
|
# every cone and the Phase 3c digest byte-identical. Demonstrated on
|
||||||
|
# 2026-07-28: risc0 and betrusted ship different extracted models and
|
||||||
|
# produce the SAME audit-manifest digest. Only the byte pin separates them.
|
||||||
|
expect0b() {
|
||||||
|
local name="$1" want_rc="$2" want_txt="$3" out rc
|
||||||
|
out=$(bash "$DRIVER0B" 2>&1); rc=$?
|
||||||
|
if [ "$rc" -ne "$want_rc" ]; then
|
||||||
|
echo " FAIL $name: exit $rc, expected $want_rc"; FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
if ! grep -qF "$want_txt" <<<"$out"; then
|
||||||
|
echo " FAIL $name: exit code right, diagnostic wrong (rejected for the wrong reason)"
|
||||||
|
echo " wanted: $want_txt"; FAILURES=$((FAILURES+1)); return
|
||||||
|
fi
|
||||||
|
echo " ok $name"
|
||||||
|
}
|
||||||
|
expect0b "model pin: baseline green" 0 "match their pins"
|
||||||
|
GENF=$(awk 'NR==1{print $2}' "$HERE/GEN-MODEL.sha256")
|
||||||
|
cp "$HERE/gen/$GENF" "$STASH/genfile.bak"
|
||||||
|
printf '\n-- edited\n' >> "$HERE/gen/$GENF"
|
||||||
|
expect0b "model pin: edited model body caught" 1 "does not match its pin"
|
||||||
|
cp "$STASH/genfile.bak" "$HERE/gen/$GENF"
|
||||||
|
cp "$HERE/gen/$GENF" "$HERE/gen/$(dirname "$GENF")/ZZExtra.lean"
|
||||||
|
expect0b "model pin: an unlisted model file caught" 1 "does not match GEN-MODEL.sha256"
|
||||||
|
rm -f "$HERE/gen/$(dirname "$GENF")/ZZExtra.lean"
|
||||||
|
|
||||||
|
# ── 1. Baseline: untouched repository passes and reports what it bound.
|
||||||
|
expect "baseline green, manifest digest matches" 0 "audit-manifest sha256"
|
||||||
|
|
||||||
|
# ── 2. WIDEN THE POLICY. Add one name to the apex boundary.
|
||||||
|
# The policy IS inside the digest, but this attack never reaches the
|
||||||
|
# digest: because the apex tier requires EXACT cone equality, a widened
|
||||||
|
# boundary immediately shows up as `missing=` on all four apex
|
||||||
|
# certificates. That is a strictly stronger rejection than a digest
|
||||||
|
# mismatch — it names which certificates stopped matching instead of
|
||||||
|
# merely reporting that some byte moved. Asserted here as such, because a
|
||||||
|
# test that demanded the weaker diagnostic would go red the day the
|
||||||
|
# stronger guard started working.
|
||||||
|
python3 - "$HERE/Proofs/Audit.lean" <<'PY'
|
||||||
|
import sys, re
|
||||||
|
f = sys.argv[1]; s = open(f).read()
|
||||||
|
m = re.search(r'^def apexExtra : List Name :=\n \[(.*)\]$', s, re.M)
|
||||||
|
assert m, "apexExtra not found"
|
||||||
|
s = s.replace(m.group(0), m.group(0)[:-1] + ", `Classical.byContradiction]", 1)
|
||||||
|
open(f, "w").write(s)
|
||||||
|
PY
|
||||||
|
recompile_audit
|
||||||
|
expect "widened policy caught by the exact-cone requirement" 1 "missing=[Classical.byContradiction]"
|
||||||
|
cp "$STASH/Audit.lean" "$HERE/Proofs/Audit.lean"; recompile_audit
|
||||||
|
|
||||||
|
# ── 3. HAND-EDIT THE COMMITTED BLOCK. The digest still matches the emitted
|
||||||
|
# block, so only the byte-comparison against the committed input can see
|
||||||
|
# this. Without it the diff printed on a future failure would silently
|
||||||
|
# compare against a doctored reference.
|
||||||
|
sed -i '2s/$/ TAMPERED/' "$HERE/AUDIT-MANIFEST.txt"
|
||||||
|
expect "hand-edited committed block caught" 1 "does not match the emitted block"
|
||||||
|
cp "$STASH/AUDIT-MANIFEST.txt" "$HERE/AUDIT-MANIFEST.txt"
|
||||||
|
|
||||||
|
# ── 4. DROP A CERTIFICATE FROM THE AUDITOR — AND REFRESH THE DIGEST TO MATCH,
|
||||||
|
# exactly as an author covering their tracks would. The digest and the
|
||||||
|
# committed block are now perfectly consistent with each other. The only
|
||||||
|
# thing that can still object is the cross-check against the certificate
|
||||||
|
# list this script derives from its OWN two sources.
|
||||||
|
python3 - "$HERE/Proofs/Audit.lean" <<'PY'
|
||||||
|
import sys, re
|
||||||
|
f = sys.argv[1]; s = open(f).read()
|
||||||
|
lines = s.splitlines(True)
|
||||||
|
i = next(k for k, l in enumerate(lines) if l.strip().startswith(', (`') and 'kernel3)' in l)
|
||||||
|
del lines[i]
|
||||||
|
open(f, "w").write("".join(lines))
|
||||||
|
PY
|
||||||
|
recompile_audit
|
||||||
|
# Regenerate the committed block and re-pin the digest from the tampered run.
|
||||||
|
TAMPERED_OUT=$(cd "$AENEAS_LEAN" && lake env bash -c "
|
||||||
|
set -uo pipefail
|
||||||
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||||
|
cd '$HERE'
|
||||||
|
LEAN_TIMEOUT=$TIMEOUT '$HERE/lean-guard' Proofs/Audit.lean 2>&1")
|
||||||
|
awk '/AUDIT-MANIFEST-BEGIN/{f=1;next} /AUDIT-MANIFEST-END/{f=0} f' <<<"$TAMPERED_OUT" > "$HERE/AUDIT-MANIFEST.txt"
|
||||||
|
NEWSHA=$(sha256sum "$HERE/AUDIT-MANIFEST.txt" | cut -d' ' -f1)
|
||||||
|
sed -i "s/^EXPECTED_AUDIT_SHA256=.*/EXPECTED_AUDIT_SHA256=\"$NEWSHA\"/" "$HERE/check.sh"
|
||||||
|
build_driver
|
||||||
|
expect "dropped certificate caught by the cross-check, digest refreshed or not" 1 "have drifted"
|
||||||
|
cp "$STASH/Audit.lean" "$HERE/Proofs/Audit.lean"
|
||||||
|
cp "$STASH/AUDIT-MANIFEST.txt" "$HERE/AUDIT-MANIFEST.txt"
|
||||||
|
cp "$STASH/check.sh" "$HERE/check.sh"
|
||||||
|
build_driver
|
||||||
|
recompile_audit
|
||||||
|
|
||||||
|
# ── 5. THE REAL ONE: gut a certificate's STATEMENT while preserving its axiom
|
||||||
|
# cone. Every earlier phase passes this; only the statement binding sees it.
|
||||||
|
if [ "$SKIP_SLOW" = "1" ]; then
|
||||||
|
echo " skip gutted-statement case (SKIP_SLOW=1) — the fast gates above do not cover it"
|
||||||
|
else
|
||||||
|
# A TERMINAL certificate: nothing else in the corpus consumes it. Gutting a
|
||||||
|
# load-bearing one simply breaks its consumers and the module stops
|
||||||
|
# compiling, which demonstrates the compiler working, not this gate.
|
||||||
|
GUT_MOD=FieldMain
|
||||||
|
GUT_CERT=CurveFieldProofs.fieldImplementation
|
||||||
|
cp "$HERE/Proofs/$GUT_MOD.lean" "$STASH/gut.lean"
|
||||||
|
python3 - "$HERE/Proofs/$GUT_MOD.lean" "$GUT_CERT" <<'PY'
|
||||||
|
import sys, re
|
||||||
|
f, cert = sys.argv[1], sys.argv[2]
|
||||||
|
short = cert.split('.')[-1]
|
||||||
|
s = open(f).read()
|
||||||
|
m = re.search(r'^theorem %s\b' % re.escape(short), s, re.M)
|
||||||
|
assert m, f"certificate {short} not found in {f}"
|
||||||
|
i = m.start()
|
||||||
|
# find the next top-level declaration after it
|
||||||
|
nxt = re.search(r'^(theorem|lemma|def|noncomputable def|end|/--|@\[)', s[i+10:], re.M)
|
||||||
|
assert nxt, "no following declaration"
|
||||||
|
j = i + 10 + nxt.start()
|
||||||
|
# Same cone (Classical.em pulls in Classical.choice/propext), utterly different claim.
|
||||||
|
gut = "theorem %s : (∀ p : Prop, p ∨ ¬p) := Classical.em\n\n" % short
|
||||||
|
open(f, "w").write(s[:i] + gut + s[j:])
|
||||||
|
PY
|
||||||
|
( cd "$AENEAS_LEAN" && lake env bash -c "
|
||||||
|
set -uo pipefail
|
||||||
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||||
|
cd '$HERE'
|
||||||
|
LEAN_TIMEOUT=$TIMEOUT '$HERE/lean-guard' Proofs/$GUT_MOD.lean
|
||||||
|
" ) >/dev/null 2>&1 || { echo " FAIL setup: the gutted module did not compile"; FAILURES=$((FAILURES+1)); }
|
||||||
|
recompile_audit
|
||||||
|
expect "gutted statement caught (cone unchanged)" 1 "audit-manifest digest mismatch"
|
||||||
|
cp "$STASH/gut.lean" "$HERE/Proofs/$GUT_MOD.lean"
|
||||||
|
( cd "$AENEAS_LEAN" && lake env bash -c "
|
||||||
|
set -uo pipefail
|
||||||
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||||
|
cd '$HERE'
|
||||||
|
LEAN_TIMEOUT=$TIMEOUT '$HERE/lean-guard' Proofs/$GUT_MOD.lean
|
||||||
|
" ) >/dev/null 2>&1
|
||||||
|
recompile_audit
|
||||||
|
fi
|
||||||
|
|
||||||
|
# ── 6. Restored: green again, and the working tree is as we found it.
|
||||||
|
expect "restored to green" 0 "audit-manifest sha256"
|
||||||
|
# String comparison, not diff of process substitutions: for a clean tree the
|
||||||
|
# variable is empty and `echo` emits a blank line the raw command does not,
|
||||||
|
# which reports a difference precisely when there is none.
|
||||||
|
TREE_NOW="$(cd "$HERE/.." && git status --porcelain)"
|
||||||
|
if [ "$TREE_AT_START" != "$TREE_NOW" ]; then
|
||||||
|
echo " FAIL restore: the working tree differs from how this test found it:"
|
||||||
|
diff <(printf '%s\n' "$TREE_AT_START") <(printf '%s\n' "$TREE_NOW") | sed 's/^/ /'
|
||||||
|
FAILURES=$((FAILURES+1))
|
||||||
|
else
|
||||||
|
echo " ok working tree restored to its starting state"
|
||||||
|
fi
|
||||||
|
|
||||||
|
echo ""
|
||||||
|
if [ "$FAILURES" -eq 0 ]; then
|
||||||
|
echo "SELFTEST PASSED — Phase 3c rejects statement- and specification-level"
|
||||||
|
echo "tampering that moves no axiom cone, for the stated reason in each case."
|
||||||
|
exit 0
|
||||||
|
fi
|
||||||
|
echo "SELFTEST FAILED: $FAILURES check(s) did not behave as claimed."
|
||||||
|
exit 1
|
||||||
Loading…
Reference in a new issue