PaperlayerView exact revision on arXiv

Source-linked AI summary

Exploiting The Laws of Order in Smart Contracts

Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena

arXiv:1810.11605v1cs.CR

TL;DR

Reordering smart-contract function calls can change contract outputs, raising event-ordering bugs that connect to concurrency violations. ETHRACER uses partial-order reduction and automatically inferred happens-before relations to search for them; its analysis found synchronization and linearizability violations across more than ten thousand contracts.

  • Problem

    Reordered contract function invocations can produce different outputs, and contracts can exhibit linearizability and synchronization violations.

    Source: §I · p. 2

  • Method

    ETHRACER applies partial-order reduction using automatically inferred happens-before relations, alongside dynamic symbolic execution, to reduce event-ordering analysis.

    Source: §I · p. 2, B. Our Solution · p. 5, §VIII · p. 15

  • Results

    789 (7.89%) synchronization-property violations and 47 (11%) linearizability-property violations were found among over ten thousand contracts.

    Source: §I · p. 2

  • Takeaways & Limitations

    ETHRACER provides concrete witnesses, typically 1–3 cases requiring only a few minutes per contract for human confirmation and fixing.

    Source: §I · p. 2

Abstract

from arXiv · show

We investigate a family of bugs in blockchain-based smart contracts, which we call event-ordering (or EO) bugs. These bugs are intimately related to the dynamic ordering of contract events, i.e., calls of its functions on the blockchain, and enable potential exploits of millions of USD worth of Ether. Known examples of such bugs and prior techniques to detect them have been restricted to a small number of event orderings, typicall 1 or 2. Our work provides a new formulation of this general class of EO bugs as finding concurrency properties arising in long permutations of such events. The technical challenge in detecting our formulation of EO bugs is the inherent combinatorial blowup in path and state space analysis, even for simple contracts. We propose the first use of partial-order reduction techniques, using happen-before relations extracted automatically for contracts, along with several other optimizations built on a dynamic symbolic execution technique. We build an automatic tool called ETHRACER that requires no hints from users and runs directly on Ethereum bytecode. It flags 7-11% of over ten thousand contracts analyzed in roughly 18.5 minutes per contract, providing compact event traces that human analysts can run as witnesses. These witnesses are so compact that confirmations require only a few minutes of human effort. Half of the flagged contracts have subtle EO bugs, including in ERC-20 contracts that carry hundreds of millions of dollars worth of Ether. Thus, ETHRACER is effective at detecting a subtle yet dangerous class of bugs which existing tools miss.

I. INTRODUCTION

The introduction frames event-ordering (EO) bugs as concurrency errors that arise when reordered contract events produce different outputs. ETHRACER analyzes these bugs across multiple events and finds violations in thousands of contracts while providing concrete witnesses for review.

I. INTRODUCTION

  • Earlier tools often checked only one event or a pair, while analyzing many events creates combinatorial state-space blowup.Examples include re-entrancy checks within a transaction and transaction-ordering checks over a pair of events.Source: §I · p. 1
  • An EO bug occurs when reordering a contract’s input events changes its outputs; the paper relates these violations to linearizability and synchronization properties.The authors describe asynchronous call-return interleavings and improperly enforced synchronization as examples.Source: §I · p. 2
  • ETHRACER combines symbolic execution, randomized event-sequence fuzzing, and automatically recovered happens-before relations to reduce the search over event orderings.It analyzes Ethereum bytecode directly and reports violations with concretely executable witnesses.Source: §I · p. 2
  • ETHRACER found 789 (7.89%) synchronization-property violations and 47 (11%) linearizability violations among over ten thousand contracts.The authors conclude that this formulation detects subtle EO bugs without excessively triggering alarms.Source: §I · p. 2
  • ETHRACER found all 78 true EO bugs found by OYENTE, with 674 EO bugs in total, and identified 47 linearizability violations not captured by prior work.For 95% of analyzed contracts, ETHRACER produced results in an average of 18.5 minutes per contract.Source: §I · p. 2
  • ETHRACER flags about 7–11% of analyzed contracts and typically provides only 1–3 witnesses for human confirmation, often taking a few minutes per contract.The authors report that over half of flagged contracts yielded subtle EO bugs.Source: §I · p. 2

A. Ethereum Smart Contracts

Ethereum transactions execute atomically, but miners determine their order, so contract behavior can still depend on interleavings across transactions and callbacks. The examples show how these orderings can violate linearizability or synchronization expectations.

