Reentrancy as Concurrent Interleaving

Abstract

Reentrancy vulnerabilities in smart contracts are typically described informally: a contract calls an external address, which calls back before the first invocation completes. This paper provides a formal treatment by modeling reentrancy as unsafe interleaving of execution frames over shared mutable state—precisely the same phenomenon that produces data races in concurrent programs. We define an execution model for EVM call frames, introduce happens-before relations over state operations within and across frames, and show that a contract is reentrancy-safe if and only if all feasible interleavings of its call frames are conflict-serializable with respect to storage operations. This reduction allows us to apply classical conflict graph analysis from concurrency theory to detect reentrancy statically. We extend the model to cross-function reentrancy, read-only reentrancy, and cross-contract reentrancy, showing these correspond to increasingly general forms of non-serializable schedules. We prove that reentrancy guards are isomorphic to mutual exclusion locks and that the checks-effects-interactions pattern enforces a strict partial order equivalent to two-phase locking. The framework unifies previously ad-hoc detection heuristics under a single theoretical foundation and provides correctness criteria for evaluating static analyzers.

1. Introduction

Smart contract reentrancy has caused some of the largest financial losses in blockchain history, beginning with the 2016 DAO exploit and recurring in various forms through Curve pool reentrancy in 2023. Despite extensive study, the treatment of reentrancy in the security literature remains largely pattern-based: detectors look for external calls preceding state updates, or for the absence of reentrancy guard modifiers. These heuristics work in common cases but lack formal grounding, making it difficult to reason about their completeness or to extend them to novel reentrancy patterns.

The central observation of this paper is that reentrancy is not a smart-contract-specific phenomenon. It is a concurrency bug. The EVM is single-threaded, but the CALL instruction creates a new execution frame that can modify shared state before the calling frame resumes. This is operationally identical to a context switch in a concurrent program where two threads share mutable state without synchronization. The fact that the interleaving is adversary-controlled (the callee chooses whether to re-enter) rather than scheduler-controlled does not change the structural problem.

This equivalence is not merely an analogy. We show it formally: the state operations of interleaved EVM call frames form a schedule in the sense of classical concurrency theory [Bernstein et al., 1987], and the conditions under which reentrancy causes incorrect behavior are exactly the conditions under which such a schedule is non-serializable. Detection therefore reduces to conflict graph analysis, a problem with well-understood algorithms and complexity bounds.

The paper proceeds as follows. Section 3 defines the EVM execution model at the level of abstraction needed for our analysis. Section 4 introduces the formal model: execution traces, state operations, and the happens-before relation. Section 5 defines reentrancy as non-serializable interleaving and proves the main theorem. Section 6 presents the detection algorithm. Section 7 extends the model to cross-function, read-only, and cross-contract reentrancy.

2. Preliminaries

2.1 EVM Execution Model

The Ethereum Virtual Machine executes transactions sequentially. Each transaction begins in a single execution frame (call context) associated with the target contract’s code and storage. Within a frame, execution is a deterministic sequence of opcodes operating on a stack, memory (frame-local), and storage (persistent, shared across frames of the same contract).

The opcodes relevant to our model are:

• SLOAD(s): Read the value of storage slot s. Returns value v.
• SSTORE(s, v): Write value v to storage slot s.
• CALL(addr, …): Transfer execution to address addr, creating a new child frame. The child frame can execute arbitrary code, including calling back to the original contract.

Critically, storage is committed incrementally: an SSTORE in frame F₁ is visible to a subsequently created child frame F₂, and an SSTORE in F₂ is visible to F₁ when it resumes after the CALL returns. There is no isolation between frames—they operate on the same storage with read-committed visibility.

2.2 Call Frame Nesting

A single transaction produces a tree of call frames. We denote the root frame as F₀ and child frames as F₁, F₂, …. Reentrancy occurs when a frame Fᵢ at depth d in the call tree calls an external address, which (directly or indirectly) creates a new frame Fⱼ targeting the same contract as some ancestor frame Fₖ (where k ≤ i). Frame Fⱼ then executes the contract’s code while Fₖ’s execution is suspended.

graph TD
    F0["F₀: Contract A\n(withdraw)"]
    F1["F₁: External Call\n(to attacker)"]
    F2["F₂: Contract A\n(re-entrant withdraw)"]
    F3["F₃: External Call\n(to attacker, 2nd)"]

    F0 --> F1
    F1 --> F2
    F2 --> F3

    classDef system fill:#1a3333,stroke:#5ba8a8,stroke-width:2px,color:#c0e8e8
    classDef attack fill:#331a1a,stroke:#d97777,stroke-width:2px,color:#f0c0c0

    class F0,F2 system
    class F1,F3 attack

