tla: model-check verifier-challenge gaps (#429 fail-open, #431 scan coverage) - #454
Open
eigmax wants to merge 4 commits into
Open
tla: model-check verifier-challenge gaps (#429 fail-open, #431 scan coverage)#454eigmax wants to merge 4 commits into
eigmax wants to merge 4 commits into
Conversation
Two TLA+ specs (node/tla/) formalising the unauthorized-kickoff -> uncontested Take1 threat, verified against the real dev (gc-v2) source and reproduced under TLC. VerifierKickoffFailOpen (issue #429) - LIVE on dev. handle_kickoff_sent_verifier is one-shot and fail-open: when GOAT SPV lags the kickoff height it returns Ok(()) with no push_local_unhandled_messages_with_ reason, so the KickoffSent message is marked Processed and the Challenge is never retried (detect_kickoff only re-scans OperatorDataPushed; should_always_ challenge is never called). The committee handler defers the same lag; the verifier does not. - VerifierKickoffFailOpen.cfg -> FAILS (NoUnauthorizedTake1, 3-step CEX) - VerifierKickoffFailOpenFixed.cfg -> passes (defer/retry, mirroring committee) KickoffScanCoverage (issue #431) - FIXED on dev by 2bce25d (#451). detect_kickoff's per-operator round-robin (fetch_first_graph_per_operator_by_ status) watched only the lowest-nonce graph, so a kickoff on a later graph was never observed. scan_kickoff_chain now walks confirmed prekickoff successors from the idle root, closing the filed 2-graph attack; detect_take1_or_challenge and process_graph_challenge also moved to fetch_all_graphs_by_status. - KickoffScanCoverage.cfg -> FAILS (original one-per-operator select) - KickoffScanCoverageFixed.cfg -> passes (chain walk, adequate depth) - KickoffScanCoverageResidual.cfg -> FAILS (chain deeper than the MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 cap) Root cause (shared): the challenge defense is built from best-effort, at-most-once local scheduling primitives (round-robin selection, one-shot message handlers) rather than a persistent challenge obligation created by complete observation and retired only by an on-chain Challenge. #431 is the completeness face; #429 is the persistence face.
- pull_request trigger now runs on ANY base branch (was main/dev/gc-v2), so the tla-plus gate (and the CI behind it) runs on every PR. - must-pass step now also runs VerifierKickoffFailOpenFixed (#429 fix design) and KickoffScanCoverageFixed (#431 shipped fix) - both must pass. - bug-reproduction step now also tracks VerifierKickoffFailOpen (#429, LIVE), KickoffScanCoverage (#431, fixed by #451), and KickoffScanCoverageResidual (#431 depth-cap residual) as reproduction pointers; an unexpected PASS on any still fails the job as a drift signal. - reproduction-step summary reworded: the list is no longer all-fixed-by-991faaa. Verified locally: must-pass step exits 0 (11 specs), bug step exits 0 (all reproduce, no drift).
Replace the two ad-hoc TLA+ steps with a single declarative spec table + a
generic router. Every spec carries a tier and the script routes by it - no
per-issue logic:
pass - fix/baseline design; MUST verify clean (else a fix regressed).
historical - a bug fixed in code, kept as a frozen regression record; MUST
still reproduce its counterexample (an unexpected PASS = spec
drift or a reverted fix -> hard fail).
live - a known-unfixed bug; while its frozen spec still reproduces the
counterexample it is an OPEN finding that BLOCKS merge. Clear it
by fixing the code and moving the row's tier to `historical`.
Adding any future finding is one row; fixing a live bug is one word. This makes
the gate generic for all similar issues instead of hardcoding each one.
Current live (blocking) rows: issue #429 (verifier KickoffSent fail-open) and
the issue #431 depth-cap residual. All Findings 1-9 and issue #431 are
historical (informational).
Verified locally: pass specs verify, historical specs reproduce, the 2 live
rows are flagged OPEN and the step exits 1 (blocks merge, as intended).
- The TLA+ step now runs ALL specs (no early exit on the first failure) and prints a dynamic result table in the job summary - each row shows the spec's actual TLC outcome (verified / counterexample) and a computed status, instead of static pre-written labels. It accumulates failures and exits 1 at the end if any (still blocking merge on live bugs). - Removed `needs: tla-plus` from fmt/clippy/test so every check runs on every PR in parallel, regardless of the TLA+ outcome. tla-plus is now a first-class parallel check rather than a hard gate that skips the others. Verified locally: all 20 specs run, table renders, 2 live bugs -> exit 1.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Two TLA+ specs in
node/tla/that formally model the unauthorized-kickoff → uncontested Take1 threat, verified against the realdev(gc-v2) source and reproduced under TLC. Companion to issues #429 and #431.Run any spec:
#429 — verifier KickoffSent challenge is one-shot & fail-open (LIVE on dev)
handle_kickoff_sent_verifierreturnsOk(())on the SPV-lag branch (kickoff_height >= goat_confirmed_btc_height) withoutpush_local_unhandled_messages_with_reason, so the message is markedProcessedand the Challenge is never retried.detect_kickoffonly re-scansOperatorDataPushed;should_always_challengeis never called. The committee handler defers the same lag — the verifier does not.VerifierKickoffFailOpen.cfg(current code)NoUnauthorizedTake1violated (3-step counterexample)VerifierKickoffFailOpenFixed.cfg(defer/retry)#431 — detect_kickoff coverage gap (FIXED on dev by 2bce25d / #451)
The per-operator round-robin (
fetch_first_graph_per_operator_by_status) watched only the lowest-nonce graph, so a kickoff on a later graph was never observed.scan_kickoff_chainnow walks confirmed prekickoff successors from the idle root, closing the filed 2-graph attack;detect_take1_or_challenge/process_graph_challengealso moved tofetch_all_graphs_by_status. A residual remains: the walk is capped atMAX_PREKICKOFF_SUCCESSORS_PER_SCAN = 32, so a chain of >32 idle decoys with a kick beyond depth 32 still escapes.KickoffScanCoverage.cfg(original one-per-operator)kicked = 1escapesKickoffScanCoverageFixed.cfg(chain walk, adequate depth)KickoffScanCoverageResidual.cfg(chain deeper than the cap)kicked = 3escapesRoot cause (shared)
The challenge defense is built from best-effort, at-most-once local scheduling primitives (round-robin selection, one-shot message handlers) rather than a persistent challenge obligation created by complete observation of confirmed kickoffs and retired only by an on-chain Challenge. #431 is the completeness face; #429 is the persistence face. A single "scan all confirmed kickoffs → create obligation → clear only on Challenge-confirm" design forecloses both.
Notes
tla-plusgate now runs on every PR (any base branch). The two*Fixedconfigs are in the must-pass step; [Security] Verifier KickoffSent challenge is one-shot and fail-open (unauthorized Take1) #429, [Security] detect_kickoff only watches one OperatorDataPushed graph per operator (unauthorized Take1) #431, and the [Security] detect_kickoff only watches one OperatorDataPushed graph per operator (unauthorized Take1) #431 depth-cap residual are tracked as reproduction pointers (only an unexpected PASS — drift — fails the job). Verified locally: must-pass exits 0, bug step exits 0.🤖 Generated with Claude Code