audit: use tla+ to formally verify transaction graphs#417
Open
eigmax wants to merge 31 commits into
Open
Conversation
CI's Rustfmt check was failing on the tla_model_matches_shipped_timelock_configs test added earlier - never ran cargo fmt locally since this crate can't be compiled in the dev sandbox (unrelated zkVM build dependency issue). rustfmt itself doesn't need the crate to build, only to parse, so `cargo fmt --all` applied cleanly. No logic changes.
This branch is an audit pass: node/tla/*.tla proves several real races/ boundary bugs exist in the current code, and proves correct fix designs for each - but applying those fixes to Rust is separate work the team should review and land themselves, not something to ship silently inside an audit PR. Reverted to gc-v2 (git checkout gc-v2 -- <file>, clean revert since this branch never touched these files before this session): - node/src/utils.rs (update_graph_status_guarded / set_instance_presigned_guarded atomic-CAS guards) - node/src/scheduled_tasks/event_watch_task.rs (routing through the guard) - node/src/scheduled_tasks/instance_maintenance_tasks.rs (TOCTOU fix) - crates/store/src/localdb.rs (GraphUpdate/InstanceUpdate::only_if_status_in) - crates/store/src/schema.rs (reverse-pointer doc comments) - crates/bitvm-gc/src/timelocks.rs (validate_timelock_config strictness, testnet4 connector_d 34->35) Kept as-is: every node/tla/*.tla and *.cfg file - the formal proofs are the actual audit deliverable and remain accurate regardless of whether the fix is applied yet. Updated to stop claiming the reverted fixes are shipped: - README.md's TLA+ table: "current code" -> "current code (still buggy)" for the bug configs, "proposed fix (verified, not applied)" for the fix configs. Also added the MultiActorRace.tla/.cfg row, built after the table was first written. - node/README.md: "Resolved: ..." section reverted back to "Known gap: ...", now pointing at the verified-but-unapplied fix design instead of claiming it's live. - node/tla/GraphLifecycle.md: same current-code correction. - .github/workflows/ci.yml's tla-plus job: relabeled both steps (baseline+proposed-fix vs known-bug) to match, and added MultiActorRace.cfg to the must-pass set (it didn't exist yet when the job was first written). Verified locally before pushing: all 6 must-pass configs still pass, all 3 known-bug configs still fail as expected, cargo fmt --all -- --check is clean.
Pre-existing on gc-v2, never caught before because CI never ran against gc-v2-based PRs until this branch's pull_request.branches fix. Not related to any change in this audit. - too_many_arguments on verify_real_setup: #[allow], 8 semantically distinct crypto-verification params, not a design smell worth a breaking API refactor. - needless_borrow: &package -> package (package is already &CACSetupPackage). - unnecessary_unwrap: is_none()/unwrap() -> ok_or_else(...), same behavior.
Pre-existing needless-borrow, clone-on-copy, collapsible-if, and needless-borrows-for-generic-args lints in code never touched by CI clippy until the gc-v2 PR-trigger fix. No behavior change.
…races Two new confirmed races found while sweeping every remaining stateful enum in the codebase, each with a verified counterexample and a verified (not applied) fix design: - InstanceBridgeOutStatus: three independently-scheduled writers (RPC stale-upsert, GoatChain event watcher, maintenance monitor) can resurrect a terminal Claim/Timeout/Refund back to Initialize. node/tla/InstanceBridgeOutRace.tla - MessageState: upsert_message's unconditional ON CONFLICT DO UPDATE can resurrect a Cancelled message back to Pending and re-dispatch it after its graph already closed. node/tla/MessageStateRace.tla GoatTxProcessingStatus was also audited and found safe (causal ordering via on-chain proof requirement + a processing gate), with two unrelated lower-priority defects noted for follow-up. Also cross-checked against blake-pro/bitvm-node-formal-verification, an independent Ivy-based effort targeting the same source commit - complementary rather than overlapping coverage (see report). CI's tla-plus job and root README's spec table updated to include the two new specs. audit/TLAPlus-20260630.md is the full narrative report. No Rust behavior changes - audit-only branch.
Mapped every shared/bottleneck Taproot connector in the goat crate's peg-out transaction graph (not just ConnectorD, the original scope), looking for the same margin-race shape Finding 4 found there. - Finding 9 (new bug): ConnectorA (Take1 vs Challenge) has NO margin check anywhere in validate_timelock_config, unlike every other timelock field. Real shipped Regtest value gives a challenger exactly zero reaction margin - same coin-flip-boundary shape as the original ConnectorD/testnet4 finding. node/tla/Take1ChallengeRace.tla (+ Fixed.cfg design, verified) - Finding 10 (verification, not a bug): ConnectorF leaf 1 has two alternative "committee blocks Take2" spenders (Nack and CommitTimeout), but MultiActorRace.tla only proved the margin for one (Nack). Extended it with operator_commit's margin against ConnectorF using real shipped values - holds on all 4 networks, closing a verification-coverage gap (the Rust ensure_lt check was previously unverified at the TLA+ level). - ConnectorZ and AckConnector's un-covered leaves reviewed and found to have no CSV-margin structure to check (documented reasoning, no forced/artificial model). - Take2DisproveRace.tla's header updated to acknowledge ConnectorD's third leaf (PubinDisprove) - zero CSV, can't be slower than the already-proven-safe Disprove path, so no new model needed, but the header no longer implies it doesn't exist. CI's tla-plus job and root README's spec table updated. No Rust behavior changes - audit-only branch.
Tie Finding 4's connector_a observation forward to Finding 9 (same
gap, discovered in two passes) instead of leaving it as a redundant,
disconnected aside. Fix two positional counts ("seven"/"three of the
seven") that went stale once Finding 9/10 were added after them.
tla-plus is the fastest job (seconds, no Rust toolchain build) and a failure there means either a real regression or a stale/broken spec - not worth burning 30+ minutes of Cargo Test/Clippy compute before finding out. Reordered it to the top of the file since it now gates everything else via needs:.
…elocks.tla Extract the two literal value-table duplications found across node/tla/: - AllStatuses/TerminalStatuses/AllowedTransitions (the real Graph.status state machine) was byte-identical across GraphLifecycle.tla, GraphLifecycleFineGrained.tla, and GraphLifecycleFineGrainedFixed.tla. - Networks/ProverConnector/ConnectorD/ConnectorF/MinReactionBlocks (and more) was byte-identical between Take2DisproveRace.tla and MultiActorRace.tla, with MinReactionBlocks also duplicated a third time in Take1ChallengeRace.tla. Both are now single-source-of-truth modules the relevant specs EXTEND, removing a real drift risk (already caught one: MultiActorRace.tla's comment said "shipped values" without noting ConnectorD is actually the post-fix value, inconsistent with Take2DisproveRace.tla's more careful "(post-fix)" annotation on the identical table). Also removed `EXTENDS FiniteSets` from 5 files that never used Cardinality/IsFiniteSet - dead imports. Net: 1033 -> 1000 lines despite adding 2 new files. Every one of the 15 spec+config combinations re-verified via TLC to behave identically to before (same pass/fail outcome, same state counts - e.g. GraphLifecycleFineGrainedFixed.cfg still finds exactly 132 states, matching the audit report's existing claim). No .cfg files touched; CI's working-directory: node/tla resolves the new EXTENDS targets the same way it already resolves everything else. Also strengthens Finding 8 with direct confirmation against the L2 Gateway.sol contract (KSlashh/bitvm-L2-contracts@2173b92, gc-v2): proceedWithdraw requires a Merkle-proven kickoff tx and is onlyCommittee-gated; finishWithdrawDisproved has its own on-chain AlreadyDisproved guard - confirming this report's races are about the local node's bookkeeping drifting from a well-guarded on-chain source of truth, not the L2 contract itself being unsafe.
Previously the "known-bug specs must still fail" step only failed CI if a bug config unexpectedly started passing (spec/code drift). That meant CI showed green despite 6 TLC-proven, unfixed findings still being present in the shipped code - a clean-looking pipeline hiding real, documented gaps. Now the step fails whenever ANY bug config correctly reproduces its finding (the normal, expected case right now), in addition to the original harder failure if one unexpectedly passes. Since fmt/clippy/ test are gated behind tla-plus, this intentionally keeps the whole pipeline red until each finding's verified fix design is actually applied to the Rust code - moving a bug config to the must-pass list (and its Fixed.cfg out of hiding) is how a fix "turns CI green" again. Verified the exact YAML-parsed script (heredoc dedenting etc.) end to end locally before pushing: correctly identifies all 6 open findings and exits 1. Updated the job's top comment and root README to explain this is expected, not broken.
Companion to audit/TLAPlus-20260630.md, per request to generate fix suggestions without reversing this branch's audit-only stance. For each of the 6 CI-gated findings (1/1b, 2, 6, 7, 9) plus Finding 4: exact current code (verified against the real source, not from memory), exact suggested change, and why it implements the property the corresponding TLA+ spec proved. Cross-checked every referenced API against the real codebase before writing it down: - GraphStatus doesn't derive EnumIter, so the Finding 1/2 guard's allow-list is hardcoded from GraphTopology.tla's AllStatuses minus TerminalStatuses instead of a speculative .iter() call. - QueryBuilder::and_where_in already exists (crates/store/src/ utils.rs:77-92) and does exactly what the guard needs - used that instead of hand-rolling placeholder-building SQL. - InstanceUpdate is missing all 5 fields Finding 6b's fix needs (bridge_out_amount/goat_tx_hash/goat_tx_height/user_change_addr/ user_refund_addr) - called that out explicitly rather than waving it away as "add whichever are missing". No Rust source files changed.
…itted doc Remove audit/fix-implementation-guide.md - per feedback, this branch stays audit-only with no extra committed artifacts; the fix guidance belongs in CI output, not a standalone file. The "Fail while documented bugs remain unfixed" step now carries a one-line fix direction + affected files per finding directly in its own script (cfg|tla|finding|files|hint rows) and, for each still-open finding, writes a formatted section to $GITHUB_STEP_SUMMARY (rendered as markdown on the run's summary page) in addition to the existing ::warning:: annotations - so anyone looking at a failed run sees exactly what to fix and where, without needing a separate file. Verified the exact YAML-parsed script end to end locally (including simulating $GITHUB_STEP_SUMMARY) before pushing.
Follow-up to 29ef86a, which deleted audit/fix-implementation-guide.md but the actual CI script change didn't get staged in that commit (pathspec typo aborted the git add). This is that missing change. The "Fail while documented bugs remain unfixed" step now carries a one-line fix direction + affected files per finding in its own script (cfg|tla|finding|files|hint rows) and writes a formatted section to $GITHUB_STEP_SUMMARY per still-open finding, in addition to the existing ::warning:: annotations.
The condensed per-finding hints weren't enough - print the full write-up (exact current code, exact suggested change, and why it implements the property the TLA+ spec proved, per finding) verbatim to both the raw log and $GITHUB_STEP_SUMMARY whenever any bug remains open. Content is the same detail level as the now-removed audit/fix-implementation-guide.md, just generated inline in the CI script instead of living as a separate committed file. The bug-detection loop is back to simple 3-field records (cfg/tla/ finding) since the fix text is no longer threaded through it - the full report is one static heredoc block printed once, not per-finding interpolation. Verified the exact YAML-parsed script end to end locally: correct exit code, full 298-line report written to both stdout and a simulated GITHUB_STEP_SUMMARY, byte-identical head and tail spot checks against the source content.
* Use JSON for graph params hash * add verifier challenge tool * update log * fix tx-size-too-small * fix instance status transition * fix pegin queue * add sqlx cache * update timelocks * fix graph status transition * fix tla 3,6,7,9 * fix clippy --------- Co-authored-by: ethan <kslashhh@gmail.com>
Replace the embedded 295-line fix-suggestions report with generic reproduction instructions: for each open finding, the exact TLC command to reproduce its counterexample locally, plus a pointer to audit/TLAPlus-20260630.md for the verified fix design. The fix content lives in one place (the report) instead of being duplicated in ci.yml where it would drift out of sync. Note: an earlier attempt at this edit used a fragile line-boundary search that matched the wrong closing `fi` and left corrupted duplicate content in the file. Caught before pushing, reset to the last-known-good commit, and redid the edit with exact asserted line boundaries. Verified the final YAML-parsed script end to end locally (correct exit code, clean warnings + step summary, no leftover content) before this commit.
The repro string printed a bare `tla2tools.jar`, which only resolves if the jar happens to be in the caller's current directory - not where the setup instructions (root README.md) actually put it. Reported by the user copy-pasting a printed command and hitting "Unable to access jarfile". Fixed to the real path, ~/.local/share/tlaplus/tla2tools.jar, matching every other invocation in this workflow and the README. Verified the corrected command actually runs locally before pushing.
…1faaa Every finding this audit formally proved (1, 1b, 2, 3, 4, 6, 7, 9) now has a "What actually shipped" note describing the real applied fix, verified against the actual diff (not the commit message) and, for the two timelock findings, re-checked with TLC using the real new shipped numbers. In several cases the shipped fix goes further than what this audit proposed (per-writer-source transition tables for Finding 1, extra idempotency/collision guards for Finding 6). Finding 8's two adjacent non-race defects were specifically checked and remain unfixed - called out explicitly rather than assumed. node/tla/ShippedTimelocks.tla updated to the real new Testnet4 values (connector_d 35->40, prover_connector 22->20, and others) - re-run through TLC, all properties still hold. Take1ChallengeRace.tla's ConnectorA deliberately left at its historical pre-fix value (a permanent regression-check record); header comments updated to explain this on both files. README.md's spec table reframed: "current code"/"proposed fix" -> "pre-fix code (historical)"/"fix design (applied in 991faaa)". No ci.yml changes - the must-pass/must-fail lists already correctly reflect this state (bug configs still fail against their unchanged historical constants, fix configs still pass against the real current numbers), consistent with CI being designed to keep the bug-reproduction configs as permanent regression checks.
… bugs The "fail while documented bugs remain unfixed" step was designed before commit 991faaa fixed all 8 findings; keeping it failing afterward served no regression-detection purpose (the bug configs' constants are frozen snapshots that never read the real Rust source) while permanently blocking CI. Only an unexpected PASS (a bug config no longer reproducing its counterexample) is a genuine drift signal now, so that's the only case that still fails the job - a config correctly still failing its historical counterexample is now just an informational note in the step summary.
Keeps the report focused on this audit's own findings; the comparison against the separate blake-pro/bitvm-node-formal-verification project was tangential to the report's purpose.
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
2 participants
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.
No description provided.