From 18e8753a62401df013c00e56e3a054ff3f52d200 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Wed, 29 Jul 2026 20:12:57 +0200 Subject: [PATCH] verification: pin the harness, the audit drivers and the policy files (P1-c) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Every gate this repository has was executed by scripts that 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; 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 — and every gate added this week made that gap more valuable to an attacker, not less. Phase 0c requires every harness file to match HARNESS.sha256. Two design points carry the weight: - WHICH files must be pinned is POLICY and lives in check.sh, never in the map being consulted. If the required set were read from the pin file, deleting an entry would silently un-pin that file. It is instead derived from the filesystem, so a deleted entry is a set mismatch and a build failure. That is the exact defect SLH-DSA round-6 found, closed here by construction. - Membership self-derives 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. Load-bearing files that are not executable — the audit driver, the committed manifests, the policy tables — cannot be discovered that way and are listed explicitly. lean-guard is inside the set, which finally makes the standing "lean-guard stays hash-pinned" rule a property of the repository rather than a convention. selftest-harness.sh replays five cases, each asserting a specific diagnostic: an edited lean-guard, a new unpinned executable, a deleted pin entry, a missing pin file, and a positive control. It was itself negative-tested — with the hash comparison removed it goes red on exactly that case while cheerfully reporting "10 harness files match their pins". TRUSTED-BASE.md states the limit at equal length to the claim: pinning a harness from inside that harness is circular, and an author who edits a script 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 being reviewed. A green button says "this is the apparatus that was reviewed", never "this apparatus is trustworthy". Also fixed, found by this sweep: both self-tests compared the working tree against its starting state with `diff <(echo "$VAR") <(command)`, which is asymmetric — for a clean tree the variable is empty and `echo` emits a blank line the command does not. It reported a difference precisely when nothing was wrong, and only surfaced once P1-a was committed and Proofs/ became clean. Both now compare as strings. Verified green: 20 runs across the four ed25519 repositories (four buttons, four harness self-tests, four axiom-gate self-tests, four binding self-tests, four scalar buttons), zero red. Co-Authored-By: Claude Opus 4.8 --- TRUSTED-BASE.md | 24 +++++++ verification/HARNESS.sha256 | 10 +++ verification/check.sh | 48 +++++++++++++ verification/selftest-axgate.sh | 11 +-- verification/selftest-harness.sh | 108 ++++++++++++++++++++++++++++ verification/selftest-statements.sh | 8 ++- 6 files changed, 203 insertions(+), 6 deletions(-) create mode 100644 verification/HARNESS.sha256 create mode 100755 verification/selftest-harness.sh diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 3509eaa..d4adc15 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -86,3 +86,27 @@ running Rust code. Everything else is machine-checked. 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. + +9. **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". diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 new file mode 100644 index 0000000..4877077 --- /dev/null +++ b/verification/HARNESS.sha256 @@ -0,0 +1,10 @@ +c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4 AUDIT-MANIFEST.txt +64df281594fd38ac42aa06623839608a7fba74b0d91994c114b55e25a9233a33 check-scalar.sh +3259a791ce6996023909e7ea1033d55f73fc2881128787f383daa606c83fb2f1 check.sh +c0fd4ba1fdec8a6f37b28b5fbe3fc7e93a54f1365443d365ca44c48c117c56b7 extract.sh +d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4 GEN-MODEL.sha256 +736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard +79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8 Proofs/Audit.lean +79611f9689ba714fb8d3f57aee86ad9655509303445beaad766bf8b049de8c44 selftest-axgate.sh +3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh +a14acaafe914aabb9df44fcd05fd50d475804280fab9e332fdb5ea0b0d35f164 selftest-statements.sh diff --git a/verification/check.sh b/verification/check.sh index 09f2911..a200b8d 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -189,6 +189,54 @@ if ! ( cd "$HERE/gen" && sha256sum -c --quiet "$HERE/GEN-MODEL.sha256" ) ; then 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 diff --git a/verification/selftest-axgate.sh b/verification/selftest-axgate.sh index b214926..140f0a1 100755 --- a/verification/selftest-axgate.sh +++ b/verification/selftest-axgate.sh @@ -113,11 +113,14 @@ fi # 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. -if ! diff -q <(echo "$TREE_AT_START") \ - <(cd "$HERE/.." && git status --porcelain -- verification/Proofs) >/dev/null; then +# 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 <(echo "$TREE_AT_START") \ - <(cd "$HERE/.." && git status --porcelain -- verification/Proofs) | sed 's/^/ /' + 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" 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