Files
magnetar/TRUSTED-COMPUTING-BASE.md
T
Antje Worring df4c537c16 magnetar: remove proof-by-rename + circular proofs; honest threshold status
True no-reconstruction threshold SLH-DSA is impossible in the no-dealer /
no-preprocessing model a public, leaderless, permissionless chain needs
(Kondi-Kumar-Vanegas: extractable hash-based signatures cannot be thresholded
by black-box hash use). Stop pretending otherwise.

De-cheat:
  - DELETE the circular/vacuous proofs that manufactured false assurance:
    Magnetar_N1_Atom_Refinement.ec, Magnetar_N1_SHAKE_Expand.ec,
    Magnetar_N4_KeyDeriveStable.ec, lemmas/{Magnetar_CT,SLHDSA_Functional}.ec.
    The headline "strict-atom byte-equality" theorem was `apply <axiom that
    restates the theorem>`; the Lean side was `sorry`/`:= True`.
  - Re-open MAGNETAR-STRICT-ATOM (BLOCKERS): the public combiner DOES
    reconstruct the full FIPS 205 master every signature; the v1.1 "closure"
    only renamed identifiers. PROOF-CLAIMS / AXIOM-INVENTORY / TCB docs now say
    what the code does.
  - Re-label the name-grep "strict-atom" / "CT" checks as identifier-hygiene
    lint, NOT security or constant-time properties.
  - PVSS-DKG open-reveal (publishes the master to any observer) is gated as a
    TEST-ONLY path with HONEST LIMITATIONS; production does not rely on it.
  - Remove dead htRootCompute; staticcheck clean.

Honest three-leg posture (SPEC 1.0, BLOCKERS):
  - Permissionless production = INDEPENDENT FIPS 205 sigs + the weighted quorum
    certificate (luxfi/consensus), optionally STARK/FRI-compressed (luxfi/p3q).
    No key sharing, no reconstruction.
  - Trusted-hardware custody = TEE-attested combiner (trust-relocation, NOT MPC).
  - THBS-SE = RESEARCH-ONLY (transient seed reconstruction at the combiner);
    the T-SLH-DSA-MPC track (MPC over SHAKE) is the other research escape hatch.

Tests green (CGO=1, 71s). Net -923 lines.
2026-06-21 13:06:57 -07:00

17 KiB

TRUSTED-COMPUTING-BASE --- Magnetar implementation TCB

v1.0 framing. This document is a v0.x archival snapshot. The v1.0 TCB for the per-validator standalone primitive is cloudflare/circl/sign/slhdsa v1.6.3. The v1.0 TCB for THBS-SE additionally includes the public combiner's transient memory at the precise sub-second sign moment (see DEPLOYMENT-RUNBOOK.md sec 2.1).

What you must trust to rely on Magnetar's byte-equality correctness claim. Companion to PROOF-CLAIMS.md (proof scope) and DEPLOYMENT-RUNBOOK.md (operator-facing trust-model disclosure).

