mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-03 20:13:47 +00:00
P2-a': can a declaration hide from the inventory walker?
Phase 2c exists because a source-regex enumerator proved evadable in ltl-accumulator-verified: attributed, private and `instance` declarations and a nested-namespace basename collision all slipped past it. The fix was to stop reading source text and ask the Lean environment, and that fix was ported here. But a fix ported is not a fix tested. selftest-inventory.sh proves the GATE reacts to a difference; it feeds synthetic observations and never runs the walker. Nothing here had ever asked whether the WALKER SEES a declaration written in an evasive shape. selftest-shapes.sh adds all four shapes to an audited module, recompiles it, runs the real Phase 2c, and requires each one to be NAMED in the UNCLASSIFIED list. Asserting that the gate merely failed would not do: one shape surfacing fails the run while the other three ride along unseen. All four forks report all four. Negative-tested by removing the injection — the run then reports the walker blind and fails. The victim module is derived from each repo's own manifest, not named: the forks do not share a corpus (dalek/anza attack Proofs.Basic, risc0/betrusted Proofs.DecompressMain), and a hard-coded name would have silently found nothing on half of them. It must be manifested, must not be an inventory or audit driver, and must be imported by no other manifest module. Two notes for whoever edits this next. When re-deriving a leaf module, the inventory drivers must be excluded from the set of IMPORTERS as well as from the candidates: they import the whole corpus, so leaving them in makes every module look imported, finds no leaf, and the test silently has no victim at all. And a lift of Phase 2c needs SCALAR_SH/SCALAR_MANIFEST alongside PROOFS, or the coverage check dies on an unbound variable. New executable pinned in HARNESS.sha256. Certified by a full sweep: both buttons, all four forks, purged trees, machine otherwise idle. 8/8 green.
This commit is contained in:
parent
9f7e0ee594
commit
054a35413a
3 changed files with 233 additions and 0 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
223
verification/selftest-shapes.sh
Executable file
223
verification/selftest-shapes.sh
Executable file
|
|
@ -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
|
||||
Loading…
Reference in a new issue