Skip to main content

Exploit Demo: The "Shadow Withdrawal" Interleaving

This document demonstrates how Sector9’s TLA+ bridge can detect protocol-level exploits that traditional testing often misses. The "Visual Trace Replay" pieces below are product-facing mockups, not a shipped UI guarantee. For source-level checks, the same protocol should still use entry guards, regular contracts, and actor invariants.

1. The Vulnerable Code (Simplified Sector9-Style Pseudocode)​

In this scenario, a Treasury actor manages user funds. It follows a "Checks-Effects-Interactions" pattern, but because it is asynchronous, it has a hidden interleaving vulnerability. The snippet is intentionally simplified to show the protocol bug; production verified Sector9 code would also need caller binding, entry_requires/requires guards where appropriate, and catch-all handling around suspending awaits.

// Treasury.sr9
persistent actor Treasury {
  var balance : Nat = 1000;
  var pending_payouts : Nat = 0;

  // Protocol property checked by the model:
  // pending_payouts <= balance

  public shared({caller}) func withdraw(amount : Nat) : async () {
    // 1. CHECK: BUG - ignores already pending payouts.
    if (amount > balance) { return; };

    // 2. INTERACT: Reserve the funds and call the ledger.
    pending_payouts += amount;

    try {
      // SUSPENSION POINT: The environment can interleave here!
      await ledger.send(caller, amount);

      // 3. EFFECT: Commit the withdrawal.
      balance -= amount;
      pending_payouts -= amount;
    } catch (e) {
      pending_payouts -= amount; // Rollback reservation on failure
    }
  };
}

2. The TLA+ "Raw" Counter-example​

When Sector9 translates this to TLA+, the model checker (TLC) explores all interleavings. It finds a state where the invariant is violated. The raw output looks like this:

Error: Invariant "pending_payouts <= balance" is violated.
Trace:
1. Action: withdraw(500) started by Alice. pending_payouts = 500, balance = 1000.
2. Action: CHECKPOINT (await ledger.send). Alice is suspended.
3. Action: withdraw(600) started by Bob.
   - Evaluates: 600 > 1000? -> FALSE.
   - Evaluation Error: the check ignores Alice's pending 500, so Bob is allowed to reserve another 600.
4. Action: pending_payouts becomes 1100.
5. VIOLATION: 1100 <= 1000 is FALSE.

3. The "Visual Exploit Demo" (Proposed UI)​

Instead of the raw trace above, the "Visual Trace Replay" tool would overlay the exploit directly on the Sector9 source code as a step-by-step "Time-Travel" view.

Step 1: Alice's Request​

Highlighted Line: pending_payouts += 500; State: balance: 1000, pending: 500 Message: Alice calls withdraw(500).

Step 2: Suspension​

Highlighted Line: await ledger.send(...); UI Indicator: ⏳ Alice is now suspended. State: balance: 1000, pending: 500

Step 3: The Interleaving (The Exploit)​

Highlighted Line: if (amount > balance) { ... } UI Indicator: ⚠️ New Message: Bob calls withdraw(600). Logic Check: 600 > 1000 is FALSE, so Bob is incorrectly allowed to continue. TLA+ Finding: The protocol must check available capacity (balance - pending_payouts), not raw balance. Otherwise, concurrent in-flight withdrawals can reserve more than the treasury can pay.

Step 4: The Failure​

Highlighted Line: pending_payouts += amount; UI Indicator: ❌ CRASH: Total committed + pending (1100) exceeds Treasury capacity (1000).

4. The Value of the Demo​

For a business client (e.g., a DAO looking to store $10M), this exploit demo is useful because it ties the model-checker result back to source-level protocol behavior:

  1. Transparency: It shows exactly why the code is unsafe.
  2. Education: It teaches the developer the nuances of "Async State Drift."
  3. Assurance: Once the developer applies a fix, the model can be rerun to show that this specific counterexample is no longer reachable under the modeled assumptions.

5. The Fix (Verified)​

The "Visual Demo" would then show the fix being verified:

public shared({caller}) func withdraw(amount : Nat) : async () {
  // Atomic check against currently available capacity.
  if (amount + pending_payouts > balance) { return; };

  pending_payouts += amount;
  // ... rest of the logic
}

With this fix, TLA+ can check that pending withdrawals do not exceed the balance for the modeled Alice/Bob interleavings, while the Sector9 contract lane can separately check the local update facts that support the protocol model.