mirror of
https://github.com/luxfi/corona.git
synced 2026-07-27 02:50:34 +00:00
Antje Worring
dc15c54a47
Closes the CRIT-1 residual (D1-2) sid-entropy gap and the CT/doc hygiene
gaps to bring Corona to the no-leak/no-gap bar. EasyCrypt proofs untouched.
PRIORITY 1 — anti-nonce-reuse / no-leak durability:
- The Round-1 nonce-PRF key no longer keys on a bare 64-bit sid. It now
derives from a 256-bit domain-separated SessionID (primitives.DeriveSessionID:
TranscriptHash("corona.sign.session-id.v1" || be64(sid) || T)) AND a fresh
per-signature 256-bit hedge salt drawn inside the kernel from party.Rand
(default crypto/rand). PRNGKeyForRound = PRF(skShare, "CoronaNonceV3" ||
sessionID || salt). Hedging restores threshold-Raccoon's fresh-per-signature
nonce posture: reuse durability no longer rests on the external consensus
layer never reissuing an sid — even an sid collision yields distinct R with
prob 2^-256. A deterministic 256-bit SessionID alone is necessary but NOT
sufficient (it repeats when sid repeats); the salt is what closes the leak.
- SignRound1 is fail-closed: rejects an all-zero derived SessionID or all-zero
salt with ErrDegenerateSession, and surfaces a short-read error. The
consensus slot-uniqueness invariant is documented as a HARD precondition at
SignRound1 and Signer.Round1 (no longer a buried comment).
- KAT/oracle determinism preserved via one seam: sign.DeterministicNonceSource
(KeyedPRNG over seed || "corona.sign.nonce-salt.v1" || partyIndex), set on
Party.Rand / Signer.SetNonceRand only by reproducibility harnesses.
- SignRound1 / Signer.Round1 now return an error; all call sites updated.
- KAT REGEN: only sign_verify_e2e.json changes (nonce-key bytes moved);
transcript_hash.json / MAC / legacy PRNGKey vectors are byte-stable, proving
the consensus-agreed transcript path was left untouched. Regenerated via
`bash scripts/regen-kats.sh`; `--verify` confirms byte-determinism (10 files).
- Regression: sign/nonce_reuse_test.go proves same-(skShare,sid) yields distinct
D (fresh R), pinned-nonce reproduces byte-identically, and the degenerate-
session guard fires. TestE2EKATReplayDeterminism rewritten to assert both the
hedged-differs and pinned-reproduces properties (was a defanged no-op).
PRIORITY 2 — constant-time hygiene:
- reshare/commit.go already used a constant-time comparator; the real gap was
the verbatim duplication of constTimePolyEqual+uint64SliceToBytes across dkg2
and reshare. Consolidated to one canonical utils.ConstantTimePolyEqual; both
delegate (no dkg2<->reshare dependency). Orphaned imports removed.
- FullRankCheck and the reshare commit path are now covered in the CT review
with their public-operand justification.
PRIORITY 3 — doc accuracy:
- CONSTANT-TIME-REVIEW.md rewritten Corona-specific and file:line-accurate:
drops the stale Pulsar/lens/warp/secp256k1 content; audits the real call
sites (hedged nonce key, masking PRF, lattigo samplers as the residual TCB
axiom, utils.ConstantTimePolyEqual, CheckL2Norm/Verify/FullRankCheck big.Int
variable-time on PUBLIC operands, activation/commit-digest array equality,
keyera/reshare zeroization).
- PROOF-CLAIMS.md §1: threshold.Combine / sign.LocalSign (nonexistent) -> the
real sign.Party.SignFinalize exposed as threshold.Signer.Finalize.
- threshold/threshold.go package doc: Ring-LWE -> Module-LWE.
Corona dudect constant-time harness
Statistical CT validation for Corona's threshold path, mirroring ~/work/lux/pulsar/ct/dudect/.
What's here
| File | Purpose |
|---|---|
verify_ct.go |
cgo bridge: corona threshold.Verify |
combine_ct.go |
cgo bridge: corona threshold Signer.Finalize (Combine) |
dudect_verify.c |
dudect main loop driving Verify |
dudect_combine.c |
dudect main loop driving Combine |
dudect_compat.h |
AArch64 compat shim for x86 intrinsics |
Makefile |
build verify + combine binaries |
fetch.sh |
clone upstream dudect at the pinned commit |
Build + run
./fetch.sh # first time only -- clones dudect
make # builds dudect_verify + dudect_combine
./dudect_verify # smoke test (10000 samples/batch * 4 batches)
./dudect_combine # smoke test (2000 samples/batch * 4 batches)
Submission run
# 10^9 samples per target on a pinned-CPU quiet host:
DUDECT_SAMPLES=1000000 DUDECT_MAX_BATCHES=1000 ./dudect_verify
DUDECT_SAMPLES=1000000 DUDECT_MAX_BATCHES=1000 ./dudect_combine
CT-population framing
Both harnesses use the valid-signature class framing:
- Verify: both class A and class B are valid Corona signatures on the same (group_pk, message). They differ only in the per-signing rejection-loop randomness. Any timing difference detected is a signature-content-dependent code path in Verify.
- Combine: both class A and class B are valid R2-data tuples. The Combine path has NO secret inputs (every input is broadcast on the wire), so any timing difference is an unexpected content-dependent code path in Finalize.
The valid-class framing differs from the simpler garbage-bytes-vs- random-bytes pattern because Corona Verify has no secret state to leak; the empirically meaningful CT property is the valid-population constancy.
Hosts
- x86_64 Linux/macOS: builds against upstream dudect.h directly.
- aarch64 Linux/macOS:
dudect_compat.his force-included to supply AArch64 cycle-counter equivalents (CNTVCT_EL0 on Linux,mach_absolute_time()on Darwin).
Limitations
- 10000-sample smoke runs are NOT statistically meaningful for CT certification. The smoke-test pass is "the harness compiles and runs without obvious leakage signal." The submission-grade verdict requires the full 10^9-sample run on pinned, quiet hardware.
- Combine's CT property is trivially true (no secret inputs); the Combine harness is a SANITY CHECK on the Finalize pipeline, not a property test.
Refinement
The dudect harnesses provide EMPIRICAL CT evidence for the modules:
Verify: corona/threshold/threshold.go:Verify + corona/sign/sign.go:VerifyCombine: corona/threshold/threshold.go:Signer.Finalize + corona/sign/sign.go:SignFinalize
The Jasmin-CT theoretical CT proof for the threshold layer is in
~/work/lux/corona/jasmin/threshold/{round1,round2,combine}.jazz and
scripts/checks/jasmin.sh enforces it as a per-push blocking gate.