diff --git a/.gitignore b/.gitignore index ca82639..16c7452 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,6 @@ dogfood/quorum/*/Cargo.lock dogfood/quorum/*/target/ dogfood/state/quorum/ paper/eprint-submission.md +dogfood/quorum/.build-slhdsa/ +dogfood/quorum/verify-slhdsa/Cargo.toml +dogfood/quorum/verify-slhdsa/Cargo.lock diff --git a/dogfood/quorum/build-verify-slhdsa.sh b/dogfood/quorum/build-verify-slhdsa.sh new file mode 100755 index 0000000..24ff35c --- /dev/null +++ b/dogfood/quorum/build-verify-slhdsa.sh @@ -0,0 +1,102 @@ +#!/usr/bin/env bash +# Build pacta-verify-slhdsa from the PINNED proven source. +# +# The pinned checkout is never modified. This script exports the pinned commit +# into a scratch tree, applies expose-mono.patch there, builds against that, and +# records exactly what went in. If the pinned checkout is dirty, or is not at +# the commit the attestation names, it refuses: a quorum member built from a +# tree nobody can identify is a quorum member that proves nothing. +set -euo pipefail + +HERE="$(cd "$(dirname "$0")" && pwd)" +SRC="${FIPS205_SOURCE:-$HOME/GitClone/FormalVerification/sources/fips205-source}" +PIN="${FIPS205_PIN:-a3ce8e8}" +BUILD="${BUILD_DIR:-$HERE/.build-slhdsa}" +OUT="$HERE/verify-slhdsa/target/release/pacta-verify-slhdsa" + +echo "=== pacta-verify-slhdsa: build from the proven source ===" + +[ -d "$SRC/.git" ] || { echo "FATAL: '$SRC' is not a git checkout of fips205-source."; exit 2; } +HEAD_SHA="$(git -C "$SRC" rev-parse HEAD)" +case "$HEAD_SHA" in + "$PIN"*) ;; + *) echo "FATAL: pinned source is at ${HEAD_SHA:0:8}, expected $PIN." + echo " The certificates cover $PIN. Building a 'proven' verifier from any" + echo " other tree would be a claim nobody can check."; exit 1;; +esac +if [ -n "$(git -C "$SRC" status --porcelain)" ]; then + echo "FATAL: the pinned source has uncommitted changes:" + git -C "$SRC" status --porcelain | sed 's/^/ /' + echo " Refusing: the binary must correspond to a nameable tree."; exit 1 +fi +echo " pinned source $SRC @ ${HEAD_SHA:0:8} (clean)" + +# Export the pinned commit, never a working copy. +rm -rf "$BUILD"; mkdir -p "$BUILD" +git -C "$SRC" archive --format=tar "$HEAD_SHA" | tar -x -C "$BUILD" +echo " exported $(find "$BUILD" -type f | wc -l) files from $PIN" + +# --- the two changes, applied verbatim and then VERIFIED to be present ------- +LIB="$BUILD/src/lib.rs"; VM="$BUILD/src/verify_mono.rs" +grep -q '^mod verify_mono;' "$LIB" || { echo "FATAL: 'mod verify_mono;' not found in lib.rs — the source moved."; exit 1; } +# The crate is `#![deny(missing_docs)]`, so a module cannot become public +# without a doc comment. The comment is part of the visibility change, not an +# extra edit: `pub mod` alone does not compile here. +sed -i 's|^mod verify_mono;|/// Aeneas-compat monomorphic verify path: the extraction root the eleven\n/// certificates cover (apex `fips205.slh_verify_128s_accepts_iff`). Public only\n/// so a quorum binary can call the proven function; see expose-mono.patch.\npub mod verify_mono;|' "$LIB" + +cat >> "$VM" <<'RUST' + +/// Byte-level entry to the PROVEN root, for out-of-crate callers. +/// +/// Assembles arguments only; the body is the crate's own test helper +/// `internal_inputs` followed by the call. `mprime` is FIPS 205's M' and is +/// built by the CALLER — its construction is outside every certificate +/// (TRUSTED-BASE item 10), which is why it is a parameter and not computed +/// here. +pub fn verify_mono_bytes(mprime: &[u8], sig_bytes: &[u8; 7856], pk_bytes: &[u8; 32]) -> bool { + let mut pk_seed = [0u8; 16]; + let mut pk_root = [0u8; 16]; + pk_seed.copy_from_slice(&pk_bytes[0..16]); + pk_root.copy_from_slice(&pk_bytes[16..32]); + let pk = SlhPublicKey { pk_seed, pk_root }; + let sig = SlhDsaSig::<12, 7, 9, 14, 35, 16>::deserialize(sig_bytes); + slh_verify_128s(mprime, &sig, &pk) +} +RUST + +# The extraction root must be untouched. Compare it against the pinned tree. +if ! diff <(git -C "$SRC" show "$HEAD_SHA:src/verify_mono.rs") \ + <(head -n "$(git -C "$SRC" show "$HEAD_SHA:src/verify_mono.rs" | wc -l)" "$VM") > /dev/null; then + echo "FATAL: the patch altered existing lines of verify_mono.rs, not just appended." + exit 1 +fi +echo " patched lib.rs visibility + verify_mono_bytes appended (existing lines unchanged)" + +# --- render Cargo.toml from the template ------------------------------------ +sed "s|{{SOURCE}}|$BUILD|g" "$HERE/verify-slhdsa/Cargo.toml.template" > "$HERE/verify-slhdsa/Cargo.toml" + +echo " building..." +( cd "$HERE/verify-slhdsa" && cargo build --release 2>&1 | tail -5 | sed 's/^/ /' ) + +[ -x "$OUT" ] || { echo "FATAL: build produced no binary at $OUT"; exit 1; } + +cat > "$HERE/verify-slhdsa/target/release/pacta-verify-slhdsa.provenance.json" < `pub mod verify_mono;` + A visibility keyword. Rust's `src/bin/` and `examples/` targets are + SEPARATE crates, so neither can reach a `pub(crate)` item; the module has + to be public for any binary to call into it at all. + + 2. A new `verify_mono_bytes` function, appended. + It only assembles arguments: split the 32-byte public key into pk_seed and + pk_root, deserialize the 7856-byte signature, call `slh_verify_128s`. The + body is copied from the crate's OWN test helper `internal_inputs`, so the + conversion is the one the crate already trusts rather than one invented + here. Exposing the argument types and their fields instead would have + meant four more visibility changes across two files. + +WHAT THIS DOES NOT CHANGE. No existing line's semantics. The extraction root +`slh_verify_128s` is untouched -- same body, same callees. Module visibility and +an added sibling function do not alter the MIR of an existing function, so the +code the certificates cover compiles to what it compiled to before. What IS +true and must be said: the binary is built from `pinned commit + this patch`, +not from the pinned commit alone, and the diff below is the whole of the +difference. + +--- a/src/lib.rs ++++ b/src/lib.rs +@@ +-mod verify_mono; // Aeneas-compat monomorphic verify path (formal-verification campaign; additive) ++pub mod verify_mono; // Aeneas-compat monomorphic verify path (formal-verification campaign; additive) + +--- a/src/verify_mono.rs ++++ b/src/verify_mono.rs +@@ (appended after slh_verify_128s) ++/// Byte-level entry to the PROVEN root, for out-of-crate callers. ++/// ++/// Assembles arguments only. `mprime` is FIPS 205's M' and is built by the ++/// CALLER -- its construction is outside every certificate (TRUSTED-BASE item ++/// 10), which is exactly why it is a parameter here and not computed inside. ++pub fn verify_mono_bytes(mprime: &[u8], sig_bytes: &[u8; 7856], pk_bytes: &[u8; 32]) -> bool { ++ let mut pk_seed = [0u8; 16]; ++ let mut pk_root = [0u8; 16]; ++ pk_seed.copy_from_slice(&pk_bytes[0..16]); ++ pk_root.copy_from_slice(&pk_bytes[16..32]); ++ let pk = SlhPublicKey { pk_seed, pk_root }; ++ let sig = SlhDsaSig::<12, 7, 9, 14, 35, 16>::deserialize(sig_bytes); ++ slh_verify_128s(mprime, &sig, &pk) ++} diff --git a/dogfood/quorum/verify-slhdsa/src/main.rs b/dogfood/quorum/verify-slhdsa/src/main.rs new file mode 100644 index 0000000..f48b40d --- /dev/null +++ b/dogfood/quorum/verify-slhdsa/src/main.rs @@ -0,0 +1,101 @@ +//! warden quorum member: SLH-DSA-SHA2-128s, the Lean-proven verify path. +//! +//! Built against a copy of the PINNED proven source (`fips205-source` at the +//! commit named in the build provenance sidecar) plus `expose-mono.patch`, +//! which adds a visibility keyword and an argument-assembly function and +//! changes no existing line's semantics. +//! +//! The function this calls, `slh_verify_128s`, is the extraction root the +//! eleven certificates cover, apex `fips205.slh_verify_128s_accepts_iff`. +//! Verify-only on purpose: quorum members judge, they never sign. +//! +//! TWO THINGS THIS BINARY DOES THAT NO CERTIFICATE COVERS, stated here because +//! a reader of the output cannot see them: +//! +//! * It assembles M'. FIPS 205 hashes M' = toByte(0,1) ‖ toByte(|ctx|,1) ‖ +//! ctx ‖ M, and Algorithm 20's input is already M'. Everything above the +//! extraction root -- including that leading domain-separator byte, the one +//! thing distinguishing the pure variant from prehash -- is outside every +//! proof (TRUSTED-BASE item 10). This binary implements the PURE variant +//! with EMPTY context, i.e. M' = 0x00 ‖ 0x00 ‖ payload, and refuses to +//! guess at anything else. +//! * It parses hex and reads a file. +//! +//! Usage: +//! stdout OK / INVALID; exit 0 = accept, 1 = reject, 2 = input error. + +use std::process::ExitCode; + +const SIG_LEN: usize = 7856; +const PK_LEN: usize = 32; + +fn hex_decode(s: &str) -> Result, String> { + if s.len() % 2 != 0 { + return Err("odd-length hex".into()); + } + (0..s.len() / 2) + .map(|i| u8::from_str_radix(&s[2 * i..2 * i + 2], 16).map_err(|e| e.to_string())) + .collect() +} + +fn main() -> ExitCode { + let args: Vec = std::env::args().collect(); + if args.len() != 4 { + eprintln!("usage: {} ", args[0]); + return ExitCode::from(2); + } + + let pk_bytes = match hex_decode(&args[1]) { + Ok(b) if b.len() == PK_LEN => b, + Ok(b) => { + eprintln!("error: public key must be {PK_LEN} bytes, got {}", b.len()); + return ExitCode::from(2); + } + Err(e) => { + eprintln!("error: public key hex: {e}"); + return ExitCode::from(2); + } + }; + let sig_bytes = match hex_decode(&args[2]) { + Ok(b) if b.len() == SIG_LEN => b, + Ok(b) => { + // Size is part of the parameter set. A 7856-byte signature is + // SLH-DSA-SHA2-128s; anything else is a DIFFERENT parameter set and + // outside every certificate this binary exists to exercise. Refuse + // rather than attempt it. + eprintln!("error: signature must be {SIG_LEN} bytes (SLH-DSA-SHA2-128s), got {}", b.len()); + return ExitCode::from(2); + } + Err(e) => { + eprintln!("error: signature hex: {e}"); + return ExitCode::from(2); + } + }; + let payload = match std::fs::read(&args[3]) { + Ok(p) => p, + Err(e) => { + eprintln!("error: cannot read payload file {}: {e}", args[3]); + return ExitCode::from(2); + } + }; + + // M' for the PURE variant with empty context: two length/domain bytes then + // the message. Built here, not proven anywhere. + let mut mprime = Vec::with_capacity(payload.len() + 2); + mprime.push(0u8); // domain separator: 0 = pure, 1 = prehash + mprime.push(0u8); // |ctx| = 0 + mprime.extend_from_slice(&payload); + + let mut sig_arr = [0u8; SIG_LEN]; + sig_arr.copy_from_slice(&sig_bytes); + let mut pk_arr = [0u8; PK_LEN]; + pk_arr.copy_from_slice(&pk_bytes); + + if fips205::verify_mono::verify_mono_bytes(&mprime, &sig_arr, &pk_arr) { + println!("OK"); + ExitCode::from(0) + } else { + println!("INVALID"); + ExitCode::from(1) + } +}