diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 64e9e76..335a36e 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -92,3 +92,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. + +10. **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..dc9b4f2 --- /dev/null +++ b/verification/HARNESS.sha256 @@ -0,0 +1,10 @@ +6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt +b88f4bc16d3188f4830f8333201fc7826d46acf829c37f7da398d6ae9bfca15e check-scalar.sh +813c31664484adddd1752ea3bb30da826ad1050fd378604c242bcafb105fb4a3 check.sh +afa13c814ba9757de8d59777524e496653351112a1a7037a56f1b0b436b28cf9 extract.sh +0ea20d74cd359da404ee3be116058374cbb9fd992ed170e5f6c64f8d7a6b2733 GEN-MODEL.sha256 +736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard +772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 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 b0293f0..df44168 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -186,6 +186,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