3. Formal Model

3.1 State Operations

Let S be the set of all storage slot identifiers for a given contract. A state operation is a tuple (f, type, s, v, t) where:

• f ∈ F is the frame identifier
• type ∈ {R, W} denotes read or write
• s ∈ S is the storage slot
• v is the value read or written
• t ∈ ℕ is a global timestamp (logical clock, monotonically increasing with each operation across all frames)

We write Rf(s, t) for a read of slot s by frame f at time t, and Wf(s, v, t) for a write.

3.2 Execution Traces

An execution trace τ is a finite totally ordered sequence of state operations produced by a single transaction. The total order reflects the actual execution order across all frames (since the EVM is single-threaded at any instant).

For a frame f, we write τ|f for the subsequence of τ containing only operations from f. Note that τ|f may be non-contiguous in τ: if frame f makes an external call that triggers re-entry, the operations of the re-entrant frame are interposed.

Definition 1 (Frame projection). Given trace τ = ⟨o₁, o₂, …, oₙ⟩, the frame projection τ|f = ⟨oᵢ₁, oᵢ₂, …, oᵢₖ⟩ where each oᵢⱼ has frame identifier f and i₁ < i₂ < … < iₖ.

3.3 Happens-Before Relation

We define a happens-before relation →ₕᵦ on state operations, following Lamport [1978]:

1. Program order: If operations a and b belong to the same frame f and a precedes b in τ|f, then a →ₕᵦ b.
2. Call order: If frame f executes a CALL that creates frame g, and a is the last operation in f before the CALL, and b is the first operation in g, then a →ₕᵦ b.
3. Return order: If a is the last operation in child frame g, and b is the first operation in parent frame f after g returns, then a →ₕᵦ b.
4. Transitivity: If a →ₕᵦ b and b →ₕᵦ c, then a →ₕᵦ c.

This mirrors the happens-before relation in shared-memory concurrency [Manson et al., 2005], with CALL/return taking the role of thread fork/join.

3.4 Conflict Relation

Two operations conflict if they access the same storage slot and at least one is a write.

Definition 2 (Conflict). Operations a = (f₁, type₁, s, v₁, t₁) and b = (f₂, type₂, s, v₂, t₂) conflict iff f₁ ≠ f₂, s₁ = s₂, and type₁ = W ∨ type₂ = W.

This is the standard definition from database serializability theory [Weikum and Vossen, 2001].

3.5 Serial Trace

Definition 3 (Serial trace). A trace τ is serial if for every frame f, the operations in τ|f form a contiguous subsequence of τ. Equivalently, no operations from other frames are interposed between operations of f.

A serial trace corresponds to the execution completing each frame’s work atomically before any re-entrant frame executes.

3.6 Conflict-Serializability

Definition 4 (Conflict equivalence). Two traces τ and τ’ are conflict-equivalent if they contain the same operations and every pair of conflicting operations appears in the same relative order.

Definition 5 (Conflict-serializable). A trace τ is conflict-serializable if it is conflict-equivalent to some serial trace.

4. Reentrancy as Unsafe Interleaving

We now state the central result.

Definition 6 (Reentrant trace). A trace τ is reentrant if there exist two distinct frames f and g targeting the same contract such that τ|f and τ|g are interleaved in τ (neither is a contiguous subsequence).

Definition 7 (Reentrancy-safe). A contract C is reentrancy-safe if for every feasible reentrant trace τ involving C, the trace τ is conflict-serializable.

This definition captures the intuition precisely: reentrancy is not inherently a bug. It is only a vulnerability when the interleaving produces a state that cannot be achieved by any serial (non-interleaved) execution of the same frames.

Theorem 1. A reentrant trace τ is conflict-serializable if and only if its conflict graph is acyclic.

Proof sketch. Construct the conflict graph G(τ) where vertices are frames and there is a directed edge from fᵢ to fⱼ if there exist conflicting operations a ∈ τ|fᵢ and b ∈ τ|fⱼ with a preceding b in τ. By the serializability theorem [Bernstein et al., 1987, Theorem 3.6], τ is conflict-serializable iff G(τ) is acyclic. The proof transfers directly because our definitions of conflict and serial trace are instantiations of the general definitions for which the theorem was proved. □

4.1 The Classic Reentrancy Pattern

Consider the standard vulnerable withdrawal:

function withdraw() external {
    uint256 bal = balances[msg.sender];  // R(balances[sender])
    (bool ok, ) = msg.sender.call{value: bal}("");  // CALL
    balances[msg.sender] = 0;            // W(balances[sender])
}

