diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 65ed43d2..0213728c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -7,11 +7,9 @@ on: - dev tags: - v[0-9]+.* + # Run on every pull request regardless of base branch, so the TLA+ formal- + # verification gate (and the rest of CI behind it) runs on ANY PR. pull_request: - branches: - - main - - dev - - gc-v2 env: CARGO_TERM_COLOR: always @@ -21,20 +19,12 @@ concurrency: cancel-in-progress: true jobs: - # Runs first and gates everything else (fmt/clippy/test all `needs: tla-plus` - # below) - it's the fastest job (seconds, no Rust toolchain to build) and a - # failure here means either a real regression the other, much slower jobs - # can't catch, or a stale/broken spec - either way not worth burning 30+ - # minutes of Cargo Test/Clippy compute on before finding out. - # - # All 8 findings from audit/TLAPlus-20260630.md were fixed in commit - # 991faaa, so this job is expected to be GREEN. Its steps still run every - # bug config that reproduced the original counterexamples, but a bug - # config correctly still failing is no longer treated as a job failure - - # see the second step's own comment for why (its constants are frozen - # historical snapshots, not a live read of the Rust source, so they can't - # detect a regression by staying red; only an unexpected PASS is a real - # drift signal now). + # Runs independently and in parallel with fmt/clippy/test (no `needs:` gating) + # so EVERY check runs on every PR regardless of the others' outcome. It is a + # first-class check: it fails (and blocks merge, if branch protection requires + # it) whenever a `live` bug spec still reproduces its counterexample. See the + # step below - it runs every spec, prints each one's actual TLC result in the + # job summary, and routes by tier (pass / historical / live). tla-plus: name: TLA+ Formal Verification runs-on: ubuntu-latest @@ -49,77 +39,104 @@ jobs: mkdir -p ~/.local/share/tlaplus curl -sL -o ~/.local/share/tlaplus/tla2tools.jar \ https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar - # This audit pass proves bugs exist in CURRENT code and proves correct - # fix designs for them - the fixes are NOT yet applied to the Rust code - # (see node/README.md's "Known gap" sections). These configs model the - # verified fix designs (or a baseline that was never buggy) and must - # always pass. See root README.md's "Formal verification (TLA+)" - # section for what each spec covers. - - name: Run baseline + proposed-fix specs (must pass) - working-directory: node/tla - run: | - set -e - JAR=~/.local/share/tlaplus/tla2tools.jar - java -jar "$JAR" -config GraphLifecycleCoreOnly.cfg GraphLifecycle.tla - java -jar "$JAR" -config GraphLifecycleFixed.cfg GraphLifecycle.tla - java -jar "$JAR" -config GraphLifecycleFineGrainedFixed.cfg GraphLifecycleFineGrainedFixed.tla - java -jar "$JAR" -config InstancePresignedFixed.cfg InstancePresigned.tla - java -jar "$JAR" -config Take2DisproveRace.cfg Take2DisproveRace.tla - java -jar "$JAR" -config MultiActorRace.cfg MultiActorRace.tla - java -jar "$JAR" -config InstanceBridgeOutRaceFixed.cfg InstanceBridgeOutRace.tla - java -jar "$JAR" -config MessageStateRaceFixed.cfg MessageStateRace.tla - java -jar "$JAR" -config Take1ChallengeRaceFixed.cfg Take1ChallengeRace.tla - # This job's earlier design (while all 8 findings from this round were - # still genuinely unfixed) made this step - and everything gated - # behind it - fail for as long as any bug config still reproduced its - # counterexample. As of commit 991faaa, every one of those findings - # has actually been fixed in the shipped Rust code (see - # audit/TLAPlus-20260630.md) - keeping the job permanently red past - # that point stopped being useful: these bug configs' constants are - # frozen historical snapshots (e.g. Take1ChallengeRace.tla's - # ConnectorA), not live readings of the current Rust source, so they - # can never detect a real code regression by themselves - they will - # keep reproducing the same counterexample forever regardless of - # what the Rust code does. Their only genuine ongoing signal is the - # OPPOSITE direction: if one of them ever unexpectedly STOPS - # reproducing its counterexample, that means the spec itself was - # edited into no longer demonstrating the bug it's supposed to - - # that's the one case this step still treats as a hard failure. - # Otherwise, a bug config correctly still failing is expected and - # does not fail the job - it's just printed as an informational - # reproduction pointer. - - name: Confirm known-bug specs still reproduce their counterexample + # One declarative spec table + a generic router. Each spec carries a + # `tier`: + # pass - a fix/baseline design; MUST verify clean (else a fix + # design regressed). + # historical - a bug already fixed in the code; the frozen spec MUST + # still reproduce its counterexample. An unexpected PASS + # means the spec drifted (no longer demonstrates the bug) + # or a landed fix was reverted -> hard fail. + # live - a known-unfixed bug; while its spec still reproduces the + # counterexample it is an OPEN finding that BLOCKS merge. + # To clear it: fix the code, then change its tier to + # `historical` here (the spec is frozen and cannot detect + # the code fix on its own). + # Adding any future finding is one row; that is the whole maintenance + # surface. No per-issue logic lives in the script below. + - name: TLA+ formal verification (verify fixes, reproduce fixed bugs, block live ones) working-directory: node/tla run: | + set -u JAR=~/.local/share/tlaplus/tla2tools.jar + hard_fail=0 + live_open=0 { - echo "## TLA+ audit: historical bug-reproduction specs" + echo "## TLA+ formal verification" echo - echo "These model the PRE-FIX code as a permanent historical record (all" - echo "findings below were fixed in commit 991faaa - see" - echo "\`audit/TLAPlus-20260630.md\`). Still correctly reproducing their" - echo "original counterexample below is expected and does not fail this job." + echo "Every spec is run and its live TLC result reported below. Tiers:" + echo "**pass** must verify; **historical** (fixed bug) must still reproduce" + echo "its counterexample; **live** (unfixed bug) blocks merge while it does." echo + echo "| Spec | Tier | TLC result | Status |" + echo "|---|---|---|---|" } >> "$GITHUB_STEP_SUMMARY" - while IFS='|' read -r cfg tla finding; do - [ -z "$cfg" ] && continue - if java -jar "$JAR" -config "$cfg" "$tla" | grep -q "Model checking completed. No error has been found."; then - echo "::error::$tla / $cfg was expected to keep reproducing its historical counterexample but passed instead - the spec itself was likely edited into no longer demonstrating the bug it's supposed to. If the underlying Rust fix was somehow reverted, this is also how you'd find out - either way, investigate before trusting this spec again." - exit 1 - fi + # true iff TLC reports the spec holds (no violation found) + verifies() { java -jar "$JAR" -config "$1" "$2" 2>/dev/null | grep -q "Model checking completed. No error has been found."; } + while IFS='|' read -r tier cfg tla desc; do + tier="$(echo "$tier" | tr -d '[:space:]')" + cfg="$(echo "$cfg" | tr -d '[:space:]')" + tla="$(echo "$tla" | tr -d '[:space:]')" + desc="$(echo "$desc" | sed 's/^ *//; s/ *$//')" + [ -z "$tier" ] && continue + case "$tier" in \#*) continue ;; esac repro="cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config $cfg $tla" - echo "- **$finding** - reproduce: \`$repro\`" >> "$GITHUB_STEP_SUMMARY" - done <<'BUGS' - GraphLifecycle.cfg|GraphLifecycle.tla|Finding 1: Graph.status race - GraphLifecycleFineGrained.cfg|GraphLifecycleFineGrained.tla|Finding 1b: naive guard still unsafe - InstancePresignedBug.cfg|InstancePresigned.tla|Finding 2: Instance.status regression past Presigned - InstanceBridgeOutRace.cfg|InstanceBridgeOutRace.tla|Finding 6: InstanceBridgeOutStatus resurrection - MessageStateRace.cfg|MessageStateRace.tla|Finding 7: MessageState resurrection - Take1ChallengeRace.cfg|Take1ChallengeRace.tla|Finding 9: connector_a has no margin check - BUGS + # run the check - never short-circuit; record the real outcome + if verifies "$cfg" "$tla"; then tlc="verified (no violation)"; ok=1; else tlc="counterexample found"; ok=0; fi + case "$tier" in + pass) + if [ "$ok" = 1 ]; then status="OK"; else + status="REGRESSED - fix/baseline no longer verifies"; hard_fail=$((hard_fail+1)) + echo "::error::[pass] $cfg / $tla did NOT verify ($desc). Repro: $repro" + fi ;; + historical) + if [ "$ok" = 0 ]; then status="OK - reproduces (regression record)"; else + status="DRIFT - no longer reproduces (spec edited or fix reverted)"; hard_fail=$((hard_fail+1)) + echo "::error::[historical] $cfg / $tla unexpectedly verified ($desc) - investigate drift/revert. Repro: $repro" + fi ;; + live) + if [ "$ok" = 0 ]; then + status="OPEN - blocks merge"; live_open=$((live_open+1)); hard_fail=$((hard_fail+1)) + echo "::error::OPEN BUG (blocks merge): $desc. Repro: $repro" + else + status="review - no longer reproduces; if fixed, move tier to historical" + echo "::warning::[live] $cfg / $tla no longer reproduces ($desc) - move its tier to 'historical' if the code is fixed. Repro: $repro" + fi ;; + *) status="UNKNOWN TIER"; hard_fail=$((hard_fail+1)); echo "::error::unknown tier '$tier' for $cfg (use pass|historical|live)" ;; + esac + echo "| \`$tla\` (\`$cfg\`) | $tier | $tlc | $status - $desc |" >> "$GITHUB_STEP_SUMMARY" + done <<'SPECS' + pass | GraphLifecycleCoreOnly.cfg | GraphLifecycle.tla | baseline chain-scan state machine is sound + pass | GraphLifecycleFixed.cfg | GraphLifecycle.tla | Finding 1 fix - atomic guard closes Graph.status race + pass | GraphLifecycleFineGrainedFixed.cfg | GraphLifecycleFineGrainedFixed.tla | Finding 1b fix - single-statement atomic CAS + pass | InstancePresignedFixed.cfg | InstancePresigned.tla | Finding 2 fix - Instance.status regression guarded + pass | Take2DisproveRace.cfg | Take2DisproveRace.tla | Finding 4 - Take2 vs Disprove margin holds (real shipped values) + pass | MultiActorRace.cfg | MultiActorRace.tla | Finding 5/10 - 1-of-N watchtower/verifier + operator_commit margin + pass | InstanceBridgeOutRaceFixed.cfg | InstanceBridgeOutRace.tla | Finding 6 fix - terminal-status guard closes resurrection + pass | MessageStateRaceFixed.cfg | MessageStateRace.tla | Finding 7 fix - terminal-guarded resurrect + pass | Take1ChallengeRaceFixed.cfg | Take1ChallengeRace.tla | Finding 9 fix - connector_a margin check added + pass | VerifierKickoffFailOpenFixed.cfg | VerifierKickoffFailOpen.tla | Issue #429 fix design - defer/retry mirrors committee + pass | KickoffScanCoverageFixed.cfg | KickoffScanCoverage.tla | Issue #431 fix - scan_kickoff_chain with adequate depth + historical | GraphLifecycle.cfg | GraphLifecycle.tla | Finding 1: Graph.status race (fixed 991faaa) + historical | GraphLifecycleFineGrained.cfg | GraphLifecycleFineGrained.tla | Finding 1b: naive guard still unsafe (fixed 991faaa) + historical | InstancePresignedBug.cfg | InstancePresigned.tla | Finding 2: Instance.status regression past Presigned (fixed 991faaa) + historical | InstanceBridgeOutRace.cfg | InstanceBridgeOutRace.tla | Finding 6: InstanceBridgeOutStatus resurrection (fixed 991faaa) + historical | MessageStateRace.cfg | MessageStateRace.tla | Finding 7: MessageState resurrection (fixed 991faaa) + historical | Take1ChallengeRace.cfg | Take1ChallengeRace.tla | Finding 9: connector_a has no margin check (fixed 991faaa) + historical | KickoffScanCoverage.cfg | KickoffScanCoverage.tla | Issue #431: detect_kickoff one-per-operator coverage gap (fixed by #451) + live | VerifierKickoffFailOpen.cfg | VerifierKickoffFailOpen.tla | Issue #429: verifier KickoffSent fail-open (SPV lag skips Challenge, never retried) + live | KickoffScanCoverageResidual.cfg | KickoffScanCoverage.tla | Issue #431 residual: MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 depth cap leaves deeper decoy chains uncovered + SPECS + { + echo + echo "**Result: $hard_fail check(s) failing, $live_open live bug(s) open.**" + } >> "$GITHUB_STEP_SUMMARY" + if [ "$hard_fail" -gt 0 ]; then + echo "::error::$hard_fail TLA+ check(s) failed ($live_open live bug(s) block merge). See the result table in the job summary." + exit 1 + fi fmt: name: Rustfmt - needs: tla-plus runs-on: ubuntu-latest steps: - uses: actions/checkout@v5 @@ -136,7 +153,6 @@ jobs: args: --all -- --check clippy: name: Clippy - needs: tla-plus runs-on: ubuntu-latest steps: - uses: actions/checkout@v5 @@ -155,7 +171,6 @@ jobs: cargo clippy --all-targets -- -D warnings test: name: Cargo Test - needs: tla-plus runs-on: ubuntu-latest strategy: matrix: diff --git a/node/tla/KickoffScanCoverage.cfg b/node/tla/KickoffScanCoverage.cfg new file mode 100644 index 00000000..c4382ae3 --- /dev/null +++ b/node/tla/KickoffScanCoverage.cfg @@ -0,0 +1,7 @@ +\* ORIGINAL #431 @ f2f0285e: detect_kickoff watches only the lowest-nonce +\* graph per operator (no chain walk). ScanDepth=0. Operator has 3 graphs. +\* Expected to FAIL: kicking nonce 1 or 2 escapes coverage. +CONSTANTS NumGraphs = 3 ScanDepth = 0 +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT KickoffAlwaysCovered diff --git a/node/tla/KickoffScanCoverage.tla b/node/tla/KickoffScanCoverage.tla new file mode 100644 index 00000000..3e1467ba --- /dev/null +++ b/node/tla/KickoffScanCoverage.tla @@ -0,0 +1,80 @@ +---- MODULE KickoffScanCoverage ---- +(***************************************************************************) +(* Model of GOATNetwork/bitvm-node issue #431: *) +(* "detect_kickoff watches only the lowest-nonce graph per operator, so *) +(* a kickoff on a later graph is never Challenged (unauthorized Take1)". *) +(* *) +(* THE ORIGINAL BUG (gc-v2 @ f2f0285e): detect_kickoff sourced its graphs *) +(* from fetch_on_turn_graph_by_status, which keeps ONE row per *) +(* operator_pubkey - the lowest kickoff_index still at OperatorDataPushed *) +(* (SQL: ORDER BY operator_pubkey, kickoff_index; Rust keeps the first per *) +(* operator). An operator with two posted graphs leaves nonce 0 idle and *) +(* kicks nonce >= 1; the kicked graph is never in the watched set, so no *) +(* KickoffSent / Challenge is ever created for it, and after the ConnectorA *) +(* CSV the operator Take1s with pegBTC never burned. Distinct from #429 *) +(* (there the message exists but the verifier skips it on SPV lag). *) +(* *) +(* THE FIX (commit 2bce25d, "Fix graph maintenance logic" #451, on current *) +(* dev): detect_kickoff now runs scan_kickoff_chain from each root, which *) +(* walks confirmed_prekickoff_successor forward - following each graph's *) +(* on-chain-confirmed next_prekickoff to the successor (validated *) +(* kickoff_index == prev+1) - so the idle lowest-nonce decoy no longer *) +(* hides a kicked successor. This closes the filed 2-graph attack. *) +(* *) +(* THE RESIDUAL: the walk is capped at MAX_PREKICKOFF_SUCCESSORS_PER_SCAN *) +(* = 32 (graph_maintenance_tasks.rs). The perpetually-idle root (never *) +(* kicked, so never advancing out of OperatorDataPushed) means the scan *) +(* window never slides; a chain of > 32 idle decoys with the kicked graph *) +(* beyond depth 32 is never reached on any tick. Expensive (33+ confirmed *) +(* on-chain prekickoffs, capital-locked) but structurally open. *) +(* *) +(* This spec is a COVERAGE abstraction (same static-Init idiom as *) +(* Take2DisproveRace.tla): the operator kicks graph `kicked`, keeping the *) +(* root idle; detect_kickoff covers exactly the confirmed chain reachable *) +(* from the root within ScanDepth. Property: the kicked graph is covered *) +(* (hence Challenged). ScanDepth=0 models the original no-walk selection; *) +(* ScanDepth>=NumGraphs-1 models the fix with an adequate depth budget; *) +(* 0= NumGraphs-1 = shipped fix with adequate budget (real MAX = 32) + \* 0 < d < NumGraphs-1 = depth-limit residual + +Graphs == 0 .. (NumGraphs - 1) + +\* The operator keeps the lowest-nonce graph idle as the decoy; it is the +\* single root detect_kickoff selects per operator (fetch_first_graph_per_ +\* operator_by_status). Because it is never kicked it never leaves +\* OperatorDataPushed, so the scan window never advances past it. +Root == 0 + +VARIABLE kicked \* the graph whose kickoff the operator broadcasts (no L2 initWithdraw) +vars == <> + +TypeOK == kicked \in Graphs + +\* To broadcast graph `kicked`'s kickoff the operator must have confirmed the +\* prekickoff chain Root..kicked on Bitcoin (each successor's prekickoff spends +\* the prior next_prekickoff). scan_kickoff_chain therefore CAN follow that +\* confirmed chain from Root - but only up to ScanDepth successors deep. A +\* graph g is covered (its kickoff observed -> KickoffSent -> Challenge) iff +\* the walk reaches it: it lies on the confirmed chain (g <= kicked) and within +\* the depth budget (g <= ScanDepth). +WalkedSet == { g \in Graphs : g <= kicked /\ g <= ScanDepth } + +Init == kicked \in Graphs +Next == UNCHANGED vars \* exhaustive over the Init choice of `kicked` +Spec == Init /\ [][Next]_vars + +-------------------------------------------------------------------------- +\* Safety: every unauthorized kickoff is covered by detect_kickoff (so a +\* Challenge can fire before the operator's uncontested Take1). +\* kicked \in WalkedSet <=> kicked <= ScanDepth. +KickoffAlwaysCovered == kicked \in WalkedSet + +==== diff --git a/node/tla/KickoffScanCoverageFixed.cfg b/node/tla/KickoffScanCoverageFixed.cfg new file mode 100644 index 00000000..7299a8b0 --- /dev/null +++ b/node/tla/KickoffScanCoverageFixed.cfg @@ -0,0 +1,8 @@ +\* SHIPPED FIX (commit 2bce25d / #451): scan_kickoff_chain walks confirmed +\* prekickoff successors from the root. Modeled with a depth budget covering +\* the whole chain (real cap MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32). +\* Expected to PASS: every kicked graph on the confirmed chain is covered. +CONSTANTS NumGraphs = 4 ScanDepth = 3 +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT KickoffAlwaysCovered diff --git a/node/tla/KickoffScanCoverageResidual.cfg b/node/tla/KickoffScanCoverageResidual.cfg new file mode 100644 index 00000000..47e535fe --- /dev/null +++ b/node/tla/KickoffScanCoverageResidual.cfg @@ -0,0 +1,7 @@ +\* DEPTH-LIMIT RESIDUAL: a chain of idle decoys deeper than the scan cap. +\* ScanDepth=2 with 4 graphs (real analogue: >32 decoys, kick beyond depth 32). +\* Expected to FAIL: kicking the graph beyond the depth budget still escapes. +CONSTANTS NumGraphs = 4 ScanDepth = 2 +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT KickoffAlwaysCovered diff --git a/node/tla/VerifierKickoffFailOpen.cfg b/node/tla/VerifierKickoffFailOpen.cfg new file mode 100644 index 00000000..c8f239c0 --- /dev/null +++ b/node/tla/VerifierKickoffFailOpen.cfg @@ -0,0 +1,8 @@ +\* Models the CURRENT gc-v2 code (issue #429): the verifier consumes the +\* KickoffSent message and skips the Challenge when GOAT SPV lags the kickoff +\* height, with no defer/retry - expected to FAIL (fail-open). This is a live +\* bug, not a historical artifact. +SPECIFICATION FairSpec +CHECK_DEADLOCK FALSE +INVARIANT TypeOK +INVARIANT NoUnauthorizedTake1 diff --git a/node/tla/VerifierKickoffFailOpen.tla b/node/tla/VerifierKickoffFailOpen.tla new file mode 100644 index 00000000..30bdcf9a --- /dev/null +++ b/node/tla/VerifierKickoffFailOpen.tla @@ -0,0 +1,136 @@ +---- MODULE VerifierKickoffFailOpen ---- +(***************************************************************************) +(* Model of GOATNetwork/bitvm-node issue #429: *) +(* "[Security] Verifier KickoffSent challenge is one-shot and fail-open *) +(* (unauthorized Take1)" - checked on gc-v2 @ f2f0285e. *) +(* *) +(* BRANCH STATUS: dev (gc-v2) IS the default/shipping branch and it *) +(* CONTAINS this bug - verified live at handle.rs handle_kickoff_sent_ *) +(* verifier (the goat_confirmed_btc_height SPV-lag branch returns Ok(()) *) +(* with no push_local_unhandled; should_always_challenge is never called; *) +(* detect_kickoff only scans OperatorDataPushed). The stale origin/HEAD *) +(* points at main (d74bf3c, 218 commits behind), whose older Actor:: *) +(* Challenger KickoffSent handler defers via save_unhandle_message and *) +(* calls should_challenge - i.e. main lacks this code path; it is a *) +(* gc-v2 regression that is live on the branch actually shipped. *) +(* *) +(* Threat: an operator broadcasts a kickoff with NO L2 initWithdraw (no *) +(* pegBTC burned). The automated defense is the verifier's *) +(* handle_kickoff_sent_verifier (node/src/handle.rs): if the L2 withdraw *) +(* status for the graph is None/Canceled, it must broadcast a Challenge, *) +(* forcing the operator off the uncontested Take1 fast-exit. *) +(* *) +(* THE BUG (node/src/handle.rs handle_kickoff_sent_verifier): *) +(* *) +(* if [None, Canceled].contains(&withdraw_status) { *) +(* if kickoff_height >= goat_confirmed_btc_height { *) +(* tracing::warn!(...); return Ok(()); // <-- NO defer/retry *) +(* } else { send_challenge_tx(...); } *) +(* } *) +(* *) +(* At first confirmation GOAT's SPV view lags the Bitcoin tip, so *) +(* `kickoff_height >= goat_confirmed_btc_height` is the COMMON case (and, *) +(* because the check is a strict `>` on the send side, it also skips when *) +(* SPV == kickoff_height). On that branch the handler returns Ok(()) *) +(* WITHOUT push_local_unhandled_messages_with_reason, so node/src/action.rs*) +(* marks the KickoffSent message `Processed`. Nothing re-enqueues it: *) +(* detect_kickoff (graph_maintenance_tasks.rs) only scans OperatorDataPushed*) +(* graphs, and upsert_message(is_update=false) will not recreate *) +(* `{graph_id}_KickoffSent`. So every online honest verifier processes *) +(* once, skips, and is done. After the ConnectorA CSV the operator signs *) +(* Take1 (n-of-n pre-signed on connector_0) and exits - pegBTC never *) +(* burned. handle_kickoff_sent_committee DOES defer the same SPV lag; the *) +(* verifier does not. *) +(* *) +(* This is the classic "consume-without-retry on a transient guard" fail- *) +(* open, the same shape as MessageStateRace but on the Challenge defense. *) +(* NOT #418 (the Take1/Challenge CSV margin) - per the issue, the scripts *) +(* are fine IF a Challenge is actually sent; the defect is that it is *) +(* never sent. So this spec abstracts the CSV margin as adequate and *) +(* checks only the control-flow question: does the Challenge ever fire *) +(* before the operator's uncontested Take1? *) +(***************************************************************************) + +MsgStates == {"Pending", "Processed"} + +VARIABLES + msg, \* local-queue state of the {graph_id}_KickoffSent message + spvLags, \* kickoff_height >= goat_confirmed_btc_height (GOAT SPV not strictly past the kickoff) + challengeSent, \* verifier broadcast send_challenge_tx for this unauthorized kickoff + take1 \* operator completed the uncontested Take1 (unauthorized withdrawal) + +vars == <> + +TypeOK == + /\ msg \in MsgStates + /\ spvLags \in BOOLEAN + /\ challengeSent \in BOOLEAN + /\ take1 \in BOOLEAN + +\* detect_kickoff enqueued KickoffSent to Actor::All; at first confirm GOAT +\* SPV lags the Bitcoin tip (the common case, and the == case the strict `>` +\* also skips); withdraw status for this graph is the unauthorized None. +Init == + /\ msg = "Pending" + /\ spvLags = TRUE + /\ challengeSent = FALSE + /\ take1 = FALSE + +-------------------------------------------------------------------------- +\* GOAT SPV eventually catches up to the already-confirmed kickoff (the lag +\* always closes with time). +SpvCatchesUp == + /\ spvLags + /\ spvLags' = FALSE + /\ UNCHANGED <> + +\* BUGGY handle_kickoff_sent_verifier: consumes the message either way. When +\* SPV still lags it returns Ok(()) with no defer -> Processed, NO challenge; +\* only when SPV is strictly past does it send the Challenge. +VerifierProcessBuggy == + /\ msg = "Pending" + /\ msg' = "Processed" + /\ challengeSent' = (IF spvLags THEN challengeSent ELSE TRUE) + /\ UNCHANGED <> + +\* FIXED (issue's suggested fix): on None/Canceled while SPV is not strictly +\* past the kickoff, push_local_unhandled_messages_with_reason - i.e. DEFER, +\* leaving the message Pending to be retried - so the verifier only finalises +\* the message once SPV has caught up and the Challenge is actually sent. +VerifierProcessFixed == + /\ msg = "Pending" + /\ ~spvLags + /\ msg' = "Processed" + /\ challengeSent' = TRUE + /\ UNCHANGED <> + +\* After the ConnectorA CSV the operator broadcasts Take1. It is an +\* unauthorized withdrawal only if no Challenge was ever sent (a sent +\* Challenge forces the long dispute path; per the issue the CSV margin is +\* adequate once the Challenge fires). The verifier's one-shot handling has +\* run to a final decision by the time Take1 is spendable (msg = Processed). +OperatorTake1 == + /\ msg = "Processed" + /\ ~challengeSent + /\ ~take1 + /\ take1' = TRUE + /\ UNCHANGED <> + +Next == SpvCatchesUp \/ VerifierProcessBuggy \/ OperatorTake1 +NextFixed == SpvCatchesUp \/ VerifierProcessFixed \/ OperatorTake1 + +Spec == Init /\ [][Next]_vars +FairSpec == Spec /\ WF_vars(Next) +SpecFixed == Init /\ [][NextFixed]_vars +FairSpecFixed == SpecFixed /\ WF_vars(NextFixed) + +-------------------------------------------------------------------------- +\* Safety (fail-open check): an unauthorized kickoff must never reach a +\* completed Take1 without the verifier's Challenge defense having fired. +\* Buggy: violated - process while SPV lags -> Processed, no Challenge, +\* never retried -> Take1. Fixed: holds - the message is deferred until the +\* Challenge is sent, so Take1's guard (Processed /\ ~challengeSent) is +\* never reachable. +NoUnauthorizedTake1 == take1 => challengeSent + +==== diff --git a/node/tla/VerifierKickoffFailOpenFixed.cfg b/node/tla/VerifierKickoffFailOpenFixed.cfg new file mode 100644 index 00000000..d2d7e82c --- /dev/null +++ b/node/tla/VerifierKickoffFailOpenFixed.cfg @@ -0,0 +1,7 @@ +\* The issue's suggested fix: defer (push_local_unhandled_messages_with_reason) +\* while SPV lags, so the Challenge is retried and actually sent before the +\* operator's Take1 - expected to PASS. +SPECIFICATION FairSpecFixed +CHECK_DEADLOCK FALSE +INVARIANT TypeOK +INVARIANT NoUnauthorizedTake1