commit 31f00fe756c6a9cf197bb482280357f22aa7e4a6 Author: mrwulf Date: Wed Jul 22 21:00:57 2026 +0200 SLH-DSA (FIPS 205) campaign skeleton: honest zero-certificate state Subject pinned: integritychain/fips205 @ 30bac08 via saymrwulf/fips205-source @ 5dca0db. Parameter set SLH-DSA-SHA2-128s. Scope: verify path only (slh_verify -> ... -> chain); six SHA-2 hash oracles opaque per the standing boundary. Gate-0 record (2026-07-22): charon clean on the full verify cone; aeneas translates everything except the Hashers fn-pointer struct (3 unique errors, the sole obstruction) -> phase 1 = named-opaque- free-function compat patch in the snapshot repo, the established dalek sha512-shim pattern. check.sh exits non-green and says NOTHING PROVEN YET (H5, R3). lean-guard copied; every future compile runs under it (S1, S2). Co-Authored-By: Claude Fable 5 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..f41f5ec --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +*.olean +target/ +.lake/ diff --git a/README.md b/README.md new file mode 100644 index 0000000..013950e --- /dev/null +++ b/README.md @@ -0,0 +1,86 @@ +# fips205-slhdsa-verified + +Machine-checked verification campaign for the **SLH-DSA (FIPS 205) verify +path**, extracted from a pure-Rust implementation into Lean 4 via +Charon/Aeneas — the same pipeline, discipline, and honesty rules as the +four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`). + +## STATUS: SKELETON — NOTHING PROVEN YET + +There are **zero certificates** in this repository. `verification/check.sh` +exits non-green and says so. Every claim in this README below the line +"What will be claimed" is a *plan*, not a result. (Honesty invariant H5: +an honest gap outranks a hollow certificate.) + +## Subject + +- Upstream: `integritychain/fips205` — pure-Rust FIPS 205 (final standard, + 2024-08-13), zero `unsafe`, `no_std`, const-generic parameterization, + modules mirroring the FIPS 205 algorithm structure. +- Pinned at upstream commit `30bac08580aa61f653e5436d1bbacb5ffac446c4` + (2025-09-01), snapshotted with full history at + `saymrwulf/fips205-source` (snapshot head `5dca0db`, whose single + deviation from verbatim is the removal of upstream CI workflows, + documented in that commit). Aeneas-compat patches will land in the + snapshot repo as transparent, individually-justified commits — never + upstream. **No affiliation with, and no changes proposed to, the + upstream project.** +- Parameter set: **SLH-DSA-SHA2-128s** first (the small-signature profile + deployed in the firmware/code-signing lane). The architecture + generalizes; each further parameter set is a separate claim (rigor + invariant R2). + +## Scope + +**Verify path only.** The extraction cone, mirroring FIPS 205's own +algorithm tree: + +``` +slh_verify -> slh_verify_internal + -> fors_pk_from_sig + -> ht_verify -> xmss_pk_from_sig -> wots_pk_from_sig -> chain +``` + +Key generation and signing are out of scope (trusted base), exactly as +ed25519 signing was. The six hash oracles (`h_msg, prf, f, h, t_l, +t_len` — SHA-2 instantiations) are opaque external models with written +justifications, kept outside every certificate's dependency cone +(honesty invariant H4); their semantics are the standing SHA-2 oracle +boundary documented in [TRUSTED-BASE.md](TRUSTED-BASE.md). + +## Gate-0 record (2026-07-22) + +Per TARGETS.md ("re-verify before use"), the subject was probed before +this repository was created: + +- **Charon**: clean (`charon cargo --preset=aeneas`, roots at the verify + cone, `sha2/sha3/zeroize/rand_core` opaque, features + `slh_dsa_sha2_128s`) — LLBC produced, exit 0. +- **Aeneas**: translated the entire const-generic verify cone to Lean + definitions (`wots.chain` … `slh.slh_verify_internal` all generated), + with exactly **one obstruction class** (3 unique errors): the + `crate::hashers::Hashers` struct of plain **function pointers** cannot + be translated. +- **Consequence (campaign phase 1)**: an Aeneas-compat patch in + `fips205-source` will replace the fn-pointer struct with named opaque + free functions on the verify path — the same pattern as the + `sha512_new/update/finalize` shims in `curve25519-dalek-source`'s + verify glue. Until that patch lands, `verification/extract.sh` + documents intent and produces a partial model. + +## What will be claimed (when the button is green, not before) + +One theorem per layer, each a statement about the **extracted** functions +(H3), compiled by `verification/check.sh` with `#print axioms` reporting +exactly `[propext, Classical.choice, Quot.sound]` (H1): chain semantics, +WOTS+ pk recomputation, XMSS path recomputation, hypertree acceptance, +FORS pk recomputation, and the apex — `slh_verify_internal` accepts iff +the recomputed hypertree root equals the pinned public-key root, under +the stated oracle boundary. + +## Discipline + +Every Lean compile in this repository runs under `verification/lean-guard` +(memory-capped, machine-wide serialized). Extraction is reproducible from +the committed `extract.sh` against the pinned snapshot (R1). What cannot +be proven is named in [TRUSTED-BASE.md](TRUSTED-BASE.md), not hidden (H5). diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md new file mode 100644 index 0000000..da13d58 --- /dev/null +++ b/TRUSTED-BASE.md @@ -0,0 +1,30 @@ +# TRUSTED-BASE — what the certificates will NOT cover + +Initial statement, written at skeleton time (nothing proven yet); this +file is maintained as the campaign proceeds and is part of every claim. + +1. **The six hash oracles.** `h_msg, prf, f, h, t_l, t_len` + (SLH-DSA-SHA2-128s instantiations over SHA-256) are modeled as opaque + functions with assumed functional behavior. Their correctness against + FIPS 180-4 is NOT proven here — the same standing boundary as SHA-512 + in the ed25519 apex. A collision or misimplementation inside the hash + layer is invisible to these certificates. +2. **Signing and key generation.** Out of extraction scope entirely. A + verified verify path says nothing about the safety of signature or key + production (including randomness). +3. **The transpilation pair.** Charon and Aeneas (pinned versions in the + toolchain) are trusted to preserve semantics from Rust (MIR) to the + Lean model. Divergence between rustc's semantics and the extracted + model is trusted base. +4. **The Lean kernel and its three axioms** + (`propext, Classical.choice, Quot.sound`). +5. **Build correspondence.** No reproducible-builds claim: the proof is + about the pinned source, not about any particular compiled binary + (the estate's R5 gap, stated everywhere it matters). +6. **Parameter-set scope.** Claims will bind SLH-DSA-SHA2-128s only; + other parameter sets are unverified until separately extracted and + proven (R2). +7. **Aeneas-compat patch surface.** The fn-pointer-to-named-oracle + rewrite in `fips205-source` (phase 1) is part of the verified surface: + the certificate covers the patched verify path, and the patch commits + are the auditable delta from upstream `30bac08`. diff --git a/verification/Proofs/.gitkeep b/verification/Proofs/.gitkeep new file mode 100644 index 0000000..e69de29 diff --git a/verification/check.sh b/verification/check.sh new file mode 100755 index 0000000..6e93d22 --- /dev/null +++ b/verification/check.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +# The one-button claim for this repository (rigor invariant R3). +# Green output == the full claim. This script is the ONLY source of the +# word "proven" for this repo. +set -euo pipefail + +echo "fips205-slhdsa-verified — check" +echo "================================" +echo "SKELETON: 0 certificates. NOTHING PROVEN YET." +echo "Campaign phase 1 (Aeneas-compat patch + clean extraction) has not" +echo "landed. See README.md 'Gate-0 record' and TRUSTED-BASE.md." +exit 1 diff --git a/verification/extract.sh b/verification/extract.sh new file mode 100755 index 0000000..b9e72c3 --- /dev/null +++ b/verification/extract.sh @@ -0,0 +1,52 @@ +#!/usr/bin/env bash +# Regenerate the Lean model in gen/ from the pinned fips205 snapshot. +# +# SCOPE: the SLH-DSA verify path, parameter set SLH-DSA-SHA2-128s +# roots: slh_verify(_internal), fors_pk_from_sig, ht_verify, +# xmss_pk_from_sig, wots_pk_from_sig, chain +# (sign/keygen are out of scope; the six hash oracles are opaque — +# see TRUSTED-BASE.md.) +# +# Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean +# +# PHASE-1 PRECONDITION (gate-0 finding, 2026-07-22): upstream models the +# hash family as `crate::hashers::Hashers`, a struct of plain function +# pointers, which Aeneas cannot translate (3 unique errors, the only +# obstruction in the whole cone). Until the Aeneas-compat patch in +# fips205-source replaces that struct with named opaque free functions +# on the verify path (the curve25519-dalek-source sha512-shim pattern), +# this script produces a PARTIAL model. Do not build proofs on a partial +# model; check.sh stays non-green until extraction is clean. +# +# Usage: ./extract.sh +set -euo pipefail + +source ~/aeneas-toolchain/env.sh +HERE="$(cd "$(dirname "$0")" && pwd)" +CRATE=~/GitClone/FormalVerification/sources/fips205-source + +echo "[1/2] charon: Rust -> LLBC (verify cone, SHA2-128s, hash oracles opaque)" +cd "$CRATE" +charon cargo --preset=aeneas \ + --start-from 'crate::slh::slh_verify' \ + --start-from 'crate::slh::slh_verify_internal' \ + --start-from 'crate::fors::fors_pk_from_sig' \ + --start-from 'crate::hypertree::ht_verify' \ + --start-from 'crate::xmss::xmss_pk_from_sig' \ + --start-from 'crate::wots::wots_pk_from_sig' \ + --start-from 'crate::wots::chain' \ + --opaque 'sha2' --opaque 'sha3' --opaque 'zeroize' --opaque 'rand_core' \ + --opaque 'crate::hashers::sha2_cat_1' \ + --opaque 'crate::hashers::sha2_cat_3_5' \ + --opaque 'crate::hashers::shake' \ + --hide-marker-traits \ + --dest-file "$HERE/SlhVerify.llbc" \ + -- --no-default-features --features slh_dsa_sha2_128s + +echo "[2/2] aeneas: LLBC -> Lean (split files, SlhVerify.* modules;" +echo " hand-maintained TypesExternal.lean / FunsExternal.lean are" +echo " NOT overwritten once they exist)" +cd "$HERE" +aeneas -backend lean -split-files -subdir SlhVerify -dest gen SlhVerify.llbc + +echo "Done. Now run ./check.sh (expect non-green until phase 1 lands)." diff --git a/verification/lean-guard b/verification/lean-guard new file mode 100755 index 0000000..5f03315 --- /dev/null +++ b/verification/lean-guard @@ -0,0 +1,189 @@ +#!/usr/bin/env bash +# ──────────────────────────────────────────────────────────────────────────── +# lean-guard — HARD-CAPPED Lean compiler wrapper. +# +# Successor to lean-safe after the 2026-07-02 OOM incident: a single `lean` +# elaboration (tactic-search blowup: simp[*]/scalar_tac over a ~60-hypothesis +# context with 2^256-scale literals) grew to 12.2GB RSS and was killed by the +# GLOBAL kernel OOM killer, taking the driving session down with it. +# lean-safe's guards (timeout + affinity + PREFLIGHT headroom) cannot stop +# that: the process passes preflight, then balloons inside its timeout. +# +# NEW GUARDS (in addition to all lean-safe guards): +# A. lean -M — Lean's internal cap: elaboration aborts +# with a clean "maximum memory exceeded" +# error. First line of defense; graceful. +# B. systemd-run --user --scope +# -p MemoryMax / MemorySwapMax — kernel cgroup cap around the process: +# if Lean's own accounting misses (C-level +# allocations), the cgroup kills ONLY this +# lean, never the session, never the box. +# C. flock on /tmp/lean-guard.lock — machine-wide single-flight: at most ONE +# lean compile at a time, regardless of +# how many agents/scripts are active. +# +# Env knobs (defaults for this 14GB / 8-core ThinkPad): +# LEAN_TIMEOUT per-file wall clock seconds (default 400) +# LEAN_MEM_MB lean -M internal cap, MB (default 4096) +# LEAN_CGROUP_MB cgroup MemoryMax, MB (default LEAN_MEM_MB+1024) +# LEAN_MAX_CORES taskset core range (default 0-3) +# LEAN_MIN_FREE_MB preflight available-RAM floor (default 3072) +# LEAN_LOCK_WAIT max seconds to wait for the lock (default 7200) +# +# Usage: lean-guard [extra lean args...] +# The .olean output path is always computed as ${file%.lean}.olean. +# Requires: lean on PATH (caller sources the toolchain env; typically run +# inside `lake env` so LEAN_PATH is set — this wrapper does NOT clobber env). +# ──────────────────────────────────────────────────────────────────────────── +set -uo pipefail + +# No core dumps: hitting the memory cap makes lean (and uutils `timeout`) abort; +# those aborts are EXPECTED and their core dumps only trigger Ubuntu apport +# popups and fill /var/crash. ulimit applies to this shell and every child. +ulimit -c 0 2>/dev/null || true + +TIMEOUT_SEC=${LEAN_TIMEOUT:-400} +MEM_MB=${LEAN_MEM_MB:-4096} +CGROUP_MB=${LEAN_CGROUP_MB:-$((MEM_MB + 1024))} +CORES=${LEAN_MAX_CORES:-0-3} +MIN_FREE_MB=${LEAN_MIN_FREE_MB:-3072} +LOCK_WAIT=${LEAN_LOCK_WAIT:-7200} +LOCK_FILE=/tmp/lean-guard.lock +LOG_FILE="${HOME}/.lean-guard.log" + +if ! command -v lean &>/dev/null; then + echo "FATAL: lean not on PATH — source ~/aeneas-toolchain/env.sh (and run inside lake env)" + exit 1 +fi +if [ $# -eq 0 ]; then + echo "Usage: lean-guard [lean args...]" + exit 1 +fi + +LEAN_FILE="$1"; shift || true + +# ── Guard 1: source integrity (anti olean-clobber) ────────────────────────── +if [ ! -f "$LEAN_FILE" ]; then + echo "MISSING: $LEAN_FILE"; exit 1 +fi +if ! grep -qE '^[[:space:]]*(/-|import |namespace |theorem |def |open |set_option |--)' "$LEAN_FILE" 2>/dev/null; then + echo "FATAL: $LEAN_FILE is not Lean source (binary/olean data?)." + echo " Restore: git checkout HEAD -- $LEAN_FILE" + exit 1 +fi + +# ── Guard 2: output path ───────────────────────────────────────────────────── +case "$LEAN_FILE" in + *.lean) ;; + *) echo "FATAL: input lacks .lean extension"; exit 1 ;; +esac +OLEAN_FILE="${LEAN_FILE%.lean}.olean" +[ "$OLEAN_FILE" = "$LEAN_FILE" ] && { echo "FATAL: output would clobber source"; exit 1; } + +# ── Guard C: machine-wide single-flight ───────────────────────────────────── +exec 9>"$LOCK_FILE" +if ! flock -w "$LOCK_WAIT" 9; then + echo "FATAL: could not acquire lean-guard lock within ${LOCK_WAIT}s (another compile stuck?)" + exit 1 +fi + +# ── Guard 3: preflight headroom (after lock: serialized measurement) ──────── +AVAIL_MB=$(free -m | awk '/Mem:/{print $7}') +if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then + echo "FATAL: only ${AVAIL_MB}MB available (< ${MIN_FREE_MB}MB floor) — refusing to compile" + exit 1 +fi + + +# ── Guard 3b: global-headroom clamp (2026-07-03 swap-pressure incident) ───── +# A cap is a PROMISE of memory to lean; never promise more than the machine +# can afford right now. Requested caps that exceed (available − floor) are +# clamped, so raising LEAN_MEM_MB can no longer starve the rest of the system +# into swap even when lean itself stays within its cap. Clamp, don't fail: +# most compiles peak far below their cap (measure before raising — the +# incident's 9G scopes served a file whose true peak was 753MB). +REQ_MEM_MB=$MEM_MB +WAS_CLAMPED=0 +MAX_AFFORD_MB=$(( AVAIL_MB - MIN_FREE_MB )) +if [ "$MEM_MB" -gt "$MAX_AFFORD_MB" ]; then + echo "lean-guard: clamping -M ${MEM_MB} -> ${MAX_AFFORD_MB}MB (avail=${AVAIL_MB}MB, floor=${MIN_FREE_MB}MB)" + MEM_MB=$MAX_AFFORD_MB + CGROUP_MB=$(( MEM_MB + 1024 )) + WAS_CLAMPED=1 +fi +if [ "$MEM_MB" -lt 1024 ]; then + echo "FATAL: headroom clamp would leave lean < 1024MB — machine too loaded to compile safely" + exit 1 +fi + +echo "[$(date -u +%F' '%T)] $LEAN_FILE (t=${TIMEOUT_SEC}s M=${MEM_MB}MB cg=${CGROUP_MB}MB cores=$CORES avail=${AVAIL_MB}MB)" >> "$LOG_FILE" + +# ── Compile under both caps ────────────────────────────────────────────────── +run_leancmd() { + taskset -c "$CORES" \ + timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \ + lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@" +} +do_compile() { + if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; then + # --scope runs the command as a child of THIS shell (env inherited), + # merely placing it in a fresh cgroup with the hard caps below. + systemd-run --user --scope --quiet \ + -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \ + -- taskset -c "$CORES" \ + timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \ + lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@" + else + echo " (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE" + run_leancmd "$@" + fi +} +do_compile "$@" +EXIT_CODE=$? + +# ── Guard 3a: lazy wait-and-retry after a clamped memory abort (pass 3) ───── +# The clamp above protects the host, but under ambient memory pressure it +# can cut a KNOWN-NEEDED cap (ReduceSpec peaks ~6.5G) and guarantee an +# interpreter abort that reads like a proof regression. Lazy semantics keep +# light files free: only when a CLAMPED run dies on memory (134 abort / +# 137 cgroup kill) and LEAN_MEM_WAIT_SEC>0, wait — still under the +# single-flight lock — until the ORIGINAL request is affordable, then retry +# once at full cap. Default 0: behavior unchanged. +MEM_WAIT_SEC=${LEAN_MEM_WAIT_SEC:-0} +if [ "$WAS_CLAMPED" -eq 1 ] && [ "$MEM_WAIT_SEC" -gt 0 ]; then + WAITED=0 + # Retry ladder: whenever headroom improves MATERIALLY (>= +1536MB over + # the cap that just died, or reaches the full request), retry at the + # new clamp. The full request may never be affordable on a loaded host + # even though the true peak is — climbing the ladder finds the passing + # clamp without knowing the peak. Monotone caps + deadline => bounded. + while { [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; } \ + && [ "$WAITED" -lt "$MEM_WAIT_SEC" ] && [ "$MEM_MB" -lt "$REQ_MEM_MB" ]; do + sleep 20; WAITED=$(( WAITED + 20 )) + AVAIL_MB=$(free -m | awk '/Mem:/{print $7}') + NEW_AFFORD=$(( AVAIL_MB - MIN_FREE_MB )) + if [ "$NEW_AFFORD" -ge "$REQ_MEM_MB" ] || [ "$NEW_AFFORD" -ge $(( MEM_MB + 1536 )) ]; then + MEM_MB=$(( NEW_AFFORD < REQ_MEM_MB ? NEW_AFFORD : REQ_MEM_MB )) + CGROUP_MB=$(( MEM_MB + 1024 )) + echo "lean-guard: clamped run died (rc=$EXIT_CODE); retrying at -M ${MEM_MB}MB after ${WAITED}s (avail=${AVAIL_MB}MB, request=${REQ_MEM_MB}MB)" + echo "[$(date -u +%F' '%T)] RETRY $LEAN_FILE (M=${MEM_MB}MB cg=${CGROUP_MB}MB avail=${AVAIL_MB}MB after ${WAITED}s)" >> "$LOG_FILE" + do_compile "$@" + EXIT_CODE=$? + fi + done + if [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; then + echo "lean-guard: memory-death persists after ${WAITED}s of ladder retries (last -M ${MEM_MB}MB, request ${REQ_MEM_MB}MB) — keeping the failure" + fi +fi + +case $EXIT_CODE in + 0) echo " OK" >> "$LOG_FILE" ;; + 124) echo " TIMEOUT ${TIMEOUT_SEC}s" >> "$LOG_FILE" + echo "TIMEOUT: $LEAN_FILE exceeded ${TIMEOUT_SEC}s" ;; + 137) echo " KILLED (cgroup MemoryMax ${CGROUP_MB}MB hit)" >> "$LOG_FILE" + echo "KILLED: $LEAN_FILE hit the ${CGROUP_MB}MB cgroup cap (contained — machine unharmed)" ;; + *) echo " FAILED exit $EXIT_CODE (lean error, possibly '-M ${MEM_MB}MB exceeded')" >> "$LOG_FILE" ;; +esac +# stale partial olean from a failed compile must not poison later imports +[ $EXIT_CODE -ne 0 ] && rm -f "$OLEAN_FILE" +exit $EXIT_CODE