In a reentrant trace where the attacker calls withdraw again from the fallback:

Time	Frame	Operation
t₁	F₀	R₀(balances[A], t₁) — reads balance
t₂	F₁	R₁(balances[A], t₂) — re-entrant read, sees stale value
t₃	F₁	W₁(balances[A], 0, t₃) — re-entrant write
t₄	F₀	W₀(balances[A], 0, t₄) — original write, overwrites

The conflict graph has edges F₀ → F₁ (R₀ at t₁ precedes W₁ at t₃) and F₁ → F₀ (R₁ at t₂ precedes W₀ at t₄). This cycle means the trace is not conflict-serializable. Neither “F₀ before F₁” nor “F₁ before F₀” produces the same final state as the interleaved execution.

graph LR
    F0["F₀"]
    F1["F₁"]
    F0 -->|"R₀(bal) < W₁(bal)"| F1
    F1 -->|"R₁(bal) < W₀(bal)"| F0

    classDef process fill:#1a2233,stroke:#7ea8d4,stroke-width:2px,color:#c0d8f0
    classDef attack fill:#331a1a,stroke:#d97777,stroke-width:2px,color:#f0c0c0

    class F0 process
    class F1 attack

4.2 Checks-Effects-Interactions as Two-Phase Locking

The checks-effects-interactions (CEI) pattern prescribes: perform all state reads and writes before making external calls. In our model, this means every frame f completes all storage operations before any child frame begins. Formally:

Proposition 1. If a contract follows CEI, then every reentrant trace is serial (and therefore trivially conflict-serializable).

Proof. Under CEI, all operations of τ|f that precede the CALL happen before all operations of the child frame, and no operations of f follow the CALL’s return (the writes have already been committed). Therefore τ|f is contiguous in τ. □

This is directly analogous to strict two-phase locking (S2PL) in database concurrency control. Under S2PL, a transaction acquires all locks before releasing any, guaranteeing serializability. CEI achieves the same effect without explicit locks: by completing all state mutations before yielding control, the frame never needs to “re-acquire” access to its state.

4.3 Reentrancy Guards as Mutual Exclusion

The nonReentrant modifier pattern uses a storage variable as a lock:

uint256 private _locked = 1;

modifier nonReentrant() {
    require(_locked == 1);
    _locked = 2;
    _;
    _locked = 1;
}

Proposition 2. A reentrancy guard is isomorphic to a binary mutex lock over the contract’s state.

Proof. The guard variable _locked has two states: unlocked (1) and locked (2). Entering the modifier performs test-and-set: read _locked, assert it equals 1, write 2. Exiting writes 1. Any re-entrant frame attempting to enter the same guarded function reads _locked = 2 and reverts. This is the semantics of mutex.lock() / mutex.unlock() where the require assertion corresponds to blocking (or, in this case, aborting). Since any re-entrant frame that would create a non-serializable interleaving is aborted, only serializable traces complete successfully. □

The correspondence is exact, including failure modes. A mutex protects a critical section; a reentrancy guard protects a guarded function body. A forgotten unlock() causes deadlock; a forgotten _locked = 1 reset permanently locks the contract.

5. Detection via Conflict Graph Analysis

5.1 Static Conflict Graph Construction

The detection problem is: given a contract’s bytecode (or source), determine whether any feasible reentrant trace has a cyclic conflict graph. We construct a static approximation.

Algorithm: STATIC-REENTRANCY-CHECK(C)
Input:  Contract C with functions F = {f₁, ..., fₙ}
Output: Set of potentially vulnerable (function, call-site) pairs

1.  For each function fᵢ ∈ F:
2.      Compute CFG(fᵢ)
3.      For each basic block B in CFG(fᵢ):
4.          Collect SLOAD operations → reads(fᵢ)
5.          Collect SSTORE operations → writes(fᵢ)
6.          Collect CALL/DELEGATECALL sites → calls(fᵢ)
7.
8.  For each function fᵢ and each call site c ∈ calls(fᵢ):
9.      Let pre_ops  = state operations reachable before c in CFG(fᵢ)
10.     Let post_ops = state operations reachable after c in CFG(fᵢ)
11.
12.     // Determine which functions could be re-entered
13.     Let reentry_targets = public functions of C reachable from c
14.
15.     For each target function g ∈ reentry_targets:
16.         Construct conflict graph G:
17.             Add edge fᵢ → g for each conflict between pre_ops and ops(g)
18.             Add edge g → fᵢ for each conflict between ops(g) and post_ops
19.
20.         If G contains a cycle:
21.             Report (fᵢ, c, g) as potentially vulnerable
22.
23. Return reported pairs

