mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-03 19:53:45 +00:00
Compare commits
2 commits
13d974ba03
...
d2760e41ab
| Author | SHA1 | Date | |
|---|---|---|---|
| d2760e41ab | |||
| 81a802f35b |
9 changed files with 993 additions and 5 deletions
|
|
@ -60,3 +60,59 @@ running Rust code. Everything else is machine-checked.
|
|||
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
|
||||
phase. Reading the statements remains a human act.
|
||||
9. **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.
|
||||
|
||||
10. **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 @@
|
|||
5c8b68cc4b7d4782b467fa91bd21837774c9ac10b906f803d47779e92c15e061 CurveField/FunsExternal.lean
|
||||
c9cc095ef7ec6e1c1e914aec280468ad6bc27bdfb8c7eb0c2b647060a5cc7076 CurveField/FunsExternal_Template.lean
|
||||
418682624b1591b6b7f5d245efa4312498255459ce47d9b507ab77d32439484a CurveField/Funs.lean
|
||||
d197d7b9fe515863784eeee59a2fbb69735d10ebcf5cc4e03feb3afbeb53a2b7 CurveField/TypesExternal.lean
|
||||
4560fc87c6156df16c34117db0817dc0926709f884728d9ca907985cbf931c6c CurveField/TypesExternal_Template.lean
|
||||
f17fd167be6e273fe6379196f0e931dabb963d5f7c9d27efbd1e3deab74a8e1e CurveField/Types.lean
|
||||
11e90fcaf1a33a7f66b1d9eaebcd4b69db23837a027ff56f64941084d223512b CurveSig/FunsExternal.lean
|
||||
3fa865dca7f03dcfdd68533321a6669d73e8698f2780b6934ff135cef0cd8f38 CurveSig/FunsExternal_Template.lean
|
||||
28ed4991ccf04ffaf66d0f47bd1cc90dec9029ba7381d54ad1d8a3d684d074b3 CurveSig/Funs.lean
|
||||
2358490d0b10aa95cfd951e65f9d52988da52740a5c8af209cd9e0bc45a26734 CurveSig/TypesExternal.lean
|
||||
fe94bba57cba8a40aa6195f505eb56107c06f92be7dfc04931a7c05d104ae76a CurveSig/TypesExternal_Template.lean
|
||||
29e72d1c365464b009a38e2310cebbf285e96c296e59ed098e06e647bbc5ffe6 CurveSig/Types.lean
|
||||
10
verification/HARNESS.sha256
Normal file
10
verification/HARNESS.sha256
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt
|
||||
b88f4bc16d3188f4830f8333201fc7826d46acf829c37f7da398d6ae9bfca15e check-scalar.sh
|
||||
813c31664484adddd1752ea3bb30da826ad1050fd378604c242bcafb105fb4a3 check.sh
|
||||
afa13c814ba9757de8d59777524e496653351112a1a7037a56f1b0b436b28cf9 extract.sh
|
||||
0ea20d74cd359da404ee3be116058374cbb9fd992ed170e5f6c64f8d7a6b2733 GEN-MODEL.sha256
|
||||
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
||||
772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean
|
||||
79611f9689ba714fb8d3f57aee86ad9655509303445beaad766bf8b049de8c44 selftest-axgate.sh
|
||||
3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh
|
||||
a14acaafe914aabb9df44fcd05fd50d475804280fab9e332fdb5ea0b0d35f164 selftest-statements.sh
|
||||
234
verification/Proofs/Audit.lean
Normal file
234
verification/Proofs/Audit.lean
Normal file
|
|
@ -0,0 +1,234 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────
|
||||
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.DsmNafSpec
|
||||
import Proofs.DsmMulSpec
|
||||
import Proofs.SigApexSpec
|
||||
import Proofs.ToBytesSpec
|
||||
import Proofs.CompressSpec
|
||||
import Proofs.ScalarPackSpec
|
||||
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, `verifying.sha512_hash3, `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.
|
||||
# 3. axiom audit: #print axioms for every certificate in CERTS; each must
|
||||
# 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
|
||||
source ~/aeneas-toolchain/env.sh
|
||||
|
|
@ -78,6 +87,7 @@ PROOFS=(
|
|||
DecompressSpec
|
||||
FromBytesSpec
|
||||
DecompressMain
|
||||
Audit # LAST: imports the certificate corpus and runs the audit
|
||||
)
|
||||
# Fully-qualified certificate names; each must be axiom-clean.
|
||||
CERTS=(
|
||||
|
|
@ -141,6 +151,89 @@ for f in "$HERE"/gen/CurveField/*.lean "$HERE"/Proofs/*.lean; do
|
|||
done
|
||||
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 ───────────────────────────────────
|
||||
echo "=== Phase 1: stub audit ==="
|
||||
if grep -rn 'by trivial' "$HERE"/Proofs/*Spec*.lean 2>/dev/null; then
|
||||
|
|
@ -310,5 +403,103 @@ lake env bash -c "
|
|||
fi
|
||||
"
|
||||
|
||||
|
||||
# ── 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="6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24"
|
||||
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 "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"
|
||||
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 -- verification/Proofs)"
|
||||
|
||||
cleanup() {
|
||||
rm -f "$ATTACK" "${ATTACK%.lean}.olean"
|
||||
|
|
@ -106,12 +109,21 @@ else
|
|||
echo " ok no litter left by either the green or the red path"
|
||||
fi
|
||||
|
||||
# ── 5. Restored: the self-test must leave the working tree exactly as found.
|
||||
DIRT=$(cd "$HERE/.." && git status --porcelain -- verification/Proofs | wc -l)
|
||||
if [ "$DIRT" -ne 0 ]; then
|
||||
echo " FAIL restore: $DIRT file(s) under Proofs/ left modified"; FAILURES=$((FAILURES+1))
|
||||
# ── 5. Restored: the self-test must leave the working tree exactly as it found
|
||||
# it. Compared against the state recorded at START, not against a pristine
|
||||
# checkout — files can be legitimately uncommitted while work is in flight,
|
||||
# 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
|
||||
echo " ok working tree restored"
|
||||
echo " ok working tree restored to its starting state"
|
||||
fi
|
||||
|
||||
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