From 26212bf9aef07a9ab4ebac100380a4277ec74deb Mon Sep 17 00:00:00 2001 From: Antje Worring Date: Sun, 21 Jun 2026 00:54:00 -0700 Subject: [PATCH] PULSAR-V13: contain hint-path leak + land verified BCC/CEF math core - hard-gate threshold_v03 AlgebraicAggregate (fail-closed, PULSAR-V13-HINT-LEAK) - threshold_bcc.go: BoundaryClear + findHintToTarget (FIPS UseHint) + ML-DSA-65/87 param guard; no production code forms c*s2/c*t0/r0/LowBits - 6 verified tests green (gate, param guard, FindHintToTarget<->UseHint round-trip, BoundaryClear=>HighBits-stable+r0-bound, off-by-one edges, yield 9.8%) - spec/threshold-mldsa-boundary-clearance.tex (BCC0/BCC+, full-w-hidden, ZK req) - BLOCKERS: V13-HINT-LEAK + V13-W-LEAK + V13-PARTIAL-Z-PROOF + resolution criteria --- BLOCKERS.md | 80 ++++++- ref/go/pkg/pulsar/threshold_bcc.go | 167 +++++++++++++ ref/go/pkg/pulsar/threshold_bcc_test.go | 186 +++++++++++++++ ref/go/pkg/pulsar/threshold_v03.go | 32 ++- spec/threshold-mldsa-boundary-clearance.tex | 250 ++++++++++++++++++++ 5 files changed, 706 insertions(+), 9 deletions(-) create mode 100644 ref/go/pkg/pulsar/threshold_bcc.go create mode 100644 ref/go/pkg/pulsar/threshold_bcc_test.go create mode 100644 spec/threshold-mldsa-boundary-clearance.tex diff --git a/BLOCKERS.md b/BLOCKERS.md index f631231..ed53a45 100644 --- a/BLOCKERS.md +++ b/BLOCKERS.md @@ -22,7 +22,85 @@ and the v1.0.7 sign-off. ## Open -None. +### PULSAR-V13-HINT-LEAK (CRITICAL) + +The v0.3/v0.4 `AlgebraicAggregate*` path broadcasts `CS2 = c·λ_i·s_{2,i}` +and `CT0 = c·λ_i·t_{0,i}` **unmasked** (`ref/go/pkg/pulsar/threshold_v03.go` +round2EmitFull, ~:930-963) and reconstructs `c·s2_joint`, `c·t0_joint` at +the aggregator (~:1131-1168). Both are secret-key-derived: `c`, `λ_i` +public ⇒ `s_{2,i} = (c·λ_i)^{-1}·CS2` (one session when `c` invertible; +else accumulate). Worse, `c·s2_joint = c·s2_master` (Shamir), so revealing +the **aggregate** over varying public `c` leaks the long-term secret-key +components `s2` (and likewise `t0`) via a linear system, plus the secret +relation `A·s1 = (t1·2^d + t0) − s2`; whether or not this immediately +recovers short `s1` (a lattice/preimage problem), threshold secrecy and +transcript simulation are already broken. Leaderless ⇒ every +quorum member aggregates ⇒ every corrupt validator learns it each round. +The in-code `PUBLIC-BFT-SAFETY NOTE` claiming `(z_i,cs2_i,ct0_i)` are +`(t−1)`-secret is **false** — it only covers the `y_i`-masked `z_i`. + +Confirmed by adversarial audit (`AUDIT-2026-06.md` re-audit) + direct code +read. Masking the individual shares is necessary but **not** sufficient — +the aggregate reconstruction still leaks the master key. The fix must +never reconstruct `c·s2`/`c·t0`/`r0`. + +**Containment (landed, branch `fix/threshold-mldsa-hint-leak`):** +`Round2Sign` now **fails closed** with `ErrUnsafeThresholdV03HintPath` +unless `AllowUnsafeThresholdV03ForTests` is set (test +`TestThresholdV03DisabledByDefault`). The dangerously-false `(t−1)`-secret +note is corrected. + +**Replacement design + verified math core:** boundary-cleared nonces + +carry elimination (`spec/threshold-mldsa-boundary-clearance.tex`, +`threshold_bcc.go`). The hint is computed from the **public** +`w' = A·z − c·t1·2^d` and `w1 = HighBits(w)` strictly via FIPS `UseHint` +(`findHintToTarget`); boundary clearance (margin `2β`) keeps the small +`c·s2` shift off the boundary; `c·t0` is structurally +`‖c·t0‖∞ ≤ τ·2^{d-1} < γ2` for **ML-DSA-65/87 only** (param-guarded). +Verified (`threshold_bcc_test.go`, all green): `FindHintToTarget↔UseHint` +round-trip, `BoundaryClear ⇒ HighBits-stable + r0-bound`, exact off-by-one +edges, offline yield ≈ **9.8 %**. + +**NOT RESOLVED.** The math is verified but the production path is not built. +Resolution criteria (all required for NIST/consensus): +- [x] `AlgebraicAggregate*` disabled in production builds (hard gate). +- [x] Hint derived only via public `FindHintToTarget(w', w1)` (FIPS `UseHint`). +- [x] No production code computes `c·s2`/`c·t0`/`r0`/`LowBits(residual)`. +- [x] Boundary predicate proves the hidden `r0` bound; ML-DSA-65 scope enforced. +- [ ] `CS2`/`CT0` and all hint-secret wire fields **deleted** from production messages (reflection test). +- [ ] **Full `w` never public / reconstructible** (PULSAR-V13-W-LEAK) — needs the ZK clearance proof. +- [ ] Partial-`z` correctness proof (PULSAR-V13-PARTIAL-Z-PROOF). +- [ ] Canonical, non-grindable nonce selection. +- [ ] DKG never reconstructs the master key / `t0`; certifies the `t0` bound. +- [ ] Rejected attempts simulatable, not publicly leaked; coarse abort classes. +- [ ] Tree aggregation (z-sums + bitmaps + proof roots) for ~1000 signers. +- [ ] Two-certificate consensus artifact (ML-DSA sig + signer bitmap/transcript root). +- [ ] Final sigs verify under ≥2 independent FIPS 204 verifiers on the BCC path. +- [ ] External cryptographic review of the no-MPC leaderless instantiation. + +### PULSAR-V13-W-LEAK (CRITICAL — replacement-design hazard) + +The boundary-cleared nonce certificate must **not** publish the full +commitment `w = A·y`. Once `z` is assembled, `w' = A·z − c·t1·2^d` is +public, so anyone with full `w` computes `w' − w = c·t0 − c·s2 = Δ` — the +same challenge-multiplied long-term-secret residual as PULSAR-V13-HINT-LEAK, +in a different form. Production may publish only `w1 = HighBits(w)`, a +commitment to `w`, and a **zero-knowledge boundary-clearance proof** (that a +hidden `w = A·y` is boundary-clear), never full `w`, `w_i` shares that +reconstruct it, `LowBits(w)`, or `w' − w`. The current `BoundaryClear(w)` +Go predicate and `spec` are **debug-oracle/prototype**: production needs the +ZK proof machinery, which does not yet exist ⇒ the BCC/CEF signing path is +**prototype, not production**, even though the arithmetic tests pass. + +### PULSAR-V13-PARTIAL-Z-PROOF (HIGH — consensus robustness) + +BCC/CEF removes the hint-path leakage, but leaderless consensus also needs +proof-carrying `z`-partials: each signer proves `z_i = λ_i·y_i + c·λ_i·s_{1,i}` +bound to `(session_id, nonce_id, party_id, DKG share commitment, nonce +commitment)` without revealing `y_i`/`s_{1,i}`. Otherwise one bad partial +fails the aggregate with no clean blame path (leaderless DoS). Verify +partials **without** `c·s2_i`/`c·t0_i`/`r0_i`/hint shares (those fields must +not exist). ## Forward-looking (v1.2) diff --git a/ref/go/pkg/pulsar/threshold_bcc.go b/ref/go/pkg/pulsar/threshold_bcc.go new file mode 100644 index 0000000..cb00b1c --- /dev/null +++ b/ref/go/pkg/pulsar/threshold_bcc.go @@ -0,0 +1,167 @@ +package pulsar + +import "errors" + +// Boundary-Cleared / Carry-Elimination threshold ML-DSA (Pulsar-BCC/CEF). +// +// No-MPC / no-TEE hint path replacing the leaking AlgebraicAggregate +// reconstruction (BLOCKERS.md PULSAR-V13-HINT-LEAK, +// spec/threshold-mldsa-boundary-clearance.tex). +// +// CONFORMANCE RULE (central invariant): the final hint h is determined by +// public nonce-region certificates and the public challenge — NEVER by +// reconstructing the secret residual. Nothing here forms c·s2, c·t0, r0, +// or LowBits(w + Δ). The hint is derived from the public reconstructed +// w' = A·z − c·t1·2^d and the public target w1 strictly via the FIPS 204 +// UseHint primitive (no informal "±1 corrector"). + +var ( + // ErrUnsafeThresholdV03HintPath gates the disabled, leaking + // AlgebraicAggregate path (PULSAR-V13-HINT-LEAK). + ErrUnsafeThresholdV03HintPath = errors.New( + "pulsar: threshold_v03 AlgebraicAggregate path is disabled " + + "(PULSAR-V13-HINT-LEAK: broadcasts c*s2/c*t0 hint-path secret " + + "material); use the BCC/CEF signing path") + + // ErrBCCParamSet rejects parameter sets outside the proven scope. + ErrBCCParamSet = errors.New( + "pulsar: Pulsar-BCC/CEF is proven for ML-DSA-65/87 only; this " + + "parameter set violates the ||c*t0||_inf < gamma2 bound") + + // ErrNoFIPSHint means no valid FIPS 204 hint reaches the target w1 for + // some coefficient (boundary/region violated, or weight > omega). + ErrNoFIPSHint = errors.New( + "pulsar: no valid FIPS hint reaches target w1 (boundary/region " + + "violated); consume the nonce and retry") +) + +// bccD is the ML-DSA Power2Round low-bit drop; t0 ∈ [−2^(d−1), 2^(d−1)]. +const bccD = 13 + +// bccParams returns (gamma2, beta = τ·η, omega) for a mode, and ok=false +// for any FIPS 204 parameter set outside the proven BCC scope. The scope +// condition is ‖c·t0‖∞ ≤ τ·2^(d−1) < γ2: it makes the FIPS c·t0 check +// vacuous and bounds the carry to ±1 high-bit. It holds for ML-DSA-65 +// (49·4096 < 261888) and ML-DSA-87 (60·4096 < 261888) but NOT ML-DSA-44 +// (39·4096 > 95232). Callers MUST gate on ok before signing. +func bccParams(mode Mode) (gamma2, beta, omega uint32, ok bool) { + tau, om, _, g2 := modeTauOmega(mode) + _, _, eta := modeShape(mode) + if uint32(tau)*(1<<(bccD-1)) >= g2 { + return 0, 0, 0, false + } + return g2, uint32(tau) * eta, uint32(om), true +} + +// boundaryThreshold is the centered-low-bits magnitude below which a +// coefficient is boundary-clear: |a0_centered(w_j)| < γ2 − 2β. The 2β +// margin covers BOTH the HighBits boundary (the ±β shift c·s2 cannot +// change HighBits) AND the FIPS r0 rejection edge (‖LowBits(w − c·s2)‖∞ < +// γ2 − β stays in range) — high-bit stability alone is insufficient. +func boundaryThreshold(gamma2 uint32, beta uint32) uint32 { return gamma2 - 2*beta } + +// centeredLowBits returns the FIPS Decompose low part of a, centered into +// (−γ2, γ2]. a must be normalized to [0, q). +func centeredLowBits(a uint32, gamma2 uint32) int32 { + a0plusQ, _ := decompose(a, gamma2) + a0 := int32(a0plusQ) + if a0plusQ > (mldsaQ-1)/2 { + a0 -= mldsaQ + } + return a0 +} + +// highBitsCoeff returns the FIPS Decompose high part a1 of a. +func highBitsCoeff(a uint32, gamma2 uint32) uint32 { + _, a1 := decompose(a, gamma2) + return a1 +} + +// boundaryClearCoeff reports whether coefficient a is far enough from +// every HighBits boundary that a hidden ±β shift cannot move its high bits +// and its hidden r0 stays in FIPS range. +func boundaryClearCoeff(a uint32, gamma2 uint32, beta uint32) bool { + a0 := centeredLowBits(a, gamma2) + if a0 < 0 { + a0 = -a0 + } + return uint32(a0) < boundaryThreshold(gamma2, beta) +} + +// BoundaryClear is the offline, message-independent, fully-public nonce- +// certification predicate: every coefficient of the public commitment w is +// boundary-clear for the c·s2 perturbation. A surviving nonce guarantees +// HighBits(w − c·s2) = HighBits(w) = w1 and the FIPS r0-norm check for +// every valid challenge — without ever computing c·s2. +func BoundaryClear(w polyVec, gamma2 uint32, beta uint32) bool { + for i := range w { + for j := 0; j < mldsaN; j++ { + if !boundaryClearCoeff(w[i][j], gamma2, beta) { + return false + } + } + } + return true +} + +// highBitsVec returns HighBits(w) coefficient-wise. w must be normalized. +func highBitsVec(w polyVec, gamma2 uint32) polyVec { + out := make(polyVec, len(w)) + for i := range w { + for j := 0; j < mldsaN; j++ { + out[i][j] = highBitsCoeff(w[i][j], gamma2) + } + } + return out +} + +// useHint applies one FIPS 204 (Algorithm 40) hint bit to coefficient r, +// returning the corrected high part r1. m = (q−1)/(2γ2) high-bit buckets. +// r must be normalized to [0, q). +func useHint(hbit, r, gamma2 uint32) uint32 { + m := uint32((mldsaQ - 1) / (2 * gamma2)) + r0plusQ, r1 := decompose(r, gamma2) + if hbit == 0 { + return r1 + } + r0 := int32(r0plusQ) + if r0plusQ > (mldsaQ-1)/2 { + r0 -= mldsaQ + } + if r0 > 0 { + return (r1 + 1) % m + } + return (r1 + m - 1) % m +} + +// findHintToTarget derives the ML-DSA hint from PUBLIC data only — the +// public reconstructed wPrime = A·z − c·t1·2^d and the public target w1 = +// HighBits(w). It NEVER forms c·s2, c·t0, or r0. The hint bit is not a +// signed correction: a coefficient takes h_j = 0 when HighBits already +// matches, h_j = 1 iff UseHint(1, ·) reaches the target, else there is no +// valid FIPS hint (boundary/region violated) and signing must consume the +// nonce and retry. Returns the hint and ok; ok=false ⇒ ErrNoFIPSHint. +// +// Theorem: findHintToTarget(wPrime, w1) = (h, true) iff +// UseHint(h, wPrime) = w1 and weight(h) ≤ omega. +func findHintToTarget(wPrime, targetW1 polyVec, gamma2, omega uint32) (polyVec, bool) { + h := make(polyVec, len(wPrime)) + var weight uint32 + for i := range wPrime { + for j := 0; j < mldsaN; j++ { + switch { + case highBitsCoeff(wPrime[i][j], gamma2) == targetW1[i][j]: + h[i][j] = 0 + case useHint(1, wPrime[i][j], gamma2) == targetW1[i][j]: + h[i][j] = 1 + weight++ + default: + return nil, false // no valid FIPS hint for this coefficient + } + } + } + if weight > omega { + return nil, false + } + return h, true +} diff --git a/ref/go/pkg/pulsar/threshold_bcc_test.go b/ref/go/pkg/pulsar/threshold_bcc_test.go new file mode 100644 index 0000000..8a1bc86 --- /dev/null +++ b/ref/go/pkg/pulsar/threshold_bcc_test.go @@ -0,0 +1,186 @@ +package pulsar + +import ( + "math/rand" + "testing" +) + +// These are DEBUG-ORACLE tests: they reconstruct the hidden commitment w +// directly to verify the BCC/CEF arithmetic, lemmas, and yield. Production +// code must NOT compute or publish full w (PULSAR-V13-W-LEAK); it publishes +// only w1, a commitment to w, and a ZK boundary-clearance proof. + +func randPolyVec(rng *rand.Rand, k int) polyVec { + w := make(polyVec, k) + for i := 0; i < k; i++ { + for j := 0; j < mldsaN; j++ { + w[i][j] = uint32(rng.Int63n(mldsaQ)) + } + } + return w +} + +func subMod(a uint32, delta int32) uint32 { + v := (int64(a) - int64(delta)) % mldsaQ + if v < 0 { + v += mldsaQ + } + return uint32(v) +} + +// The leaking AlgebraicAggregate path must be disabled by default +// (PULSAR-V13-HINT-LEAK), independent of any other signer state. +func TestThresholdV03DisabledByDefault(t *testing.T) { + s := &AlgebraicThresholdSigner{} + if _, _, err := s.Round2Sign(nil, nil); err != ErrUnsafeThresholdV03HintPath { + t.Fatalf("threshold_v03 must fail closed by default; got err=%v", err) + } +} + +// BCC/CEF is proven only where ||c·t0||_inf < gamma2 (ML-DSA-65/87, not 44). +func TestBCCParamGuard(t *testing.T) { + for _, m := range []Mode{ModeP65, ModeP87} { + if _, _, _, ok := bccParams(m); !ok { + t.Fatalf("mode %d must be in BCC scope", m) + } + } + if _, _, _, ok := bccParams(ModeP44); ok { + t.Fatalf("ML-DSA-44 must be rejected (tau*2^(d-1) >= gamma2)") + } + // Sanity on the c·t0 bound itself. + for _, m := range []Mode{ModeP65, ModeP87} { + tau, _, _, g2 := modeTauOmega(m) + if uint32(tau)*(1<<(bccD-1)) >= g2 { + t.Fatalf("mode %d: c·t0 bound should be vacuous", m) + } + } +} + +// Theorem: findHintToTarget(w', target) = (h, true) implies +// UseHint(h, w') = target coefficient-wise. The hint bit is validated via +// FIPS UseHint, never an informal ±1 corrector. +func TestFindHintToTargetMatchesUseHint(t *testing.T) { + gamma2, _, omega, _ := bccParams(ModeP65) + k, _, _ := modeShape(ModeP65) + rng := rand.New(rand.NewSource(2)) + checked := 0 + for iter := 0; iter < 3000; iter++ { + wPrime := randPolyVec(rng, k) + // Build a reachable, omega-sparse target like a real ML-DSA hint: + // baseline all h=0 (HighBits), then flip up to omega coefficients to + // the h=1 result. + target := highBitsVec(wPrime, gamma2) + nflip := rng.Intn(int(omega) + 1) + for f := 0; f < nflip; f++ { + i := rng.Intn(k) + j := rng.Intn(mldsaN) + target[i][j] = useHint(1, wPrime[i][j], gamma2) + } + h, ok := findHintToTarget(wPrime, target, gamma2, omega) + if !ok { + continue // weight > omega for random targets; skip + } + checked++ + for i := 0; i < k; i++ { + for j := 0; j < mldsaN; j++ { + if useHint(h[i][j], wPrime[i][j], gamma2) != target[i][j] { + t.Fatalf("UseHint(h,w') != target at [%d][%d]", i, j) + } + } + } + } + if checked == 0 { + t.Fatal("no reachable targets exercised") + } + t.Logf("verified UseHint(findHintToTarget(w',t),w')==t on %d vectors", checked) +} + +// Core BCC+ lemma (debug oracle): a boundary-clear w keeps HighBits stable +// under every hidden ||c·s2||_inf <= beta shift, and the hidden r0 stays in +// the FIPS rejection range — without the protocol ever forming c·s2 or r0. +func TestBoundaryClearImpliesHighBitsStable(t *testing.T) { + gamma2, beta, _, ok := bccParams(ModeP65) + if !ok { + t.Fatal("P65 params") + } + k, _, _ := modeShape(ModeP65) + rng := rand.New(rand.NewSource(1)) + cleared := 0 + for iter := 0; iter < 4000; iter++ { + w := randPolyVec(rng, k) + if !BoundaryClear(w, gamma2, beta) { + continue + } + cleared++ + hb0 := highBitsVec(w, gamma2) + for i := 0; i < k; i++ { + for j := 0; j < mldsaN; j++ { + delta := int32(rng.Intn(int(2*beta+1))) - int32(beta) // [-beta, beta] + shifted := subMod(w[i][j], delta) + if highBitsCoeff(shifted, gamma2) != hb0[i][j] { + t.Fatalf("HighBits moved under |c·s2|<=beta on boundary-clear w [%d][%d]", i, j) + } + r0 := centeredLowBits(shifted, gamma2) + if r0 < 0 { + r0 = -r0 + } + if uint32(r0) >= gamma2-beta { + t.Fatalf("hidden r0 bound violated on boundary-clear w [%d][%d]", i, j) + } + } + } + } + if cleared == 0 { + t.Fatal("no boundary-clear nonces sampled") + } + t.Logf("verified HighBits-stable + r0-bound on %d boundary-clear nonces", cleared) +} + +// Exact off-by-one audit of the 2β margin against FIPS Decompose. +func TestBoundaryClearEdgeCases(t *testing.T) { + gamma2, beta, _, _ := bccParams(ModeP65) + thr := int32(boundaryThreshold(gamma2, beta)) // gamma2 - 2*beta + mk := func(a0 int32) uint32 { // coefficient with centered low bits a0 in bucket 1 + v := (int64(2*gamma2) + int64(a0)) % mldsaQ + if v < 0 { + v += mldsaQ + } + return uint32(v) + } + cases := []struct { + a0 int32 + want bool + }{ + {thr - 1, true}, {thr, false}, {thr + 1, false}, + {-(thr - 1), true}, {-thr, false}, {-(thr + 1), false}, + {0, true}, + } + for _, c := range cases { + a := mk(c.a0) + if got := centeredLowBits(a, gamma2); got != c.a0 { + t.Fatalf("centeredLowBits(mk(%d))=%d", c.a0, got) + } + if got := boundaryClearCoeff(a, gamma2, beta); got != c.want { + t.Fatalf("boundaryClearCoeff(a0=%d)=%v want %v (thr=%d)", c.a0, got, c.want, thr) + } + } +} + +// Measure the real offline boundary-clearance yield for ML-DSA-65. +func TestBoundaryClearanceYield(t *testing.T) { + gamma2, beta, _, _ := bccParams(ModeP65) + k, _, _ := modeShape(ModeP65) + rng := rand.New(rand.NewSource(3)) + const trials = 3000 + clear := 0 + for i := 0; i < trials; i++ { + if BoundaryClear(randPolyVec(rng, k), gamma2, beta) { + clear++ + } + } + yield := float64(clear) / trials + t.Logf("ML-DSA-65 boundary-clear yield (margin 2β=%d, γ2=%d): %.4f", 2*beta, gamma2, yield) + if yield < 0.03 || yield > 0.25 { + t.Fatalf("yield %.4f outside expected ~0.10 band", yield) + } +} diff --git a/ref/go/pkg/pulsar/threshold_v03.go b/ref/go/pkg/pulsar/threshold_v03.go index 502dbc9..86848bc 100644 --- a/ref/go/pkg/pulsar/threshold_v03.go +++ b/ref/go/pkg/pulsar/threshold_v03.go @@ -439,6 +439,12 @@ type AlgebraicThresholdSigner struct { NodeID NodeID Share *AlgebraicKeyShare + // AllowUnsafeThresholdV03ForTests opts INTO the disabled, leaking + // AlgebraicAggregate hint path (PULSAR-V13-HINT-LEAK). Default false ⇒ + // Round2Sign fails closed with ErrUnsafeThresholdV03HintPath. Set only + // in tests exercising the legacy vector; NEVER in production. + AllowUnsafeThresholdV03ForTests bool + SessionID [16]byte Attempt uint32 @@ -754,15 +760,25 @@ func (s *AlgebraicThresholdSigner) Round2W(round1 []*AlgebraicRound1Message) (*A // (This party's own w_i is taken from local state — do not include it // in peerW.) // -// PUBLIC-BFT-SAFETY NOTE: this party's contribution (z_i, cs2_i, ct0_i) -// is INFORMATION-THEORETICALLY (t-1)-secret about its share material — -// the per-party arithmetic is z_i = y_i + c·λ_i·s_{1,i} where y_i is -// fresh randomness from this party's RNG and c is a public challenge. -// An adversary that obtains t-1 such contributions cannot recover any -// single party's s_{1,i} because the y_i mask hides it (each y_i is -// drawn from the FIPS 204 (-γ_1', γ_1'] uniform distribution, which -// is sufficient to mask under the M-LWE assumption). +// ⚠️ SECURITY-CRITICAL — PULSAR-V13-HINT-LEAK (see BLOCKERS.md). +// The y_i mask hides s_{1,i} in z_i = y_i + c·λ_i·s_{1,i} (correct). But +// the cs2_i = c·λ_i·s_{2,i} and ct0_i = c·λ_i·t_{0,i} fields emitted by +// round2EmitFull below carry NO mask. Since c and λ_i are public, +// s_{2,i} = (c·λ_i)^{-1}·cs2_i is recoverable; and the aggregate +// Σ cs2_i = c·s2_master (likewise ct0_i → t0) leaks long-term ML-DSA +// secret-key material over varying-c sessions plus the secret relation +// A·s1 = (t1·2^d + t0) − s2 — breaking threshold secrecy and transcript +// simulation. The prior claim that (z_i, cs2_i, ct0_i) are +// (t-1)-secret was FALSE — it only held for z_i. This path is being +// replaced by boundary-cleared nonces + carry elimination +// (spec/threshold-mldsa-boundary-clearance.tex), which never forms +// c·s2/c·t0/r0. Do NOT rely on this path for production secrecy. func (s *AlgebraicThresholdSigner) Round2Sign(round1 []*AlgebraicRound1Message, peerW map[NodeID]polyVec) (*AlgebraicRound2Message, *AbortEvidence, error) { + // PULSAR-V13-HINT-LEAK: this path broadcasts c*s2/c*t0 hint-path secret + // material; fail closed in production. Opt in only for legacy tests. + if !s.AllowUnsafeThresholdV03ForTests { + return nil, nil, ErrUnsafeThresholdV03HintPath + } return s.round2EmitFull(round1, peerW) } diff --git a/spec/threshold-mldsa-boundary-clearance.tex b/spec/threshold-mldsa-boundary-clearance.tex new file mode 100644 index 0000000..4d7e785 --- /dev/null +++ b/spec/threshold-mldsa-boundary-clearance.tex @@ -0,0 +1,250 @@ +\documentclass[11pt]{article} +\usepackage{amsmath,amssymb,amsthm} +\usepackage[margin=1in]{geometry} +\newtheorem{lemma}{Lemma} +\newtheorem{theorem}{Theorem} +\newtheorem{definition}{Definition} +\theoremstyle{remark}\newtheorem{remark}{Remark} +\title{Pulsar Threshold ML-DSA via Boundary-Cleared Nonces and Carry +Elimination\\(No MPC, No TEE) --- BCC0 / BCC+} +\author{Lux Core Team --- \texttt{github.com/luxfi/pulsar}} +\date{} +\begin{document} +\maketitle + +\section{The leak this replaces} +The v0.3/v0.4 \texttt{AlgebraicAggregate} path reconstructs $c\,\mathbf +s_2^{\mathrm{joint}}$ and $c\,\mathbf t_0^{\mathrm{joint}}$ at the +aggregator to form the FIPS hint. But $\mathbf s_2^{\mathrm{joint}}$ is +the master $\mathbf s_2$ (Shamir reconstruction) and $c$ is public and +varies per session, so revealing $c\,\mathbf s_2^{\mathrm{joint}}$ over +sessions is a linear system in the fixed $\mathbf s_2$ --- one invertible +$c$ recovers it; then $A\mathbf s_1 = \mathbf t - \mathbf s_2$ recovers +$\mathbf s_1$, a total key break. In the leaderless model every quorum +member aggregates, so every corrupt validator learns it. \textbf{Masking +the per-party shares does not help: the masks cancel in the aggregate the +protocol must reconstruct.} The cure is never to form the secret residual. + +\section{The invariant and the whole game} +With $\mathbf w = A\mathbf y$, $\mathbf z = \mathbf y + c\,\mathbf s_1$, +$\mathbf t = A\mathbf s_1 + \mathbf s_2 = \mathbf t_1 2^d + \mathbf t_0$, +the verifier recomputes +\[ + \mathbf w' \;=\; A\mathbf z - c\,\mathbf t_1 2^d + \;=\; \mathbf w + c\,\mathbf t_0 - c\,\mathbf s_2 + \;=\; \mathbf w + \Delta, \qquad \Delta := c\,\mathbf t_0 - c\,\mathbf + s_2, +\] +and accepts iff $\mathrm{UseHint}(\mathbf h, \mathbf w') = \mathbf w_1$ +where $\mathbf w_1 = \mathrm{HighBits}(\mathbf w)$ fixed $c = H(\mu \| \mathbf +w_1)$. +\begin{theorem}[No-leak target] +Produce a public $\mathbf h$ with $\mathrm{UseHint}(\mathbf h, \mathbf w + +\Delta) = \mathrm{HighBits}(\mathbf w)$ \emph{without} revealing $\Delta$, +$\mathrm{LowBits}(\mathbf w + \Delta)$, $c\,\mathbf s_2$, $c\,\mathbf +t_0$, or $r_0$. +\end{theorem} + +\section{Conformance rule (central invariant)} +\label{sec:rule} +\textbf{The final hint $\mathbf h$ must be determined by public +nonce-region certificates and the public challenge --- never by +reconstructing the secret residual.} For BCC0 the certificate guarantees +$\mathbf h = 0$; for BCC+ it guarantees a publicly-determined hint +pattern. \emph{Any implementation that computes $\mathbf h$ by first +forming $c\,\mathbf s_2$, $c\,\mathbf t_0$, $r_0$, or +$\mathrm{LowBits}(\mathbf w + \Delta)$ is non-conformant.} Note $\mathbf +w' = A\mathbf z - c\,\mathbf t_1 2^d$ is itself \emph{public} (computable +by the verifier from $A,\mathbf z,c,\mathbf t_1$); reading $\mathbf h$ off +$(\mathbf w', \mathbf w_1)$ reveals only $\mathbf h$, which is in the +signature anyway --- it is \emph{not} residual reconstruction. + +\subsection{Full $\mathbf w$ must be hidden (PULSAR-V13-W-LEAK)} +The full commitment $\mathbf w = A\mathbf y$ must \emph{never} be public or +reconstructible by a $t-1$ coalition. Since $\mathbf w' = A\mathbf z - +c\,\mathbf t_1 2^d$ becomes public once $\mathbf z$ is assembled, anyone +holding full $\mathbf w$ computes $\mathbf w' - \mathbf w = c\,\mathbf t_0 +- c\,\mathbf s_2 = \Delta$ --- the same long-term-secret residual as the +original leak. \textbf{Public:} $\mathbf w_1$, a commitment to $\mathbf w$, +a \emph{zero-knowledge} boundary-clearance proof, and the final $(\mathbf +z,\mathbf h,\text{sig})$. \textbf{Forbidden:} full $\mathbf w$, $\mathbf +w_i$ shares reconstructing it, $\mathrm{LowBits}(\mathbf w)$, $\mathbf w' - +\mathbf w$. Hence $\textsc{BoundaryClear}(\mathbf w)$ on \emph{public} +$\mathbf w$ is \textbf{debug-oracle only}; production replaces it with a ZK +proof that a hidden $\mathbf w = A\mathbf y$ satisfies the predicate, +revealing none of $\mathbf w$, $\mathrm{LowBits}(\mathbf w)$, or per- +coefficient distances. \textbf{Until that ZK machinery exists the BCC/CEF +signing path is prototype, not production.} + +\section{Profiles} +\subsection{BCC0 --- conservative $\mathbf h = 0$} +Use only nonces whose hidden shift cannot move any coefficient across a +high-bit boundary: $\mathrm{HighBits}(\mathbf w + \Delta) = +\mathrm{HighBits}(\mathbf w)$, so $\mathbf h = 0$. +\begin{lemma}[BCC0 stability]\label{lem:bcc0} +$\textsc{BoundaryClear}(\mathbf w, B_\Delta) \wedge \|\Delta\|_\infty \le +B_\Delta \;\Rightarrow\; \mathrm{HighBits}(\mathbf w + \Delta) = +\mathrm{HighBits}(\mathbf w)$, whence $\mathrm{UseHint}(0, \mathbf w') = +\mathbf w_1$ and unmodified FIPS 204 accepts. +\end{lemma} +\textbf{BCC0 is infeasible for ML-DSA-65} (\S\ref{sec:bounds}): the worst- +case $B_\Delta$ exceeds $\gamma_2$, so no coefficient can clear. Retained +as a definition / fallback profile only, not used. + +\subsection{BCC+ --- carry elimination, nonzero $\mathbf h$} +Allow $\mathbf h \neq 0$, but derive it from public data. The shift splits +into a \emph{small} part $-c\,\mathbf s_2$ and a \emph{large} part +$c\,\mathbf t_0$. Boundary-clear \emph{only} the small part; the large +part is resolved by the public hint. +\begin{definition}[Per-coefficient region] +For coefficient $w_j$ and margin $B$ (covering $\|c\,\mathbf +s_2\|_\infty$), classify by FIPS \texttt{Decompose}: +$\textsc{SafeZeroCarry}$ if $\mathrm{dist}(w_j) > B$ and the $c\,\mathbf +t_0$ carry cannot cross; $\textsc{SafeKnownCarry}$ if the carry is +resolvable to a single public bit from $\mathbf w'$; $\textsc{Unsafe}$ +otherwise. Accept a nonce iff no coefficient is $\textsc{Unsafe}$. +\end{definition} +\begin{lemma}[BCC+ correctness]\label{lem:bccplus} +If $\textsc{BoundaryClear}(\mathbf w, 2\beta)$ (clears $c\,\mathbf s_2$) +and $\|c\,\mathbf t_0\|_\infty < \alpha$ (so each coefficient's high bits +move by at most $\pm 1$), then (i) $\mathrm{HighBits}(\mathbf w - +c\,\mathbf s_2) = \mathbf w_1$ and $\|\mathrm{LowBits}(\mathbf w - +c\,\mathbf s_2)\|_\infty < \gamma_2 - \beta$ (the FIPS $r_1{=}\mathbf +w_1$, $r_0$-norm conditions); and (ii) the public hint $h_j := [\, +\mathrm{HighBits}(w'_j) \neq w_{1,j}\,]$ equals the FIPS hint +$\mathrm{MakeHint}(-c\,\mathbf t_0, \mathbf w - c\,\mathbf s_2)$ and +satisfies $\mathrm{UseHint}(\mathbf h, \mathbf w') = \mathbf w_1$. +\end{lemma} +\emph{Reconciliation with ``region-derived'':} the $c\,\mathbf t_0$ carry +depends on the secret $\mathbf t_0$ and the online $c$, so it cannot be +fixed fully offline; the \emph{offline} certificate clears $c\,\mathbf +s_2$ and bounds the carry to $\pm 1$, and the \emph{online} step reads the +carry bit off the public $\mathbf w'$. Both inputs ($\mathbf w'$, $\mathbf +w_1$) are public; no residual is formed. This is BCC+ \S2A realised. + +\section{Concrete bounds (ML-DSA-65)} +\label{sec:bounds} +$q{=}8380417,\ d{=}13,\ \tau{=}49,\ \eta{=}4,\ \gamma_2{=}261888,\ +\alpha{=}2\gamma_2{=}523776,\ \beta{=}\tau\eta{=}196,\ \omega{=}55$. +\begin{itemize} +\item $\|c\,\mathbf s_2\|_\infty \le B_{s_2} = \tau\eta = 196$. +\item $\|c\,\mathbf t_0\|_\infty \le \tau\,2^{d-1} = 49\cdot4096 = 200704 + < \gamma_2 < \alpha$: the FIPS $\|c\,\mathbf t_0\|<\gamma_2$ check is + \emph{vacuous} (always holds), and the carry moves $\mathrm{HighBits}$ + by at most $\pm1$ per coefficient. No check, no reconstruction. +\item \textbf{BCC0 infeasible:} needs clearance $> B_\Delta = B_{s_2} + + \tau\,2^{d-1} \approx 401555 > \gamma_2 = 261888$ (max possible + clearance). Yield $0$. +\item \textbf{BCC+ feasible:} clear only $c\,\mathbf s_2$ with margin $B = + 2\beta = 392$ (covers the $\mathrm{HighBits}$ boundary and the $r_0 < + \gamma_2-\beta$ edge). Per-coefficient clear prob $\approx 1 - + B/\gamma_2 = 0.9985$; all-$256{\cdot}6$ yield $\approx 0.10$ (measure; + raise margin only, never lower). $c\,\mathbf t_0$ contributes the + nonzero, $\omega$-sparse public hint. +\end{itemize} + +\section{Proof obligations} +\paragraph{BCC0 chain (Lemma~\ref{lem:bcc0}).} $\mathbf w{=}A\mathbf y$; +$\mathbf z{=}\mathbf y{+}c\mathbf s_1$; $A\mathbf z{-}c\mathbf t_1 2^d +{=}\mathbf w{+}\Delta$; $\|\Delta\|_\infty\le B_\Delta$; +$\textsc{BoundaryClear}(\mathbf w,B_\Delta)$ $\Rightarrow$ +$\mathrm{HighBits}(\mathbf w{+}\Delta){=}\mathbf w_1$ $\Rightarrow$ +$\mathrm{UseHint}(0,\cdot){=}\mathbf w_1$ $\Rightarrow$ accept. +\paragraph{BCC+ / CEF chain (Lemma~\ref{lem:bccplus}).} as above with the +public hint; $h$ region/public-$\mathbf w'$-derived; for all $\Delta$ with +$\|\Delta\|_\infty\le B_\Delta$, $\mathrm{UseHint}(\mathbf h,\mathbf w{+} +\Delta){=}\mathbf w_1$. +\paragraph{Soundness.} A malicious signer's bad $\mathbf z_i$ yields a +wrong $\mathbf w'$ and a wrong $\mathbf h$ $\Rightarrow$ the mandatory +final unmodified-FIPS verify \emph{fails} (identifiable abort via the +per-party $\mathbf z_i$ proof/MAC). \textbf{Never fall back to forming +$c\,\mathbf s_2$/$c\,\mathbf t_0$/$r_0$.} +\paragraph{Transcript privacy / simulatability.} The transcript holds +$\{\mathbf w,\mathbf w_1,c,\mathbf z,\mathbf h,\text{commitments}, +\text{proofs}\}$ and \emph{not} $c\,\mathbf s_{2,i}$, $c\,\mathbf +t_{0,i}$, $c\,\mathbf s_2^{\mathrm{joint}}$, $c\,\mathbf +t_0^{\mathrm{joint}}$, $\Delta$, $r_0$, $\mathrm{LowBits}(\mathbf +w{+}\Delta)$. A simulator reproduces it from $(pk, m, \text{final sig}, +\text{signer bitmap}, \text{corrupt shares})$ without honest shares. +\paragraph{Conditioned-nonce security (hardest).} Conditioning the pool on +the public predicate $\textsc{BoundaryClear}(\mathbf w, 2\beta)$ (resp.\ +$\textsc{AllRegionsSafe}$) must not weaken EUF-CMA: $\mathbf w = A\mathbf +y$ is independent of the key, and the surviving $\mathbf y$ distribution +must remain a valid rejection-sampled nonce distribution (or the signature +distribution must remain simulatable). \emph{This is a required proof, not +an assumption; if \textsc{2B nonce shaping} is used, the distribution +proof is mandatory before deployment.} + +\section{Wire format (deletion audit)} +\textbf{Remove} \texttt{CS2}, \texttt{CT0} (and any \texttt{cs2}, +\texttt{ct0}, \texttt{D2}, \texttt{D0}, \texttt{R0Share}, +\texttt{LowBitsShare}, \texttt{HintInput}, \texttt{HintShare}) from the +Round-2 message and the $\tau_2$ transcript. Old fields fail +deserialization outside an explicit legacy-test parser. +\begin{verbatim} +type BoundaryNonceCert struct { + NonceID [32]byte; PKEpoch uint64; CommitteeID [32]byte + SignerSetRoot [32]byte; W1 PackedHighBits; WCommitment []byte + ClearanceProof []byte; Margin uint32; CommitRoot [32]byte; Consumed bool } + // NO full W field (PULSAR-V13-W-LEAK); W is debug-oracle only. +type ZPartial struct { + PartyID PartyID; NonceID [32]byte; SessionID [32]byte + ZShare PackedPolyVecL; Proof []byte; MAC []byte } +type PulsarSignature struct { C PackedChallenge; Z PackedPolyVecL; H PackedHint } +\end{verbatim} +No \texttt{CS2/CT0/D2/D0/R0Share/LowBitsShare/HintInput/HintShare}. + +\section{Protocol} +\paragraph{Offline (message-independent) nonce pool.} Sample $\mathbf +y_i$; commit. The aggregate $\mathbf w = \sum\lambda_i\mathbf w_i$ is +\emph{hidden}: in production each signer proves in zero knowledge that the +hidden $\mathbf w$ is boundary-clear, publishing only $\mathbf w_1$, a +commitment to $\mathbf w$, and the clearance proof (PULSAR-V13-W-LEAK; the +debug oracle may form $\mathbf w$ to classify regions vs $B$). If +\textsc{AllRegionsSafe}, store the cert ($\mathbf w_1,\text{WCommitment}, +\text{ClearanceProof},\text{CommitRoot}$); else discard. Run continuously off +the consensus path. +\paragraph{Online sign.} Pick an unused cert; $\mu = H(pk\|ctx\|m)$, $c = +H(\mu\|\mathbf w_1)$; collect $\mathbf z_i = \lambda_i\mathbf y_i + +c\lambda_i\mathbf s_{1,i}$; $\mathbf z = \sum\mathbf z_i$; reject to a +fresh nonce if $\|\mathbf z\|_\infty \ge \gamma_1-\beta$; compute public +$\mathbf w' = A\mathbf z - c\mathbf t_1 2^d$ and $\mathbf h$ (BCC0: +$\mathbf 0$; BCC+: $h_j=[\mathrm{HighBits}(w'_j)\neq w_{1,j}]$); reject if +$\mathrm{wt}(\mathbf h) > \omega$; emit $\textsc{sigEncode}(\tilde +c,\mathbf z,\mathbf h)$; assert unmodified FIPS 204 verify (failure $=$ +bug). + +\section{Fallback (Option 3)} +If unmodified-FIPS-204-byte-equality is not mandatory, use the +Raccoon/Ringtail-style threshold-friendly hint scheme --- this is exactly +the \textbf{Corona} route (\texttt{luxfi/corona}, LP-4440): public +threshold signature, leaderless, no MPC/TEE, but \emph{not} FIPS-byte- +equal. + +\section{Scale / consensus notes} +For $\sim$1000+ validators: generate boundary-safe nonce certs +continuously offline; online consensus only tree-aggregates $\mathbf z$ +shares; the final signature is ordinary ML-DSA; the QC carries the signer +bitmap $+$ transcript root. Do \emph{not} boundary-filter online per +message. + +\section{Practical risks} +(1) usable safe-nonce rate; (2) the conditioned-nonce distribution proof; +(3) exact FIPS boundary classification (against \texttt{Decompose}, not +integer rounding); (4) keeping the margin small enough for yield while +covering $c\,\mathbf s_2$. If BCC+ yield is poor, prefer \textsc{2B nonce +shaping} (with its distribution proof) over weakening the margin. + +\section{Phased plan + TALUS alignment} +\textbf{Phase 1:} BCC+ as above --- this spec, Lemmas~\ref{lem:bcc0}, +\ref{lem:bccplus} machine-checked (\texttt{Crypto/Pulsar/Boundary\- +Clearance.lean}) against the FIPS \texttt{Decompose}/\texttt{HighBits}/ +\texttt{MakeHint}/\texttt{UseHint} definitions, Go impl reusing the +existing \texttt{decompose}/\texttt{power2Round} primitives, the +regression / no-residual / distribution / CIRCL$+$pq-crystals interop +tests on the BCC path, and the offline-yield measurement. +\textbf{Phase 2:} \textsc{2B nonce shaping} if yield demands, with the +distribution proof. \textbf{Phase 3:} align terminology and proof +obligations with the TALUS boundary-clearance / carry-elimination +construction. +\end{document}