Commit graph

4 commits

Author SHA1 Message Date
16040b79f5 quorum: pacta-verify-slhdsa — the SLH-DSA head-checker built from the proven source
Fifth quorum member, first post-quantum one: verifies an SLH-DSA-SHA2-128s
signature by calling slh_verify_128s, the extraction root the eleven fips205
certificates cover (apex fips205.slh_verify_128s_accepts_iff). Verify-only
like the other four: quorum members judge, they never sign.

Build discipline, because "built from the proven source" is a claim that has
to survive a hostile reader: build-verify-slhdsa.sh REFUSES to build if the
pinned checkout is dirty or at any commit other than a3ce8e8, exports the
pinned commit via git archive (never a working copy), applies
expose-mono.patch to that scratch copy, and then DIFFS the patched
verify_mono.rs against the pinned one, aborting if any existing line changed
rather than being appended. The patch is a visibility keyword plus its doc
comment (the crate denies missing_docs, so pub mod alone does not compile)
and one appended argument-assembly function whose body is the crate's own
test helper. The extraction root is provably untouched. A provenance sidecar
lands beside the binary: source commit, patch hash, main.rs hash, rustc, and
a not_covered field naming what no certificate reaches — M-prime assembly
(including the pure/prehash domain-separator byte), hex/file IO, the
compiler; signing and keygen out of scope entirely.

Demonstrated against OpenSSL 3.5.5 on a throwaway key: valid signature OK
both ways, wrong message INVALID, corrupted signature INVALID. The agreement
is itself a finding — this binary assembles M' = 0x00 || 0x00 || payload
(pure variant, empty context) and OpenSSL evidently does the same.

Convention matches the other members: template + main.rs + patch + build
script tracked; rendered Cargo.toml, lock, target/ and the .build-slhdsa
scratch tree ignored.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-06 21:52:56 +02:00
bbc99a9127 warden quorum boundary: 4 provably-equivalent verifier members, live
- dogfood/quorum/verify-{dalek,anza,risc0,betrusted}: verify-only crates
  built from the pinned proven source workspaces (serial backends pinned
  per fork; anza entry is the certificate-covered verify_sha512, not the
  default Zebra-lineage verify())
- src/pacta/quorum.py: unanimity-required acceptance, divergence
  taxonomy (semantic-edge vs unexplained/tamper), small-order/canonicity
  edge flags, per-member provenance sidecars with binary hashes
- live smoke: 4/4 members agree on accept and reject

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 23:26:21 +02:00
b8ffbafa7f The provider eats its own dogfood: root signatures via the merkleized library
The dogfood principle now runs in BOTH directions. Agents already
verified signatures through the proven dalek path; now the provider
SIGNS with it too, and proves to itself that the signing code is in its
own log before every signature:

- dogfood binary gains a `sign` mode (seed over stdin, never argv;
  ed25519_dalek::SigningKey from the same pinned merkleized workspace).
  Honesty ledger unchanged: the library's VERIFY path is
  certificate-covered; its signing path is declared trusted base - but
  it is the ATTESTED artifact, not an un-attested third implementation.
- sign_payload_ed25519_detailed: signing dispatch mirroring the verify
  dispatch; the backend that actually signed is recorded in every
  attestation signature block and STH.
- THE SELF-REFERENTIAL CHECK: before signing any tree head, the
  provider runs the SAME Merkle inclusion verification an agent runs -
  against the very tree it is about to sign - for the newest leaf
  attesting the signing library itself, and embeds the result in the
  signature block:
    signing_provenance:
      signing_backend: verified-dalek-serial
      signing_library_component: dalek-ed25519-verified
      signing_library_source_commit: aa0f6ab...
      self_inclusion: verified
      signing_library_leaf_index: 4
      signing_library_certificates_proven: 16/16
  A root signature that names the leaf vouching for the code that
  produced it. First-append chicken-and-egg is handled honestly
  (self_inclusion: library_not_in_log).
- Evidence refreshed: all four receipts re-issued under dogfood-signed
  STHs; the full agent verify loop re-run green.

50/50 tests (new signing roundtrip test, skip-safe where unbuilt).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 15:21:17 +02:00
d331ba17d9 Dogfood cryptography: pacta verifies signatures through the PROVEN code path
"Eat your own dogfood": pacta consumes certificates about a verified
Ed25519 implementation while checking those certificates' signatures
with OpenSSL. Now it can use the object of its own evidence:

- dogfood/pacta-verified-verify: a ~90-line Rust binary built against
  the PINNED proven source workspace (saymrwulf/curve25519-dalek-source
  at the exact commit the dalek certificates pin - the build records it:
  aa0f6ab...) with the serial backend pinned via RUSTFLAGS exactly as
  the verified extraction pins it. Cargo.toml is committed as a template
  ({{SOURCE}} placeholder) so no machine path is hardcoded; the rendered
  file, target/, and the built binary are gitignored.
- pacta dogfood-build --source <workspace>: renders, builds, installs
  to dogfood/state/, and writes a provenance sidecar (source commit,
  backend cfg, rustc, and an honest coverage note: the certificates
  cover verify_sha512, the extraction-refactored image of this verify
  path; SHA-512 and the wire glue remain the theorems' documented
  boundary). pacta dogfood-status reports the active backend.
- signing.verify_payload_ed25519_detailed: dispatch - the dogfood
  binary when present (backend "verified-dalek-serial"), OpenSSL
  fallback otherwise, and the backend that ACTUALLY ran is recorded in
  receipt signature statuses and attestation evidence. Fallback is
  never silent.
- --require-verified-verifier (receipt-verify + agent): policy fails
  closed when verification did not run on the certificate-covered
  path.
- ML-DSA is deliberately unchanged: no proven implementation exists,
  so the slot stays fail-closed "unavailable" - the honest hybrid-PQC
  posture is one proven-classical signature plus one required-but-
  unproven PQC slot, never a pretend backend.

Validated live: receipt verification through the proven verifier
(backend recorded), a corrupted signature bit rejected BY the proven
binary, tampered attestations rejected, and the policy failing closed
when the binary is absent. 49/49 tests green (incl. PEM-SPKI raw-key
cross-check against openssl, dispatch/backend recording with a stub,
and a real-binary roundtrip that skips gracefully where unbuilt).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 10:13:48 +02:00