A. Ethereum Smart Contracts

  • Ethereum transactions execute atomically, but miners choose their order, and contracts’ persistent state makes behavior dependent on the ordering of concurrent calls.The paper compares contracts to concurrent objects and describes linearizability as matching a legal sequential execution.Source: A. Ethereum Smart Contracts · pp. 2–3, B. Event-Ordering Bugs · p. 3

B. Event-Ordering Bugs

  • The Casino’s asynchronous oracle callbacks may arrive out of order, so correctly pairing each callback with its bet does not by itself guarantee linearizable behavior.The paper identifies the call-return sequences of multiple users as the relevant ordering concern.Source: B. Event-Ordering Bugs · p. 3
  • Two accepted concurrent bets can leave the Casino unable to pay a winner when both callbacks report wins; accepting a new bet should account for pending bets.The cited execution is bet1, bet2, callback1, callback2.Source: B. Event-Ordering Bugs · p. 3
  • In the IOU example, placing transferFrom between two approvals lets the spender use the original allocation and then spend another 100 tokens.The two orderings produce different remaining allowances after the same approve and transferFrom operations.Source: B. Event-Ordering Bugs · p. 4
  • Newer ERC-20 contracts address the approval race by forbidding allocation changes and requiring transferFrom calls to follow approvals.The passage describes this as a community-proposed fix that newer contracts have deployed.Source: B. Event-Ordering Bugs · p. 4

III. OVERVIEW

The overview defines event-ordering bugs as differing outputs from reordered events and explains why searching their traces is combinatorially expensive. ETHRACER uses dynamic symbolic execution to prune and prioritize multi-event testing, reporting witnesses for detected violations.

A. Problem

  • Reordering the same concrete events across valid traces constitutes an EO bug when the traces produce different outputs.The stated focus is efficient analysis that minimizes configurations requiring manual inspection before deployment.Source: A. Problem · pp. 4–5

B. Our Solution

  • Checking N events can require exploring N! permutations because different orders can change intermediate state and execution paths.A contract with 20 callable functions can yield millions of traces even for a relatively short sequence.Source: B. Our Solution · p. 5
  • ETHRACER uses happens-before relations to skip invalid event orders, since reversing such pairs results in exceptions and makes those permutations redundant.Symbolic analysis helps identify these relations across event values.Source: B. Our Solution · p. 5
  • Events that neither read nor write global state can be reordered without changing outputs, so their permutations need not be tested.Such events are also excluded from happens-before extraction.Source: B. Our Solution · p. 5
  • For asynchronous callbacks, ETHRACER prioritizes linearizable traces and flags orders that differ in output from a linearizable trace.Orders matching a linearizable trace are treated as likely benign and can be suppressed from reporting.Source: B. Our Solution · p. 5
  • ETHRACER tests traces up to length 6 in about 18.5 minutes for 95% of contracts, using dynamic symbolic execution to prune and prioritize the multi-event search.The trace length is configurable, including for longer traces.Source: B. Our Solution · p. 6

IV. ETHRACER DESIGN

The design section establishes a contract concurrency model in which atomic event executions are ordered across traces, and defines EO bugs through output differences under event permutations. Its scope is one contract’s local state and excludes reentrancy and non-local EO bugs.

A. Contract Concurrency Model & Terminology

  • An event run executes atomically: successful changes commit to the blockchain, while an exception commits none of that run’s changes.Concurrency arises from miners’ nondeterministic ordering of transactions in a proposed block.Source: A. Contract Concurrency Model &… · p. 6
  • An event is an externally triggered contract entry point with inputs; a trace is a sequence of event runs that update blockchain state consecutively.Events can originate from external transactions, internal calls, or off-chain asynchronous callbacks.Source: A. Contract Concurrency Model &… · p. 6
  • An EO bug is a pair of valid traces containing permutations of the same events that produce differing outputs.The model’s outputs include contract balance, state, and resulting transactions.Source: A. Contract Concurrency Model &… · p. 6
  • The model examines one contract’s local state and does not capture reentrancy or non-local EO effects such as paying a different beneficiary without local accounting.Other contracts’ state is not distinguished even when involved events may modify it.Source: A. Contract Concurrency Model &… · p. 6

B. The Core Algorithm

ETHRACER combines symbolic event analysis with concrete event-trace fuzzing to find reordered executions that diverge in output. It prunes traces using inferred ordering constraints and non-interfering events, then minimizes reported witness pairs.

