From 8530cc73f427ab04d3f35e1d31d3c858a11f2aa3 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Wed, 29 Jul 2026 20:13:21 +0200 Subject: [PATCH] verification: pin the harness, audit drivers and policy files (P1-c) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This repository has the estate's strongest gates, which makes them the most valuable to switch off. Until now every one of them was executed by scripts that nothing pinned. Phase 0c requires every harness file to match HARNESS.sha256 — 15 files: check.sh, lean-guard, inventory_gate.sh, run_bare.sh, all three self-tests, both audit drivers (Proofs/Inventory.lean, Proofs/AxiomCheck.lean), the policy tables (inventory-allowlist.txt, AUDIT-MANIFEST.txt), the toolchain pin, the fidelity harness and its Python transcription, and the extracted model. WHICH files must be pinned is policy and lives in check.sh, never in the map being consulted: the required set is derived from the filesystem (the executable bit, plus gen/**.lean, plus an explicit list for the rest), so deleting a pin entry is a set mismatch rather than a silent un-pinning. gen/LTLAcc/HashExternal.lean was previously bound by nothing at all — it was compiled and trusted. It is now pinned, and the derivation is by set, so a new model file fails closed. selftest_audit.sh case 9 is split rather than relabelled. Phase 0c now catches an unpinned rogue gen module BEFORE the dead-file gate runs, so asserting only the new diagnostic would have quietly retired the dead-file gate from the test suite. 9a asserts the harness-set mismatch on the unpinned file; 9b pins it — an author who added it deliberately — and asserts Phase 2 still dies with DEAD FILE (gen). Ten cases now, all defeated. KNOWN-GAPS and the trusted base record the circularity plainly: an author who edits a script and refreshes its pin in one commit passes every phase. The pin removes the silent path, not the possibility. Review at the pinned commit remains the consumer's protection. Verified green after the fix: button (75s), harness self-test, binding self-test, and the ten-case audit self-test. ATTESTATION GREEN (Lean + fidelity), all fidelity case counts identical to the pre-change run. Co-Authored-By: Claude Opus 4.8 --- verification/HARNESS.sha256 | 15 +++++ verification/check.sh | 53 +++++++++++++++ verification/selftest-harness.sh | 108 +++++++++++++++++++++++++++++++ verification/selftest_audit.sh | 30 +++++++-- 4 files changed, 199 insertions(+), 7 deletions(-) create mode 100644 verification/HARNESS.sha256 create mode 100755 verification/selftest-harness.sh 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