HONESTY NOTE: Magnetar's TCB is structurally simpler than Pulsar's because Magnetar ships NO mechanized refinement layer for the threshold overlay (no EasyCrypt theories specific to the overlay, no Lean ↔ EC bridges specific to the overlay, no Jasmin sources for the overlay). The FIPS 205 SLH-DSA single-party layer DOES have upstream formal artifacts available (libjade's SLH-DSA work) but Magnetar does not redistribute or re-verify them in this submission. That removes the overlay-specific proof-tool TCB but increases the trust placed in (i) the Go reference implementation review of the threshold overlay, (ii) KAT determinism, and (iii) the byte-equality test harness against the cloudflare/circl FIPS 205 verifier. See PROOF-CLAIMS.md for the honest framing.

§0 Layered trust bases

The Magnetar byte-equality claim rests on three layered trust bases:

  1. The FIPS 205 SLH-DSA standard — NIST FIPS 205 (2024). The single-party signing primitive's security analysis is NIST's; the Magnetar submission inherits it.
  2. The Go reference implementationref/go/pkg/magnetar/ (~2200 LOC) plus cloudflare/circl/sign/slhdsa (the FIPS 205 single-party reference). Reviewed by code inspection + KAT replay
    • the TestN1_ByteEquality_* empirical byte-equality harness.
  3. The trusted-computing base (TCB) below the implementation — this document.

If any element of the TCB is unsound, the implementation's correctness is unsound regardless of how clean the code review was.

§1 Implementation TCBs

§1.1 Reference implementation (Go)

Component Trust Mitigations
Magnetar Go reference (this repository) Go standard-library correctness, crypto/rand randomness quality, transcript-hash primitives in transcript.go (cSHAKE256 / KMAC256), byte-wise Shamir / Lagrange in thbsse_field.go, THBS-SE protocol in thbsse.go, Combine emit in thbsse_assemble.go + the FIPS 205 walk in slhdsa_internal.go, per-validator standalone in standalone.go, dealerless DKG in pvss_dkg.go Reviewed by code inspection; KAT replay (vectors/*.json regenerated byte-stably); byte-identity tests vs single-party FIPS 205. (The v0.x files shamir.go, dkg.go, threshold.go, combine.go were DELETED.)
github.com/cloudflare/circl/sign/slhdsa Cloudflare's audited Go reference implementation of FIPS 205 SLH-DSA. Used for: scheme-seed derivation (Scheme.DeriveKey), SignDeterministic, Verify. Version pinned in go.mod. circl is the canonical mainstream Go FIPS 205 implementation; community-audited at Cloudflare scale.
golang.org/x/crypto/sha3 cSHAKE256, KMAC256, TupleHash256 primitives (Go-stdlib-style). Version pinned in go.mod.
crypto/subtle Constant-time byte-blob compare. Standard library. (Note: Magnetar uses local ctEqualSlice / ctEqual32 constant-time helpers in transcript.go rather than crypto/subtle.ConstantTimeCompare for direct legibility; the algorithm is identical: scan every byte with `diff = a[i] ^ b[i], return diff == 0`.)

§1.2 Production targets (out of scope for v0.3.0)

Target Status
Optimized Rust crate TODO — not in this submission
C library + FFI TODO — not in this submission
WASM build TODO
no_std embedded TODO
C++ port TODO — a future cross-runtime byte-equality harness (matching Pulsar's luxcpp/crypto/pulsar/ and Corona's luxcpp/crypto/corona/) is a possible Tier A → Tier A++ evidence enhancement

For each future target, an independent constant-time audit + KAT cross-validation + binding-level fuzzing is required before considering it "production." The byte-equality claim does NOT automatically transfer to these targets — each target's correctness must be re-verified.

§2 Build TCBs

Layer What you trust Reproducibility
Go toolchain The Go compiler used to build the reference. The go.mod directive pins the language version. Hard-pinned in go.mod; go.sum enforces module checksums.
scripts/cut-submission.sh The cut orchestrator's correctness — that it produces deterministic outputs from a fresh checkout. Mirrors Pulsar's pattern; runs build → tests → KAT-regen verification → tar.
scripts/check-high-assurance.sh The high-assurance gate's correctness — go build + go vet + secret-log smoke scan. Skips proof-tool checks since Magnetar ships none for the overlay layer. Honest about what's checked and what's not; documented in the script header.
ref/go/cmd/genkat Deterministic regeneration of KAT vectors. The genkat tool consumes fixed seeds and produces byte-stable JSON output; re-running on a clean checkout produces byte-identical files.

§3 What the TCB does NOT include

Magnetar's TCB is structurally simpler than Pulsar's because Magnetar ships no mechanized refinement layer for the threshold overlay. The following are NOT in the Magnetar TCB:

  • EasyCrypt prover (Pulsar trusts it; Magnetar has no EC theories for the overlay layer)
  • Lean 4 + Mathlib (Pulsar uses Lean-bridged algebraic axioms for Shamir / Lagrange identities; Magnetar has none of its own — closure plan is cross-citation to Pulsar's bridges, since the underlying GF(257) algebra is identical)
  • Jasmin verified compiler (Pulsar's threshold layer is in Jasmin; Magnetar's is pure Go)
  • OCaml runtime (EC is OCaml; Magnetar has no EC)
  • jasmin-ct (Magnetar's CT evidence is local-helper ctEqualSlice / ctEqual32 review + the cloudflare/circl upstream constant-time claims for the FIPS 205 single-party layer; statistical CT measurement is roadmap)

What IS in the Magnetar TCB but NOT in Pulsar's:

  • Greater dependence on the Go reference review of the threshold overlay. Pulsar can fall back to the EC refinement chain if a Go reviewer misses a bug in the threshold layer; Magnetar's only line of defense for the overlay is reviewer + KAT determinism + the TestN1_ByteEquality_* harness against single-party FIPS 205.
  • Greater dependence on cloudflare/circl's FIPS 205 implementation. Pulsar's spec target (FIPS 204) is implemented both by cloudflare/circl AND independently by BoringSSL FIPS / AWS-LC / OpenSSL 3.0 (interop targets exist). Magnetar's spec target (FIPS 205) is at a less mature interop point — circl is the canonical Go implementation, but the mainstream third-party FIPS 205 implementations (BoringSSL, OpenSSL) are still landing at submission time.

§4 What the TCB does NOT cover

These are explicitly NOT part of the trust base for Magnetar's byte-equality correctness claim:

  • Specific operating system (Linux, macOS, BSD, Windows) — the Go reference is OS-independent.
  • Specific CPU architecture — Go compiles to amd64/arm64; both exercised in development.
  • Network protocol stack — Magnetar's transport is out of scope.
  • Storage layer — how KeyShare material is stored at rest is out of scope. Production deployments use HSM-backed share material or TEE-attested host configurations; see DEPLOYMENT-RUNBOOK.md.
  • Key management policies — key lifecycle is application-level (governed by the consuming consensus layer, e.g. Quasar Polaris profile).
  • Application code calling Magnetar — Magnetar's API contract is the trust boundary.

§5 TCB risks and mitigations

§5.1 Construction-soundness risk

Risk Mitigation
FIPS 205 SLH-DSA has a latent cryptanalytic flaw NIST FIPS 205 (2024) is the published standard with extensive cryptanalytic review. Lux tracks cryptanalysis literature; any flaw would prompt NIST guidance, which Magnetar would inherit. The fundamental hardness assumption (collision/preimage resistance of SHAKE) is conservative.
The Magnetar threshold lifecycle additions (byte-wise Shamir VSS, DKG, two-round commit-bind sign) have a latent bug Per-protocol tests in ref/go/pkg/magnetar/dkg_test.go, threshold_test.go, kat_test.go, n1_byte_equality_test.go. Independent third-party audit is roadmap item, see BLOCKERS.md BLK-9. The byte-equality property to single-party FIPS 205 is the load-bearing N1 invariant; any threshold-layer bug that broke it would manifest in TestN1_ByteEquality_* failure.

§5.2 Implementation-correctness risk

Risk Mitigation
Go reference implementation diverges from the construction TestN1_ByteEquality_* runs end-to-end DKG → threshold-sign → Combine and asserts byte-equality with slhdsa.SignDeterministic(KeyFromSeed(reconstructed_seed), msg, ctx). Divergence = test failure.
KAT vectors are subtly wrong Deterministic generation from fixed seeds via ref/go/cmd/genkat. The KAT replay test (kat_test.go) validates that the package implementation reproduces every KAT entry verbatim.
cloudflare/circl/sign/slhdsa has a bug in FIPS 205 implementation circl is the canonical mainstream Go FIPS 205 implementation; community-audited at Cloudflare scale. A circl bug would also affect any other Go consumer of FIPS 205. Closure: cross-implementation verifier harness against a non-Go FIPS 205 implementation (e.g., pq-crystals reference C, BoringSSL when SLH-DSA lands) is roadmap, see BLOCKERS.md BLK-6.
Hash-suite implementation bug (cSHAKE256 / KMAC256) golang.org/x/crypto/sha3 is a widely-used standard library implementation; bugs are rare and quickly patched. The Magnetar Shamir / Lagrange / mix operations route every call through transcript.go so any drift is a single-file change.

§5.3 Build / reproducibility risk

Risk Mitigation
scripts/cut-submission.sh produces non-deterministic output The build is deterministic from fixed seeds; reproducible-build property is checked at every cut. The KAT regen step explicitly compares regenerated vectors against committed copies.
Toolchain version drift between commits go.mod pin + go.sum enforcement.
KAT drift across runs ref/go/cmd/genkat consumes only fixed seeds and committed config; output is byte-stable. The cut script diffs regenerated KATs against committed copies and fails on any divergence.

§5.4 Side-channel risk

Risk Mitigation
Timing leakage on secret-dependent paths in the threshold overlay Constant-time helpers (ctEqualSlice, ctEqual32) are used for every commit verification and public-key equality check. Secret-dependent branches absent from verify.go, sign.go, and the Combine commit-verify gate. Statistical validation via dudect is NOT yet in place — roadmap item, see PROOF-CLAIMS.md §3.4.
Timing leakage in the single-party FIPS 205 layer cloudflare/circl/sign/slhdsa documents constant-time properties per FIPS 205 §6.3 guidance; libjade has SLH-DSA formal CT artifacts for the broader ecosystem. Magnetar does not redistribute these but inherits the upstream guarantees.
Memory-access / cache-timing leakage Not addressed at the software level. Production deployments should use TEE attestation (SGX, SEV-SNP, TDX) per DEPLOYMENT-RUNBOOK.md §1 ("v0.1 reveal-and-aggregate trust caveat").
Secret-buffer lifetime / coredump risk The THBS-SE Combine path (thbsse_assemble.go) zeroizes the reconstructed-master buffers (derivedExpandInput, derivedMaterial) and the PRF scratch (prfAbsorb, prfMsgAbsorb) after use. This is defense-in-depth: the full FIPS 205 master IS resident in the public combiner's memory during one Sign call (the permissionless THBS-SE path is research-grade, not no-leak — see ASSEMBLE-INVARIANT.md and BLOCKERS.md). For no-resident-seed deployments use the per-validator standalone path or the TEE pool.

§6 Independent verification protocol

To independently verify Magnetar's claims, a reviewer should:

  1. Clone the repo at the submission tag.
  2. GOWORK=off go build ./... — expect clean build.
  3. GOWORK=off go test -count=1 -short -timeout 240s ./ref/go/pkg/magnetar/ — expect all tests passing, including TestN1_ByteEquality_* across (3,2), (5,3), (7,4).
  4. Backup vectors/, run GOWORK=off go run ./ref/go/cmd/genkat -out=vectors/, then diff -qr vectors_backup/ vectors/ — expect zero differences (KAT determinism).
  5. Read the Go reference implementation:
    • params.go, types.go — public types + FIPS 205 parameter sets
    • keygen.go, sign.go, verify.go — single-party FIPS 205 dispatch
    • standalone.go — per-validator standalone (PRIMARY production path)
    • thbsse_field.go — byte-wise Shamir over GF(257)
    • transcript.go — cSHAKE256 / KMAC256 / SP 800-185 helpers
    • pvss_dkg.go — dealerless DKG (RunDKG production + open-reveal test)
    • thbsse.go, thbsse_assemble.go, slhdsa_internal.go — THBS-SE threshold sign + the master-reconstructing Combine emit (research-grade; see ASSEMBLE-INVARIANT.md)
    • zeroize.go — secret-buffer wipes (The v0.x files shamir.go, dkg.go, threshold.go, combine.go were DELETED; ignore any doc that still references them.)
  6. Cross-reference with FIPS 205 (NIST 2024) §10.1 (parameter sets), §10.2 (Sign), §10.3 (Verify).
  7. Cross-reference with SPEC.md §3 (DKG), §4 (threshold sign), §6 (byte-equality claim), §7 (trust model).

If all 7 steps pass, the trust base reduces to the TCB enumerated in this document.

§7 What this means for downstream consumers

For a downstream consumer (e.g., a Quasar consensus chain incorporating Magnetar as the hash-based PQ leg of the Polaris profile):

  • The byte-equality claim is conditional on the TCB. If you change the Go toolchain, port to a different runtime, or modify the hash suite, the claim's transferable guarantees attenuate.
  • For FIPS 140-3 module validation, Magnetar's path is via the FIPS 205 SLH-DSA standard (NIST). The single-party FIPS 205 layer in cloudflare/circl is independently validatable when FIPS 205 modules ship; the threshold overlay is not subject to FIPS 140-3 directly (there is no NIST standard for threshold SLH-DSA).
  • For NIST MPTC review, Magnetar's role is the algorithm-level reference + production lifecycle artifacts; module packaging + external audit are downstream.
  • For threshold signing in a Quasar Polaris deployment, Magnetar is the hash-based PQ kernel; the consuming consensus layer is responsible for the chain-of-custody and validator-rotation orchestration. The Magnetar reshare protocol (v0.4 roadmap) will provide the Class N4-analog primitive when it lands.

§8 Honest comparison to Pulsar's and Corona's TCBs

TCB element Pulsar Magnetar Corona
EasyCrypt prover YES (foundation of refinement proof, 13 files, 0/0 admits) NO (no EC theories for the overlay layer) NO
Lean 4 + Mathlib YES (5 Lean-bridged axioms) NO (cross-citation closure on roadmap; Shamir/Lagrange algebraically identical to Pulsar's GF(257)) NO
Jasmin verified compiler YES (threshold layer in Jasmin) NO (pure Go; libjade covers SLH-DSA single-party but is not redistributed here) NO (pure Go)
OCaml runtime YES (EC is OCaml) NO NO
Go toolchain YES (Go reference) YES (Go reference; primary) YES (Go reference)
cloudflare/circl FIPS 205 NO (Pulsar uses FIPS 204) YES (FIPS 205 single-party kernel) NO (R-LWE; no FIPS standard)
luxfi/lattice/v7 (lattigo fork) NO NO YES (R-LWE primitives)
crypto/subtle (or local CT helpers) YES YES (local ctEqualSlice / ctEqual32) YES
golang.org/x/crypto/sha3 YES YES YES
NIST standard target FIPS 204 ML-DSA FIPS 205 SLH-DSA none (Boschini ePrint 2024/1113)
Third-party FIPS-validated verifier available YES (BoringSSL FIPS / AWS-LC / OpenSSL 3.0 ML-DSA) PARTIAL (FIPS 205 still landing in third-party stacks at submission time) NO (none exists for R-LWE threshold)

Net effect: Magnetar's TCB is smaller than Pulsar's (fewer proof-tool dependencies) but the trust per-component is higher (no fall-back to a mechanized refinement chain if a Go reviewer misses a bug in the threshold overlay). Compared to Corona, Magnetar has a STRONGER baseline because the single-party layer is FIPS-anchored (FIPS 205) while Corona's underlying construction is a 2024 academic paper with less cryptanalytic surface area.


Document metadata

  • Name: TRUSTED-COMPUTING-BASE.md
  • Version: v0.1 (initial Tier A submission-package scaffolding)
  • Date: 2026-05-18
  • Go toolchain pin: see go.mod
  • cloudflare/circl pin: see go.mod
  • golang.org/x/crypto pin: see go.mod