B. The Core Algorithm

  • For each public function, symbolic execution marks inputs symbolic and collects path constraints across execution paths, over-approximating values that can drive each path.The resulting constraints are represented as SMT formulas paired with the corresponding event as a symbolic event.Source: B. The Core Algorithm · p. 7
  • SMT solving removes infeasible paths and supplies concrete inputs, global values, call targets, and transaction contexts that refine the symbolic constraints.These concretized constraints feed the later prioritization and pruning optimizations.Source: B. The Core Algorithm · p. 7
  • ETHRACER fuzzes concrete event traces by testing permutations of event pairs, triples, and longer groups, and flags traces with differing outputs.It minimizes each witness pair by removing events whose deletion leaves outputs unchanged.Source: B. The Core Algorithm · p. 7
  • Inferred happens-before relations exclude concrete event orders that would throw exceptions, potentially eliminating half of N! combinations even from a relation between two events.Generated concrete events respect the inferred relations.Source: B. The Core Algorithm · p. 7
  • Functions that neither read nor write global variables are omitted because their events cannot interfere with other events.This also reduces the amount of symbolic analysis required.Source: B. The Core Algorithm · p. 7
  • For asynchronous callbacks, the fuzzer prioritizes linearizable traces, then reorders service calls and matching callbacks independently; outputs matching a linearizable trace are not reported as bugs.Source: B. The Core Algorithm · p. 7

C. Extracting HB Relations

ETHRACER uses happens-before (HB) relations to avoid testing event orders that cannot produce valid executions. Because full HB extraction is costly, it learns a weaker pairwise relation, trading precision for fewer trace combinations.

C. Extracting HB Relations

  • Developers can impose intrinsic event order through global-variable checks that cause an exception when an event occurs in an invalid order.When only one ordering is valid, the invalid ordering need not be tested.Source: C. Extracting HB Relations · p. 8
  • HB captures required ordering: e1 happens before e2 when e1 always precedes e2 in every valid trace containing both events.Events with neither ordering relation are independent and may occur in either order.Source: C. Extracting HB Relations · p. 8
  • The full HB relation is costly to recover: even a two-event Bounty example requires checking eight event-path combinations.The example’s donate event always precedes payout in valid traces because later donations trigger an exception.Source: C. Extracting HB Relations · p. 8
  • ETHRACER learns weak HB by testing both orders of event pairs and recording a relation when one order raises an exception and the other executes normally.It focuses weak-HB analysis on pairs sharing a global variable that at least one function writes.Source: C. Extracting HB Relations · p. 8
  • Weak HB under-approximates full HB for longer traces, potentially missing EO bugs, but reduces the number of trace combinations exponentially.Other events can change state and alter ordering relations in longer traces.Source: C. Extracting HB Relations · p. 8

D. Optimizing for Linearizability Checking

ETHRACER checks asynchronous call/return traces for linearizability and filters out orderings treated as intended by EVM semantics. Its optimizer compares observed traces with outputs from linearized traces.

D. Optimizing for Linearizability Checking

  • ETHRACER suppresses orderings that follow EVM-prescribed call/return pairing because those outputs are treated as likely intended behavior.This reduces the witness pairs reported to human analysts.Source: D. Optimizing for Linearizability… · pp. 8–9
  • The optimizer targets Oraclize calls and their asynchronous callbacks, which return through a separate Ethereum transaction.Oraclize retrieves external data and later invokes the contract’s __callback function.Source: D. Optimizing for Linearizability… · p. 9
  • Linearizability requires each matching call/return pair to execute atomically, preventing out-of-order interleaving between users’ logical transactions.The optimizer uses this property to identify traces whose outputs differ from canonical linearizable executions.Source: D. Optimizing for Linearizability… · p. 9
  • ETHRACER memoizes outputs of linearizable traces as canonical, then flags a tested trace when its output matches none of them.It reports the closest linearizable trace alongside the non-linearizable witness.Source: D. Optimizing for Linearizability… · p. 9

V. IMPLEMENTATION

ETHRACER processes bytecode or an Ethereum address and uses optional Solidity source to improve report readability. Its implementation combines preprocessing with dynamic symbolic execution and path-aware handling of storage and calls.

V. IMPLEMENTATION

  • ETHRACER accepts bytecode or a deployed contract address, and optional Solidity source lets reports use function names instead of EVM signatures.For an address, it retrieves bytecode and current storage; otherwise, it assumes empty local storage.Source: §V · p. 9

A. Preprocessing

  • Preprocessing extracts function signatures from bytecode using heuristic pattern matching, or directly from supplied Solidity source compiled with solc.The bytecode heuristic inspects the beginning of the bytecode.Source: A. Preprocessing · p. 9