5.2 Soundness and Precision

The algorithm over-approximates: it considers all paths through the CFG, not only feasible ones. This makes it sound (no false negatives for the modeled reentrancy patterns) but incomplete (it may produce false positives for infeasible paths).

Theorem 2. If contract C has a feasible reentrant trace with a cyclic conflict graph, then Algorithm 1 reports at least one vulnerable pair.

Proof. A feasible reentrant trace implies the existence of a function fᵢ with a call site c and a re-entry target g such that conflicting operations exist both before and after c. Since the algorithm considers all reachable operations (a superset of any single feasible path), the conflicts are detected, the cycle is found, and the pair is reported. □

Precision improvements include:

• Path-sensitive analysis: Track state operations per CFG path rather than per function, reducing spurious conflicts.
• Slot resolution: Resolve storage slot identifiers statically (e.g., mapping keys) to distinguish operations on different logical variables that hash to computable slots.
• Call target resolution: Narrow reentry_targets using call target analysis rather than assuming all public functions.

5.3 Complexity

For a contract with n functions, m call sites, and k storage operations per function, the algorithm runs in O(n · m · n · k²) = O(m · n² · k²) time. For typical contracts (n < 50, m < 20, k < 30), this completes in milliseconds.

6. Extensions

6.1 Cross-Function Reentrancy

In cross-function reentrancy, the re-entrant call targets a different function of the same contract than the one currently executing. In our model, this means frames F₀ (executing function f) and F₁ (executing function g, where g ≠ f) interleave their operations on shared storage.

The conflict graph analysis handles this naturally: at line 15 of the algorithm, the reentry_targets set includes all public functions, not just the currently executing one. A cycle between f and g through shared storage slots detects cross-function reentrancy.

The classic example is a contract where withdraw() sends ETH before updating balances, and transfer() reads balances. Re-entering via transfer() reads stale balance data—a read-write conflict creating a cycle in the conflict graph between the withdraw and transfer frames.

6.2 Read-Only Reentrancy

Read-only reentrancy [SWC-107 variant] occurs when a re-entrant call reads state that is in an inconsistent intermediate state, even though the re-entrant call performs no writes to the original contract. The re-entrant frame reads a value and uses it in a different contract (e.g., a price oracle), causing harm elsewhere.

In our model, this requires extending the conflict definition. Classical conflict-serializability only considers read-write and write-write conflicts on the same data item. Read-only reentrancy involves a read-write conflict across contracts: the original contract has performed a write that is not yet complete (in the sense that later writes in the same logical operation have not occurred), and the re-entrant frame reads the intermediate value.

Definition 8 (Extended conflict). Let s be a storage slot of contract C. Operations a = Wf(s, v, t₁) and b = Rg(s, t₂) conflict in the extended sense if g executes in a different contract C’ but the value read at b is used to derive a state update in C’ that would differ under a serial execution of f.

This extended definition captures the essence of read-only reentrancy: the intermediate state is observable cross-contract, violating serializability of the composed system. Detection requires cross-contract analysis—tracking which storage slots are read by potential callees and whether those reads occur between logically coupled writes.

6.3 Cross-Contract Reentrancy and Multi-Resource Scheduling

When multiple contracts interact, reentrancy generalizes to a multi-resource scheduling problem. Each contract is a resource, and a transaction that touches contracts A, B, and C must serialize its access to all three.

This is analogous to distributed deadlock in database systems. Consider:

• Contract A calls contract B, which calls back to A (direct reentrancy)
• Contract A calls contract B, which calls contract C, which calls A (indirect reentrancy)
• Contract A calls contract B; contract B calls contract C; contract C calls A with state that A has left inconsistent (transitive reentrancy)

The conflict graph extends to a multi-resource conflict graph where vertices are (contract, frame) pairs and edges represent cross-contract conflicts. Cycle detection in this graph identifies cross-contract reentrancy, exactly as distributed deadlock detection identifies circular waits across multiple resources [Chandy et al., 1983].

graph TD
    A1["A: withdraw\n(frame F₀)"]
    B1["B: callback\n(frame F₁)"]
    C1["C: oracle read\n(frame F₂)"]
    A2["A: re-entered\n(frame F₃)"]

    A1 -->|"CALL"| B1
    B1 -->|"CALL"| C1
    C1 -->|"CALL (re-entry)"| A2

    A1 -.->|"W(slot) before CALL"| A2
    A2 -.->|"R(slot) sees stale"| A1

    classDef system fill:#1a3333,stroke:#5ba8a8,stroke-width:2px,color:#c0e8e8
    classDef attack fill:#331a1a,stroke:#d97777,stroke-width:2px,color:#f0c0c0
    classDef data fill:#332a1a,stroke:#d4b870,stroke-width:2px,color:#f0e0c0

    class A1,A2 system
    class B1 attack
    class C1 data

