Protocol Logic & State Violations

Domain

Web3 & smart contracts

ROOTVIEL support

Partial — Core is built; parts are not yet wired end-to-end.

Analysis family

RootRaven

CWE

CWE-840, CWE-691

OWASP

SC09

A protocol-logic (or state-machine) violation is not a single mis-written line but a business rule that the contract fails to enforce: the protocol allows an operation from a state in which that operation should be impossible. The individual functions may each look correct; the defect is that the set of reachable states includes one the designers believed unreachable.

This family is deliberately a residual: when a flaw fits a more specialized family (reentrancy, access control, oracle, accounting…), that family owns it. Protocol logic & state covers the business-rule and state-transition violations that belong to no other family — especially those that only emerge from the cumulative effect of several transactions over time.

These bugs live in stateful protocols with phases, lifecycles, time locks, eligibility windows or multi-step flows: vesting and lockups, auctions, lending markets, staking with cooldowns, cross-round games, escrow and settlement.

• ▸A withdrawal permitted while funds are supposed to be locked.
• ▸A redeem accepted before a maturity timestamp.
• ▸An operation executed in an invalid phase (e.g. claiming during the commit phase).
• ▸A reward or airdrop claimed before eligibility, or claimed twice across steps.

A contract is a state machine: its storage encodes the current state, and each external function is a transition. Correctness means that for every reachable state, only the intended transitions are enabled. Solidity gives you no built-in notion of “phase” — you encode it in storage (flags, enums, timestamps, balances) and guard transitions with require statements. A missing or wrong guard silently adds an edge to the state machine.

Two properties matter: an invariant (a predicate that must hold in every reachable state, e.g. “locked funds are never withdrawable”) and a precondition (what must be true to take a transition). Logic bugs are invariant violations reachable because a precondition was too weak, in the wrong order, or absent.

The root cause is an incomplete model of reachable states: the developer reasoned about the “happy path” and a few obvious misuse cases, but the real transition graph admits a state the guards do not cover. Frequent sources: comparing the wrong variable, using < where <= was meant, checking a stale cached value, ordering checks after effects, or assuming two steps are atomic when an attacker can interleave a third.

1. 1The attacker maps the protocol’s phases and the guards on each transition.
2. 2They look for a state the designers assumed unreachable — often reached by doing steps out of the intended order, or across several transactions/blocks.
3. 3They drive the contract into that state (e.g. start a withdrawal, then trigger a lock, then complete the withdrawal).
4. 4They invoke the operation that the current state should forbid; the weak guard lets it through.
5. 5An invariant is broken — value leaves while locked, a position is claimed twice, a phase is skipped — to the attacker’s benefit.

A synthetic vesting vault that checks maturity against a value the user can influence by re-ordering calls:

synthetic — illustrates a state/precondition gap
// UNSAFE: the "locked" check and the withdrawal are separable,
// and unlockAt is read before a later lock extension applies.
mapping(address => uint256) public balance;
mapping(address => uint256) public unlockAt;
bool public paused;

function requestWithdraw() external {
    require(block.timestamp >= unlockAt[msg.sender], "locked"); // checked here
    pendingWithdraw[msg.sender] = balance[msg.sender];          // ...but acted on later
}

function completeWithdraw() external {
    // no re-check of unlockAt or paused: the earlier snapshot is trusted
    uint256 amt = pendingWithdraw[msg.sender];
    pendingWithdraw[msg.sender] = 0;
    balance[msg.sender] -= amt;
    payable(msg.sender).transfer(amt);
}

• ▸Loss of funds that should have been locked, escrowed or vested.
• ▸Double-claims or skipped phases that break the protocol’s economic assumptions.
• ▸Availability and fairness failures (acting in a phase meant for someone else).
• ▸Because the damage is cumulative, impact can be large even when each step looks benign.

Logic bugs resist pattern matching because there is no fixed “bad” shape — the rule being broken is protocol-specific. The strongest tools are those that reason about state: invariant fuzzing (Echidna/Foundry) that asserts a stated property across random multi-call sequences, property-based testing, and symbolic/bounded model checking that searches for a reachable state violating an invariant. Static analysis helps flag missing re-checks and check-after-effect ordering, but cannot know your business rules unless you state them.

An agent models the contract as a state machine, enumerates phases and the guards on each transition, and proposes candidate invariants (“locked funds are never withdrawable”, “a position is claimed at most once”). It then searches for a transaction sequence that reaches a state violating a candidate invariant — the creative, open-ended step. Crucially, a sequence that looks promising is only a hypothesis: it must be executed and the invariant must be observed to break before anything is called a Finding.

Support level

Partial — multi-transaction, time-dependent logic is among the harder frontiers; some mechanisms are proven end-to-end, others are declared but not yet operational.

The truth it decides

Whether the protocol permitted an action from a state that should forbid it.

RootRaven treats a suspected logic flaw as a lead, not a result. It synthesizes a candidate sequence of transactions, executes it on a disposable local blockchain (or a local fork of real state — never a live network), and a deterministic, AI-free verifier checks whether a declared security property was actually violated in the resulting state. AI only composes the candidate attack; it never decides truth. A sequence that does not break a stated invariant is reported as UNKNOWN within the tested scope — never as “secure”.

• ▸State the invariants explicitly, in code and in tests — the properties that must hold in every reachable state.
• ▸Re-check preconditions at the point of effect, not only at the point of request; never trust a snapshot taken in an earlier call.
• ▸Model phases with an explicit enum/state variable and a single guarded transition function, rather than scattered boolean flags.
• ▸Prefer checks-effects-interactions ordering and make irreversible steps atomic where possible.
• ▸Add invariant fuzz tests that run long, random multi-call sequences against the stated properties.

synthetic — re-check the precondition at the point of effect
function completeWithdraw() external {
    require(!paused, "paused");                               // re-checked now
    require(block.timestamp >= unlockAt[msg.sender], "locked"); // re-checked now
    uint256 amt = pendingWithdraw[msg.sender];
    pendingWithdraw[msg.sender] = 0;                          // effects before interaction
    balance[msg.sender] -= amt;
    (bool ok, ) = payable(msg.sender).call{value: amt}("");
    require(ok, "transfer failed");
}

Write the invariant as an executable property and fuzz it: a bounded search over random sequences of requestWithdraw / lock / pause / completeWithdraw should never reach a state where locked funds left the contract. Re-run the original exploit sequence and confirm it now reverts. State the result as “the invariant held across the tested sequences and budget”, never as a guarantee of correctness.

Logic correctness is undecidable in general; fuzzing and bounded checking explore a finite slice of the state space, so a clean run means “no violation found within scope”, not “no violation exists”. Deep, long-horizon or cross-protocol sequences may lie beyond the tested budget — exactly the frontier this family marks as partial.

Many specialized families are special cases of a logic violation given a dedicated verifier: reentrancy is a state broken mid-call, accounting errors break value invariants, and access-control gaps are authority-state violations. When a flaw does not fit those, it lands here. Multi-step logic flaws also overlap with signature replay and governance when the broken rule concerns authorization or voting state.