B. Dynamic Symbolic Execution Engine

  • The DSE engine interprets EVM instructions with symbolic inputs and concrete initial storage, collecting path constraints and checking them with Z3.The implementation supports symbolic analysis of 90% of EVM opcodes; unhandled instructions preclude analysis of some paths in 6% of analyzed contracts.Source: B. Dynamic Symbolic Execution Engine · p. 9
  • DSE generally over-approximates feasible paths and external-call behavior, while lazily concretizing values to improve path coverage.External calls are not concretely executed; their return values are symbolic, and concretization also supports symbolic mapping lookups.Source: B. Dynamic Symbolic Execution Engine · pp. 9–10
  • ETHRACER tracks global-variable reads and writes to optimize HB analysis, excluding functions that do not access shared global state.For symbolic mapping keys, it branches over observed concrete values and can add a random value when needed.Source: B. Dynamic Symbolic Execution Engine · p. 10

C. Fuzzing Event Traces

ETHRACER fuzzes subsets of events in orders allowed by discovered HB relations, compares resulting storage and balances, and minimizes bug witnesses. A separate optimizer checks Oraclize call/return traces for linearizability.

C. Fuzzing Event Traces

  • The fuzzer generates all possible subsets of collected events up to a configurable maximum size, tested at sizes two through six.Each generated trace runs on a customized EVM that avoids proof-of-work mining and network message exchange.Source: C. Fuzzing Event Traces · p. 10, D. Checking Linearizability of Event… · p. 10
  • For each event subset, ETHRACER executes traces consistent with discovered HB relations, then reports pairs whose global storage or contract balances differ.It shrinks reported pairs by removing events while preserving the EO bug, producing smaller witnesses for confirmation.Source: C. Fuzzing Event Traces · p. 10
  • ETHRACER prioritizes permutations with distinct events before permutations that reorder the same entry point with different inputs, which often change state as intended.The heuristic aims to reduce benign EO reports.Source: C. Fuzzing Event Traces · p. 10

D. Checking Linearizability of Event Traces

  • For Oraclize contracts, the linearizability optimizer considers a query-sending function and its matching __callback function.It identifies matching callbacks by the unique query identifier stored in contract state and found in blockchain calls.Source: D. Checking Linearizability of Event… · pp. 10–11
  • Figure 6 summarizes flagged-contract transaction activity by block, contract creation by block, and accumulated balances.The highest-balance 1% of flagged contracts account for more than 99% of their ether.Source: Figure 6 · p. 11

VI. EVALUATION

ETHRACER was evaluated on 10,000 synchronization-violation candidates and 423 contracts with multiple Oraclize queries for linearizability violations. It flagged violations in both groups, including contracts holding substantial Ether.

VI. EVALUATION

  • The evaluation sampled 5,000 contracts with Solidity source and 5,000 randomly selected contracts without source; the linearizability analysis covered 423 contracts with at least two Oraclize queries.Experiments ran in parallel on 30 cores, with a 150-minute per-contract timeout.Source: §VI · p. 11

A. Efficacy of ETHRACER

  • 789 of 10,000 contracts (7.89%) had synchronization violations, and 47 of 423 contracts (11%) had linearizability violations.The flagged contracts had held hundreds of millions of dollars’ worth of Ether over their lifetimes.Source: A. Efficacy of ETHRACER · p. 12
  • The flagged contracts had held up to 703,676 Ether, approximately 142.5 million USD, with a large fraction in ERC-20-based contracts.The estimate uses 203 USD per Ether.Source: A. Efficacy of ETHRACER · p. 12
  • Of the 789 synchronization-flagged contracts, 785 were live and held 307 Ether, and the group had processed 1,649,192 transactions over its lifetime.The 47 linearizability-flagged contracts had held up to 5,067 Ether; 28 were live and held 862 Ether, and the group had handled 55,946 transactions.Source: A. Efficacy of ETHRACER · p. 12

B. Manual Analysis Effort

ETHRACER’s minimized witness traces generally required only a few minutes of human review. Manual inspection found both true bugs and benign violations, including recurring patterns in linearizability cases.

B. Manual Analysis Effort

  • Flagged synchronization contracts had an average of two minimized witness pairs, with a single pair for most; every flagged linearizability contract had one pair.Analysts generally needed to inspect only a handful of trace pairs.Source: B. Manual Analysis Effort · p. 12
  • Reviewing 100 randomly selected synchronization cases and all 27 source-available linearizability cases took only a few minutes per contract to confirm or reject a suspected bug.The sample contained 52% true bugs among synchronization cases and 23 true, subtle violations among the 27 linearizability cases.Source: B. Manual Analysis Effort · p. 12
  • Among the 100 reviewed synchronization cases, 48% were considered likely benign despite differing outputs under event reordering.An ERC721 example treated owner-initiated addPermission and removePermission races as intentional and benign.Source: B. Manual Analysis Effort · p. 12
  • Two recurring linearizability bug patterns were callbacks that ignored _queryId and contracts that failed to reserve Ether for all pending player payouts.The latter pattern appeared in 21 contracts; four other flagged linearizability cases seemed benign or intentional because outputs depended on block timestamps.Source: B. Manual Analysis Effort · pp. 12–13

