pulsar: external-review package (audit/pulsar-v1) — honest status, KNOWN_BAD_V03, invariants, threat model, test matrix, repro, reviewer questions

2026-07-26 22:53:49 +00:00 · 2026-06-21 01:22:47 -07:00
parent 2532a32c11
commit bbbb9a97b1
7 changed files with 145 additions and 0 deletions
@@ -0,0 +1,24 @@
+# KNOWN BAD PATH — PULSAR-V13-HINT-LEAK (CRITICAL, contained)
+
+## The leak
+The v0.3/v0.4 `AlgebraicAggregate` path (`ref/go/pkg/pulsar/threshold_v03.go`)
+broadcast `CS2 = c·λ_i·s2_i` and `CT0 = c·λ_i·t0_i` **unmasked**, and the aggregator
+reconstructed `c·s2_joint = c·s2_master`, `c·t0_joint = c·t0_master`. With public `c`
+and `λ_i`, `s2_i = (c·λ_i)^{-1}·CS2`; and over varying public `c` the aggregate is a
+linear system in the fixed master `s2`/`t0`. Leaderless ⇒ every quorum member
+aggregates ⇒ every corrupt validator learns long-term secret-key material each round.
+The in-code `(t-1)`-secret claim was false (it only covered the `y_i`-masked `z_i`).
+
+## Why masking alone is insufficient (PULSAR-V13-W-LEAK)
+Forming the byte-equal signature requires reconstructing `c·s2_joint`. Even with
+masked individual shares, the aggregate is the master `c·s2`. And publishing full
+`w = A·y` is equally fatal: with the public `w' = A·z − c·t1·2^d`,
+`w' − w = c·t0 − c·s2`. So the protocol must never reconstruct `c·s2`/`c·t0`/`r0` and
+must never publish full `w` — only `w1 = HighBits(w)`.
+
+## Containment (landed)
+`Round2Sign` fails closed with `ErrUnsafeThresholdV03HintPath` unless an explicit
+test flag is set (`TestThresholdV03DisabledByDefault`). The replacement computes the
+hint publicly from `(w', w1)` via FIPS `UseHint` (`FindHint`), and the nonce
+boundary-clearance is certified by a validator quorum (NonceCert.ClearanceQC) without
+opening `w`.
@@ -0,0 +1,27 @@
+# Pulsar V1 — External Review Package
+
+Pulsar is a threshold protocol that emits **ordinary FIPS 204 ML-DSA signatures**.
+It does not propose a new verifier-facing signature format. Its security claim is
+threshold unforgeability, transcript privacy, and public consensus accountability
+under a validator-run nonce transcript and proof-carrying partial protocol.
+
+## Status (honest)
+
+- **Contained + math-verified + production-shaped.** NOT yet production/NIST-ready.
+- The legacy `AlgebraicAggregate` path leaked `c·s2`/`c·t0` (see `KNOWN_BAD_V03.md`)
+  and is **hard-disabled** (fails closed).
+- The replacement (boundary-cleared nonce transcripts + public hint recovery) has a
+  **verified arithmetic core** (boundary clearance, FindHint↔UseHint, yield ≈9.8%) and
+  a **production-shaped, fail-closed API** (NonceCert/Partial/ConsensusCert).
+- **Not yet sound / pending this review:** the NonceTranscript validator-MPC security,
+  the PartialProof soundness, the DKG well-formedness proof, independent-verifier
+  interop on the production path, and a machine-checked boundary-clearance proof.
+
+## Documents
+- `SPEC.md` / `../../spec/threshold-mldsa-boundary-clearance.tex` — construction.
+- `KNOWN_BAD_V03.md` — the contained leak (PULSAR-V13-HINT-LEAK + W-LEAK).
+- `SECURITY_INVARIANTS.md` — the invariants reviewers must check.
+- `THREAT_MODEL.md` — adversary, trust, leakage targets.
+- `TEST_MATRIX.md` — what each test proves.
+- `REPRO.md` — exact commands.
+- `REVIEW_QUESTIONS.md` — the questions for reviewers.
@@ -0,0 +1,11 @@
+# Reproduce
+
+```
+cd ~/work/lux/luxfi/pulsar
+go build ./ref/go/pkg/pulsar/
+go test  ./ref/go/pkg/pulsar/ -run 'ThresholdV03|NoHintSecret|NonceCert|NonceTranscript|FindHint|Boundary|BCCParam|Partial|CanonicalNonce|AbortClasses|TreeAggregate|MergeAggregates|NoT0|ProductionBCC|PublishingFullW' -count=1
+go vet  ./ref/go/pkg/pulsar/
+```
+
+Spec: `spec/threshold-mldsa-boundary-clearance.tex` (latexmk -pdf).
+Blockers: `BLOCKERS.md` (PULSAR-V13-HINT-LEAK / W-LEAK / PARTIAL-Z-PROOF + criteria).
@@ -0,0 +1,16 @@
+# Reviewer Questions
+
+1. Does any production transcript reveal `w`, `LowBits(w)`, `c·s2`, `c·t0`, `r0`, or
+   residual equivalents?
+2. Is the NonceTranscript validator-MPC malicious-secure at the stated `t−1` threshold,
+   and does it output only `W1 + clear bit + transcript root`?
+3. Is `W1 = HighBits(w)` computed correctly without revealing `w`?
+4. Does `BoundaryClear(w, 2β + slack)` imply the hidden `r0` bound for all valid `c,s2`?
+   (ML-DSA-65/87 only; confirm `‖c·t0‖ < γ2`.)
+5. Is `FindHint` exactly equivalent to the FIPS 204 `UseHint` verifier relation?
+6. Does `PartialProof` soundly prove `z_i = λ_i·y_i + c·λ_i·s1_i` without leaking
+   `y_i`/`s1_i`/`s2_i`/`t0_i`?
+7. Is canonical nonce selection non-grindable after the block/message is observed?
+8. Are rejected attempts simulatable (no secret-dependent failure predicate)?
+9. Does tree aggregation preserve signer accountability and reject malformed partials?
+10. Do ≥2 independent FIPS 204 ML-DSA verifiers accept all produced signatures?
@@ -0,0 +1,27 @@
+# Security Invariants (reviewers verify each)
+
+1. **No secret residual.** No production wire type, transcript, or log carries
+   `c·s2`, `c·t0`, `r0`, `LowBits(w − c·s2)`, hint shares, or `CS2/CT0/D2/D0`.
+   Enforced: `TestNoHintSecretFieldsInProductionWireTypes`.
+2. **No full w.** `NonceCert` carries `W1 = HighBits(w)` only — never `w`, `w_i`,
+   `LowBits(w)`, or boundary distances. Enforced: `TestNonceCertHasNoFullW`,
+   `TestNonceTranscriptDoesNotRevealW`, `TestPublishingFullWWouldRevealResidual`.
+3. **Public hint.** `FindHint(w', w1)` ≡ FIPS `UseHint`; never `MakeHint(secret)`.
+   Enforced: `TestFindHintToTargetMatchesUseHint`.
+4. **Boundary ⇒ r0 safe.** `BoundaryClear(w, 2β)` ⇒ HighBits stable under `c·s2`
+   and hidden `r0 < γ2 − β`. Enforced: `TestBoundaryClearImpliesHighBitsStable`,
+   `TestBoundaryClearEdgeCases`. **Parameter scope: ML-DSA-65/87 only**
+   (`TestBCCParamGuard`; ML-DSA-44 violates `‖c·t0‖ < γ2`).
+5. **Quorum-bound nonce cert.** `ClearanceQC` binds every cert field; tamper ⇒ reject.
+   Enforced: `TestNonceCertBindsAllConsensusFields`, `TestBadNonceTranscriptRootRejected`.
+6. **Canonical nonce.** Deterministic, non-grindable per session. `TestCanonicalNonce`.
+7. **Coarse aborts.** Rejected attempts publish only a coarse class. `TestAbortClassesCoarse`.
+8. **Accountable aggregation.** Tree==flat; duplicate/cross-session rejected; bitmap
+   accountability. `TestTreeAggregateEqualsFlat`, `TestMergeAggregatesDuplicateAndSession`.
+
+## OPEN (this review's subject — NOT yet sound)
+- NonceTranscript validator-MPC malicious security (currently debug-oracle + fail-closed).
+- PartialProof soundness (currently binding + fail-closed).
+- DKG well-formedness proof (currently type-clean + reflection-tested).
+- Independent-verifier interop on the production sign path.
+- Machine-checked boundary-clearance / FindHint proof.
@@ -0,0 +1,25 @@
+# Test Matrix (what each test proves)
+
+| Test | Proves |
+|---|---|
+| TestThresholdV03DisabledByDefault | leaking legacy path fails closed |
+| TestNoHintSecretFieldsInProductionWireTypes | no CS2/CT0/D2/D0/R0/LowBits/Hint fields in prod wire |
+| TestNonceCertHasNoFullW | NonceCert has W1, not full W |
+| TestNonceTranscriptDoesNotRevealW | transcript public view has no w / LowBits(w) |
+| TestNonceTranscriptOutputsCorrectW1_DebugOracle | W1 = HighBits(w) |
+| TestNonceTranscriptBoundaryClear_DebugOracle | clear flag = BoundaryClear(w); non-clear unvotable |
+| TestNonceCertBindsAllConsensusFields | QC binds every cert field (tamper-evident) |
+| TestBadNonceTranscriptRootRejected | tampered transcript root rejected |
+| TestPublishingFullWWouldRevealResidual_DebugOracle | w' − w = residual (why w is forbidden) |
+| TestFindHintToTargetMatchesUseHint | FindHint ≡ FIPS UseHint round-trip |
+| TestBoundaryClearImpliesHighBitsStable | boundary ⇒ HighBits stable + r0 bound |
+| TestBoundaryClearEdgeCases | exact off-by-one at γ2 − 2β |
+| TestBoundaryClearanceYield | offline yield ≈ 9.8% (ML-DSA-65) |
+| TestBCCParamGuard | ML-DSA-65/87 only; 44 rejected |
+| TestValidPartial/TestBadZShareRejected/binding | partial binding + fail-closed |
+| TestCanonicalNonceSelection | deterministic non-grindable |
+| TestAbortClassesCoarse | coarse aborts only |
+| TestTreeAggregateEqualsFlat (to 1000) | tree == flat |
+| TestMergeAggregatesDuplicateAndSession | duplicate/cross-session rejected |
+| TestNoT0InProductionDKGTypes | DKG public types carry no t0/master |
+| TestProductionBCCSigningDisabledUntilSoundZK | prod signing fails closed sans sound proofs |
@@ -0,0 +1,15 @@
+# Threat Model
+
+- **Setting:** public, permissionless, leaderless BFT consensus. Any validator may
+  aggregate; there is no trusted combiner.
+- **Adversary:** static corruption of up to `t−1` of the active committee, including
+  the coordinator/aggregator role. Sees all broadcasts and the public chain.
+- **Goal of the adversary:** recover long-term key material (`s1,s2,t0`), forge, or
+  grind the nonce/challenge.
+- **Trust:** the validator set (quorum) is the MPC party set for DKG and the
+  NonceTranscript. A dishonest quorum is already a consensus-Byzantine break.
+- **Leakage targets (must be hidden from a `t−1` coalition AND the public chain):**
+  `w`, `LowBits(w)`, `c·s2`, `c·t0`, `r0`, `LowBits(w + c·t0 − c·s2)`, `y_i`, `s1_i`,
+  `s2_i`, `t0_i`.
+- **Public (allowed):** `w1 = HighBits(w)`, commitments, QCs, `z`, the final ML-DSA
+  signature `(c,z,h)`, signer bitmap, transcript roots.