Static detection of cross-contract reentrancy is significantly harder than single-contract analysis because the call graph spans unknown code. Sound analysis must assume the worst case: any external call may lead to re-entry. This is the approach taken by conservative detectors and is the reason reentrancy guard adoption is widespread even when specific re-entry paths are not identified.

6.4 ERC-777 and Callback-Induced Interleaving

Certain token standards introduce implicit callbacks. ERC-777 [EIP-777] defines tokensReceived hooks that execute during token transfers. From the caller’s perspective, a simple transfer() call can trigger arbitrary callee code, creating interleaved frames that the caller’s source code does not make visible.

In our model, these implicit callbacks are additional CALL edges in the call tree. They expand the set of feasible interleavings beyond what syntactic analysis of the caller reveals. Detection must model these implicit calls—either through standard-specific knowledge (recognizing ERC-777 transfer functions as sources of callbacks) or through conservative treatment of all external calls.

7. Related Work

The connection between reentrancy and concurrency was first noted informally by Grossman et al. [2017] in the context of formalizing the EVM. Their work defines a small-step semantics for Ethereum transactions but does not develop the serializability connection.

Luu et al. [2016] identified reentrancy as one of several bug classes in their Oyente symbolic execution tool, detecting it through symbolic path exploration. Their approach is path-sensitive but does not frame the problem in concurrency-theoretic terms.

The Securify tool [Tsankov et al., 2018] uses Datalog-based analysis to check compliance and violation patterns for security properties, including reentrancy. Their “no-write-after-call” pattern is a sufficient condition for our conflict-serializability—it ensures the conflict graph has no edges from re-entrant frames back to the original frame.

Feist et al. [2019] describe Slither, a static analysis framework that detects reentrancy through a combination of taint tracking and call graph analysis. Their reentrancy detectors check for state variables read or written after external calls, which corresponds to checking for non-empty post_ops sets that conflict with potential re-entry operations in our formalization.

Albert et al. [2020] present a formal analysis based on the notion of “effectively callback free” (ECF) programs—programs whose behavior is the same whether or not callbacks are allowed. This is equivalent to our conflict-serializability condition: an ECF program is one where all feasible interleaved traces are conflict-equivalent to serial traces.

The serializability theory we build on is classical [Bernstein et al., 1987; Weikum and Vossen, 2001]. The happens-before relation follows Lamport [1978], adapted from distributed systems to EVM call frames. The analogy between reentrancy guards and mutual exclusion was noted by Sergey and Hobor [2017], who identified parallels between smart contract idioms and concurrent programming patterns.

8. References

1. E. Albert, J. Correas, P. Gordillo, G. Román-Díez, and A. Rubio. “Don’t Run on Fumes—Parametric Gas Bounds for Smart Contracts.” Journal of Systems and Software, 169, 2020.

2. P. A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.

3. K. M. Chandy, J. Misra, and L. M. Haas. “Distributed Deadlock Detection.” ACM Transactions on Computer Systems, 1(2):144–156, 1983.

4. EIP-777: Token Standard. Ethereum Improvement Proposals. https://eips.ethereum.org/EIPS/eip-777

5. J. Feist, G. Grieco, and A. Groce. “Slither: A Static Analysis Framework for Smart Contracts.” Proceedings of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), IEEE, 2019.

6. S. Grossman, I. Abraham, G. Golan-Gueta, Y. Michalevsky, N. Rinetzky, M. Sagiv, and Y. Zohar. “Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts.” Proceedings of the ACM on Programming Languages (POPL), 2(POPL):48:1–48:28, 2017.

7. L. Lamport. “Time, Clocks, and the Ordering of Events in a Distributed System.” Communications of the ACM, 21(7):558–565, 1978.

8. L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor. “Making Smart Contracts Smarter.” Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS), 254–269, 2016.

9. J. Manson, W. Pugh, and S. V. Adve. “The Java Memory Model.” Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 378–391, 2005.

10. I. Sergey and A. Hobor. “A Concurrent Perspective on Smart Contracts.” Proceedings of the 21st International Conference on Financial Cryptography and Data Security (FC), Springer, 2017.

11. SWC Registry. Smart Contract Weakness Classification. https://swcregistry.io/

12. P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Bünzli, and M. Vechev. “Securify: Practical Security Analysis of Smart Contracts.” Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS), 67–82, 2018.

13. G. Weikum and G. Vossen. Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery. Morgan Kaufmann, 2001.