C. Performance

ETHRACER completed most contract analyses within 18.5 minutes on average and flagged more synchronization cases than OYENTE in a matched comparison. Its happens-before analysis reduced the event-pair search burden.

C. Performance

  • 95% of contracts took an average of 18.5 minutes to analyze, while 5% timed out after 150 minutes.About 15 minutes went to event production and 3.5 minutes to fuzzing.Source: C. Performance · p. 13
  • After four minutes of symbolic analysis to recover happens-before relations, ETHRACER found 3 pairs instead of 55 and fuzzed 2,560 traces rather than 8,652 in one minute, over 3x improvement.After fuzzing, witness minimization produced a single pair of traces to inspect.Source: C. Performance · p. 13
  • ETHRACER’s happens-before filtering removed 65% of function pairs on average, and a single happens-before relation reduced potential traces by nearly 42% on average.The average contract had nearly 5.5 happens-before relations; Figure 10 concerns the impact of the number of HB-related event pairs.Source: C. Performance · p. 13, Figure 10 · p. 14

D. Comparing ETHRACER and OYENTE

  • ETHRACER flagged 674 synchronization-violation contracts versus OYENTE’s 251 cases under the same 150-minute timeout; OYENTE does not analyze linearizability violations.Of OYENTE’s 251 cases, 78 were also flagged by ETHRACER; manual review found the remaining 173 to be false EO violations.Source: D. Comparing ETHRACER and OYENTE · p. 14

VII. RELATED AND FUTURE WORK

The paper frames event-ordering bugs using concurrency properties and presents inferred happens-before relations as a way to reduce search. It contrasts this multi-transactional scope with prior approaches and identifies unmodeled race effects as future work.

VII. RELATED AND FUTURE WORK

  • ETHRACER extends prior transaction-ordering work to longer traces and full-state differences, finding nearly four times more true EO violations than previously known bugs.The paper distinguishes this from liveness and safety checks and describes its techniques as complementary to symbolic-execution baselines.Source: §VII · p. 14
  • Unlike ECF analysis of re-entrant calls within a single transaction, ETHRACER targets multi-transaction executions and their associated combinatorial blowup.The paper reports 47 linearizability errors and 674 synchronization errors from about ten thousand contracts, none reported by Grossman et al..Source: §VII · p. 15
  • SERVOIS could confirm a known BlockKing linearizability violation, but its tailored-language requirement prevents its use for automated detection across an entire blockchain.The paper notes that existing tools for standard smart-contract vulnerability checklists do not address EO bugs.Source: §VII · p. 15
  • Ethereum lacks formally specified synchronization primitives and explicit concurrency abstractions, so the paper infers intrinsic happens-before relations rather than directly applying existing concurrency tools.The authors describe these abstractions as a basis for future work on smart-contract concurrency.Source: §VII · p. 15, §VIII · p. 15
  • The authors identify races involving transferred-fund recipient choice or EVM-event logging as effects that ETHRACER’s model could be extended to handle.They state that they plan to extend the model and implementation for these cases.Source: Future Work · p. 15

APPENDIX

The case studies show how event order can affect contest awards and escrow fees, while the ERC-20 example presents ETHRACER’s output for a buggy contract. The examples expose concrete histories and outcomes associated with EO bugs.

A. Case Studies: True positives

  • The Contest traces show that calling determineLuckyVoters before or after vote changes the voters array used for random selection, allowing the first voter to add themselves to the lucky-voter list and claim an award.The described sequences are (participate, vote, determineLuckyVoters) and (participate, determineLuckyVoters, vote).Source: A. Case Studies: True positives · p. 16
  • A buyer can call newEscrow before setEscrowFee, allowing the buyer to forfeit the escrow agent’s fee.The contract uses setEscrowFee to set an agent’s fee and newEscrow to store escrow funds.Source: A. Case Studies: True positives · p. 17

B. The Output of ETHRACER on ERC-20

  • For one buggy ERC-20 contract, ETHRACER’s output presents pairs of histories that constitute EO bugs, with events including transfer, approve, and transferFrom.The passage describes the displayed history list as the pairs that constitute EO bugs.Source: B. The Output of ETHRACER on ERC-20 · p. 17
Loading 1810.11605v1…