diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 78374fb..1756a2d 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -58,6 +58,15 @@ running Rust code. Everything else is machine-checked. count of shipped sources, so a deleted `.olean` cannot make the scan pass vacuously. `selftest-axgate.sh` attacks the shipping gate rather than a copy of it, and was itself negative-tested by removing the gate's error. + `selftest-shapes.sh` asks the companion question about Phase 2c: can a + declaration HIDE from the walker? It adds four shapes to an audited module + — `@[simp]`, `private`, an `instance`, and a nested namespace reusing an + audited basename — and requires the walker to report every one of them by + name, not merely to fail. Those four shapes are the ones that defeated a + source-regex enumerator in ltl-accumulator-verified and caused Phase 2c to + be written against the Lean environment instead; until 2026-07-31 the fix + was ported here but never re-attacked. It too was negative-tested, by + removing the injection and confirming the run then reports the walker blind. **The residue you must still supply yourself:** this binds *declarations*, not *statements*. Nothing in the button establishes that a certificate's theorem says what its name — or this document — suggests it says. A diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index cdc44a0..70dce86 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -15,5 +15,6 @@ bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-audit eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh +26f10a749e03cecd7ad173d0d621498386444d8e347f606a99a2fadb06738d86 selftest-shapes.sh 2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f selftest-statements.sh df2389909839c5c2275097044b112bd254e48aa21b4b8f6c1430847c0a0c7cc6 selftest-tiers.sh diff --git a/verification/selftest-shapes.sh b/verification/selftest-shapes.sh new file mode 100755 index 0000000..ebf9163 --- /dev/null +++ b/verification/selftest-shapes.sh @@ -0,0 +1,223 @@ +#!/usr/bin/env bash +# ───────────────────────────────────────────────────────────────────────────── +# selftest-shapes.sh — can a declaration HIDE from the inventory walker? +# +# check.sh Phase 2c exists because a source-regex enumerator turned out to be +# evadable: in ltl-accumulator-verified a nine-attack self-test defeated one +# with attributed, private, indented and `instance` declarations and with a +# nested-namespace basename collision. The fix was to stop reading source text +# and ask the Lean environment instead, and that fix was PORTED here — see the +# note at the head of Phase 2c. +# +# But a fix ported is not a fix tested. `selftest-inventory.sh` proves the GATE +# reacts correctly to a difference; it feeds the gate synthetic observations and +# never runs the walker. Nothing in these four forks has ever asked the question +# the accumulator's suite asks: does the WALKER SEE a declaration written in an +# evasive shape? If it silently skipped one, the observation would match the +# allowlist, the gate would be satisfied, and a hidden theorem would ride along +# inside an audited module with every button green. +# +# 0 control: the untouched tree's observation equals the allowlist +# 1 FOUR EVASIVE SHAPES added to an audited module at once: +# @[simp] theorem an attribute in front of the declaration +# private theorem not exported, name mangled by the elaborator +# instance a declaration with no `theorem`/`def` keyword +# nested namespace Ns.Hidden.X, reusing the basename of an audited +# declaration Ns.X — the spelling-vs-membership shape. +# The victim module, its namespace and X are all +# derived from this repo's own manifest below. +# EVERY ONE must be named in the gate's UNCLASSIFIED list. Asserting the +# gate merely failed is not enough: one shape surfacing would fail the run +# while the other three rode along unseen. +# +# One recompile of one leaf module, then the real Phase 2c. Run after a green +# check.sh. +# ───────────────────────────────────────────────────────────────────────────── +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}" +FAILURES=0 +SAFE_EXIT=0 +STASH="$(mktemp -d)" + +# Pick the victim from this repo's own manifest rather than naming a module: +# the four forks do not share a corpus (dalek and anza carry Proofs.Basic; +# risc0 and betrusted do not), and a hard-coded name would silently pick +# nothing on half of them. +# +# The victim must be (a) in check.sh's PROOFS — attacking an unmanifested module +# would test the dead-file gate instead of the walker; (b) NOT an inventory +# driver or the audit driver — those are the instruments, and mutating one would +# be attacking the measuring device; (c) imported by no other manifest module, +# so one recompile cannot invalidate a second module's artifact. Of those, take +# the smallest, because this test compiles it twice. +# +# Note for anyone re-deriving this: the inventory drivers import the whole +# corpus, so they must be excluded from the set of importers as well as from the +# candidates. Leave them in and every module looks imported, no leaf is found, +# and the test silently has no victim at all. +MAIN=$(sed -n '/^PROOFS=(/,/^)/p' "$HERE/check.sh" \ + | sed 's/#.*//; s/PROOFS=(//; s/)//' | tr -s ' \t' '\n' | sed '/^$/d') +SEARCHERS=$(for m in $MAIN; do case $m in Inventory*|Audit) ;; *) echo "$HERE/Proofs/$m.lean";; esac; done) +VICTIM_MOD=""; _best=999999 +for m in $MAIN; do + case $m in Inventory*|Audit) continue;; esac + grep -q "^import Proofs\.$m\$" $SEARCHERS 2>/dev/null && continue + n=$(wc -l < "$HERE/Proofs/$m.lean") + if [ "$n" -lt "$_best" ]; then _best=$n; VICTIM_MOD=$m; fi +done +if [ -z "$VICTIM_MOD" ]; then + echo "FATAL: no manifested leaf module to attack — the corpus shape changed."; exit 1 +fi +VICTIM_NS=$(grep -m1 '^namespace ' "$HERE/Proofs/$VICTIM_MOD.lean" | awk '{print $2}') +COLLIDE=$(grep -m1 '^theorem ' "$HERE/Proofs/$VICTIM_MOD.lean" | awk '{print $2}') +if [ -z "$VICTIM_NS" ] || [ -z "$COLLIDE" ]; then + echo "FATAL: $VICTIM_MOD has no namespace or no theorem to collide with."; exit 1 +fi + +cleanup() { + [ -f "$STASH/victim" ] && cp "$STASH/victim" "$HERE/Proofs/$VICTIM_MOD.lean" + [ "$SAFE_EXIT" -eq 1 ] || rm -f "$HERE/Proofs/$VICTIM_MOD.olean" "$HERE/Proofs/$VICTIM_MOD.ilean" + rm -rf "$STASH" +} +trap cleanup EXIT INT TERM +cp "$HERE/Proofs/$VICTIM_MOD.lean" "$STASH/victim" + +# Phase 2c lifted from the shipping button. `set -euo pipefail` is copied from +# check.sh:32 deliberately — the phase does its Lean work in subshells, and +# without -e a failing subshell is masked by the next echo. (That exact mistake +# produced a green report for a red condition while selftest-tiers.sh was being +# built; do not "simplify" it away.) +lift() { + { echo 'set -euo pipefail' + echo 'source ~/aeneas-toolchain/env.sh' + echo "HERE=\"$HERE\"" + echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"' + echo "TIMEOUT=$TIMEOUT" + # PROOFS, and the scalar manifest the coverage check consults. Both are + # lifted VERBATIM rather than re-derived here: re-deriving would let this + # test's idea of the manifest drift away from the button's, and then the + # test would be checking its own opinion instead of the shipping one. + sed -n '/^PROOFS=(/,/^)/p;/^SCALAR_SH=/p;/^SCALAR_MANIFEST=/p' "$HERE/check.sh" + awk '/^# ── Phase 2c/{f=1} f&&/^# ── (Phase 3|Phases end)/{exit} f{print}' "$HERE/check.sh" + } > "$STASH/p2c.sh" + for want in 'Phase 2c' 'inventory_gate.sh' 'PROOFS=(' 'SCALAR_MANIFEST='; do + grep -qF "$want" "$STASH/p2c.sh" || { + echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved."; exit 1; } + done +} +lift + +recompile() { + ( 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/$VICTIM_MOD.lean + " ) >/dev/null 2>&1 +} + +run_phase() { bash "$STASH/p2c.sh" 2>&1; } + +echo "=== selftest-shapes: can a declaration hide from the walker? ===" +echo " victim: Proofs/$VICTIM_MOD.lean ($_best lines), namespace $VICTIM_NS" +echo " colliding basename: $VICTIM_NS.$COLLIDE" + +if ! recompile; then + echo "FATAL: Proofs/$VICTIM_MOD.lean does not compile before any attack — fix the tree first." + exit 1 +fi + +# ── 0. control ───────────────────────────────────────────────────────────── +OUT=$(run_phase); RC=$? +if [ "$RC" -eq 0 ] && grep -qF "environment == allowlist" <<<"$OUT"; then + echo " ✓ control: the untouched tree's observation equals the allowlist" +else + echo " ✗ control: exit $RC — the tree is not green before the attack" + tail -8 <<<"$OUT" | sed 's/^/ /' + FAILURES=$((FAILURES+1)) +fi + +# ── 1. the four shapes ───────────────────────────────────────────────────── +python3 - "$HERE/Proofs/$VICTIM_MOD.lean" "$VICTIM_NS" "$COLLIDE" <<'PY' +import sys +f, ns, collide = sys.argv[1], sys.argv[2], sys.argv[3] +s = open(f).read() +end = f"\nend {ns}" +assert s.rstrip().endswith(end.strip()), "victim does not end by closing its namespace" +i = s.rstrip().rfind(end) +inject = f""" +-- selftest-shapes: four declaration shapes that defeated a source-regex +-- enumerator in ltl-accumulator-verified. Each must surface in the walker's +-- observation. Removed by this script's cleanup. +@[simp] theorem shape_attributed : True := trivial + +private theorem shape_private : True := trivial + +instance shape_instance : Nonempty Nat := ⟨0⟩ + +namespace Hidden +theorem {collide} : True := trivial +end Hidden +""" +open(f, "w").write(s[:i] + inject + s[i:]) +PY + +if ! recompile; then + echo " ✗ case 1: the module with the four shapes did not compile (case is vacuous)" + FAILURES=$((FAILURES+1)) +else + OUT=$(run_phase); RC=$? + if [ "$RC" -eq 0 ]; then + echo " ✗ case 1: FOUR hidden declarations and the inventory passed — the walker is blind" + FAILURES=$((FAILURES+1)) + else + # Not "did it fail" but "did it see each one". A gate that reports three of + # four still lets one declaration ride along inside an audited module. + MISSED=0 + for n in "$VICTIM_NS.shape_attributed" "shape_private" \ + "$VICTIM_NS.shape_instance" "$VICTIM_NS.Hidden.$COLLIDE"; do + if grep -qF "UNCLASSIFIED" <<<"$OUT" && grep -F "UNCLASSIFIED" <<<"$OUT" | grep -qF "$n"; then + echo " · seen: $n" + else + echo " · NOT SEEN: $n — this shape hides from the walker" + MISSED=1 + fi + done + if [ "$MISSED" -eq 0 ]; then + echo " ✓ case 1: all four evasive shapes surfaced as UNCLASSIFIED" + else + echo " ✗ case 1: the gate failed, but not for every shape" + grep -F "UNCLASSIFIED" <<<"$OUT" | head -8 | sed 's/^/ /' + FAILURES=$((FAILURES+1)) + fi + fi +fi + +cp "$STASH/victim" "$HERE/Proofs/$VICTIM_MOD.lean" +if recompile; then + SAFE_EXIT=1 +else + echo " ✗ restore: the ORIGINAL module no longer compiles — tree left for inspection" + FAILURES=$((FAILURES+1)) +fi + +OUT=$(run_phase); RC=$? +if [ "$RC" -eq 0 ] && grep -qF "environment == allowlist" <<<"$OUT"; then + echo " ✓ restored: the observation equals the allowlist again" +else + echo " ✗ restored: the tree did not come back green (exit $RC)" + FAILURES=$((FAILURES+1)) +fi + +echo "" +if [ "$FAILURES" -eq 0 ]; then + echo "SELFTEST PASSED — no declaration shape tested here can hide inside an" + echo "audited module: the walker reports each one by name." + exit 0 +fi +echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed." +exit 1