diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 new file mode 100644 index 0000000..eb9e2e4 --- /dev/null +++ b/verification/HARNESS.sha256 @@ -0,0 +1,15 @@ +e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c AUDIT-MANIFEST.txt +7ab1bfbafc8ac9ab34d1e0eaa71ba2f1f9912121345cc1af281bcb1d2ec30ad2 check.sh +070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885 fidelity/lean_defs.py +5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2 fidelity/run_fidelity.py +503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf gen/LTLAcc/HashExternal.lean +f1eb5cdd158e30df14c59065fe2050448c77b5262b282208fa831d050f6b6a71 inventory-allowlist.txt +f66fb98d2a09503d9bd0d60dc964545eea6dc94b9bbb9246d1021195b79f2601 inventory_gate.sh +736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard +ce4c4e3d87434b9663f46de25ce34b48a0cf0d392e0a320a0787b4674a2d7b61 lean-toolchain +eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87 Proofs/AxiomCheck.lean +25344c8441077277addd6b4eb769b2c0e3b173afc28d3a6e8aeba0580c22a87f Proofs/Inventory.lean +0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e run_bare.sh +67a44e0db818efc48dede26f73f76f1221424bb23e40e29d859b12d0d300403b selftest_audit.sh +3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh +cf6d4d8210e224a054d4ab693c28c83e7a9ddebda05da47d6ec311d825a606c0 selftest_statements.sh diff --git a/verification/check.sh b/verification/check.sh index 23d021f..c304ffe 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -116,6 +116,59 @@ while IFS= read -r -d '' o; do [ -f "${o%.olean}.lean" ] || { echo "ORPHAN OLEAN: $o has no sibling .lean (stale artifact)"; exit 1; } done < <(find "$HERE" -name '*.olean' -print0) +# ── Phase 0c: harness integrity ───────────────────────────────────────────── +# WHY. Every gate below 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 its button printed ALL GREEN in 3.6 seconds over +# deliberately destroyed proofs. Depth of checking is worth nothing if the +# thing doing the checking is unbound — and this repo's gates are the estate's +# strongest, which makes them the most valuable to switch off. +# +# 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 that file +# instead of failing the build. +# +# Membership is SELF-DERIVING from two sources the filesystem can answer: the +# executable bit (anything this script can shell out to) and gen/**.lean (the +# extracted model, which nothing else byte-pins in this repo). Load-bearing +# files that are neither — the audit drivers, the policy tables, the toolchain +# pin, the fidelity harness — cannot be discovered and are listed explicitly. +HARNESS_EXTRA=( + AUDIT-MANIFEST.txt # the statement block Phase 3d's digest is taken over + inventory-allowlist.txt # the pinned audit surface Phase 3b diffs against + lean-toolchain # which Lean the corpus claims to have been checked by + fidelity/lean_defs.py # the Python transcription the differential compares + fidelity/run_fidelity.py # the differential itself + Proofs/Inventory.lean # audit driver: emits the inventory AND the statements + Proofs/AxiomCheck.lean # audit driver: the #print axioms queries of Phase 3 +) +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 +# check.sh 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 one +# commit — nothing executed by the harness can. The defence there is that both +# changes appear in the diff at the pinned commit. +HARNESS_REQUIRED=$( { find "$HERE" -type f -executable -not -path '*/.git/*' -printf '%P\n' + find "$HERE/gen" -type f -name '*.lean' -printf 'gen/%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" + echo "=== Phase 1: stub + axiom-smuggling audit ===" if grep -rn 'by trivial' "$HERE"/Proofs/*.lean 2>/dev/null; then echo "STUB DETECTED"; exit 1; fi diff --git a/verification/selftest-harness.sh b/verification/selftest-harness.sh new file mode 100755 index 0000000..6425d3f --- /dev/null +++ b/verification/selftest-harness.sh @@ -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