PaperlayerView exact revision on arXiv

Source-linked AI summary

A Concurrent Perspective on Smart Contracts

Ilya Sergey, Aquinas Hobor

arXiv:1702.05511v1cs.DC

TL;DR

Transaction ordering and cross-contract calls can make smart-contract behavior resemble shared-memory concurrency. The paper uses that analogy and two deployed Ethereum examples to examine concurrency-like bugs and their implications for reasoning about contracts.

  • Problem

    Multi-transaction and cross-contract behavior can violate safety properties that cannot be stated using only a contract’s implementation and local state.

    Source: §1 · pp. 1–2

  • Method

    The paper models accounts as threads and smart contracts as concurrent objects, then examines two deployed Ethereum contracts as examples of concurrency-like behavior.

    Source: §2 · p. 3

  • Results

    BlockKing callbacks let the last contestant gain multiple chances, while DAO reentrancy enabled repeated withdrawals before the account was zeroed.

    Source: §2.1 · p. 4, §2.2 · p. 6

  • Takeaways & Limitations

    The analogy offers perspectives and existing tools for understanding, debugging, and verifying contract behavior, but should not be taken verbatim.

    Source: §7 · p. 13

    The presented synchronization solution is monolithic, combining counter functionality with a lock, and extracted locking protocols complicate isolated invariant verification.

    Source: §4 · p. 10, §5.1 · p. 11

Abstract

from arXiv · show

In this paper, we explore remarkable similarities between multi-transactional behaviors of smart contracts in cryptocurrencies such as Ethereum and classical problems of shared-memory concurrency. We examine two real-world examples from the Ethereum blockchain and analyzing how they are vulnerable to bugs that are closely reminiscent to those that often occur in traditional concurrent programs. We then elaborate on the relation between observable contract behaviors and well-studied concurrency topics, such as atomicity, interference, synchronization, and resource ownership. The described contracts-as-concurrent-objects analogy provides deeper understanding of potential threats for smart contracts, indicate better engineering practices, and enable applications of existing state-of-the-art formal verification techniques.

1 Introduction

Transaction ordering and calls across contract boundaries create observable concurrency-like behavior, even though blockchain computations are deterministic. The paper frames contracts as concurrent objects to clarify these behaviors and motivate applying concurrency reasoning and verification methods.

1 Introduction

  • Transaction races arise because block transaction order is not fixed at execution time, making outcomes depend on ordering and allowing adversarial parties to exploit nondeterminism.The paper notes that this makes contract behavior subtle in ways reminiscent of conventional concurrent programming.Source: §1 · pp. 1–2
  • Contract executions can span transactions within or across blocks, creating safety violations that cannot be expressed using only implementation and local-state verification.The paper contrasts these behaviors with existing methodologies focused on a contract’s implementation and local state.Source: §1 · p. 2
  • The paper models accounts as threads and smart contracts as concurrent objects, which hold mutable state and manage shared resources.The analogy treats contracts as objects invoked by users or other contracts rather than objects residing in shared memory.Source: §1 · p. 2
  • Calls to other contracts act like cooperative multitasking: a called contract can modify the caller’s state before returning, as in the DAO bug.The callee’s code may be unanticipated by the caller’s designer.Source: §1 · p. 3
  • The analogy aims to characterize contract concurrency issues using established abstractions and apply existing formal methods to reason about or detect good and bad behaviors.The paper draws on frameworks developed for concurrent and distributed programming.Source: §1 · p. 3

2 Deployed Examples of Concurrentesque Behavior

Two deployed Ethereum contracts illustrate distinct concurrent-type behaviors: BlockKing’s asynchronous Oraclize callback and the DAO’s reentrant withdrawal. Their bugs arise when contract state changes across calls or before it is cleared.

2.2 The DAO contract

  • Approximately 3.6 million Ether (then about USD 50 million) was lost in the DAO attack, whose recipient reentered before its balance was cleared.The DAO had more than 18,000 investors and at its height attracted more than 14% of Ether then in existence.Source: §2 · p. 4, §2.2 · pp. 5–6

2.1 The BlockKing contract

  • When gamblers entered before callbacks returned, shared warrior fields were overwritten, giving the final contestant repeated chances to match the random number.Oraclize callbacks could arrive after several blocks, during which the blockchain and contract state could change.Source: §2.1 · pp. 4–5

2.2 The DAO contract

  • The DAO bug is framed not only as recursion or reentrancy, but as sequential code running in a concurrent environment.Source: §2.2 · p. 6

3 Interference and Synchronization

The section uses shared-memory and blockchain counters to show how weak atomicity lets interleavings defeat client assumptions, then considers synchronization remedies and formal trace analysis.

3.1 Atomic updates in shared-memory concurrency

  • Interleaved thread operations can invalidate a client’s assertion and overwrite an earlier counter update, despite the counter itself being thread-safe.The client assumes its increment steps will not be interrupted by another thread.Source: §3.1 · pp. 6–7

3.2 Atomic updates in concurrent blockchain transactions

  • Separate get and set transactions can interfere when parties try to increment the same contract balance, making set’s result unpredictable from local observations.A client may query externally, then submit a separate update; limited gas also makes multi-contract calls in one transaction ill-advised.Source: §3.2 · p. 8
  • A testAndSet operation supplies check-and-update synchronization for atomic increments, unlike a counter limited to get and set.The paper relates testAndSet to compare-and-swap and notes that its consensus number is infinite.Source: §3.2 · pp. 8–9
  • Existing runtime concurrency-verification tools could analyze translated contracts’ traces to detect violations of atomicity assumptions and missing synchronization.The proposed route translates a contract into a corresponding shared-memory concurrent object.Source: §3.2 · p. 9

4 State Ownership and Permission Accounting

The section applies ownership and permission accounting to restrict interference, using exclusive ownership or a Read/Write lock to control contract access.

State ownership

  • Exclusive ownership limits access to a dedicated owner, justifying that party’s local assumptions about the contract’s state.The example uses a byOwner modifier to restrict get and set to the contract owner.Source: §4 · pp. 9–10

Permission accounting

  • A Read/Write lock tracks active readers and writers so readers can coexist when no writer is active, while write access is governed by separate permissions.Callers acquire the relevant permission before an operation and release it afterward.Source: §4 · p. 10
  • Combining counter functionality and locking in one contract makes the solution monolithic, while permission formalisms can verify that a Read/Write lock prohibits concurrent write modifications.The paper identifies modularity as the drawback and cites a formal permissions model for proving the lock safe.Source: §4 · p. 10

5 Discussion

The discussion weighs modular contract composition against verification complexity and highlights liveness concerns that arise when locks are introduced.

5.1 Composing the contracts

  • Factoring lock logic into a separate contract makes invariant proofs depend on external protocol properties, such as uniqueness of a writer.The locking pattern’s contract-local implementation is non-modular, while extracted locks require reasoning about interactions with other rigorously specified contracts.Source: §5.1 · p. 11
  • Protocol-based abstractions that hide implementation details suggest a possible route to modular verification of mutually dependent, higher-order contract interactions.The paper proposes leveraging its analogy to develop such a verification method.Source: §5.1 · p. 11

5.2 Liveness properties

  • A reader that never releases its lock can block future state changes, so liveness reasoning depends on an assumption of scheduler fairness.The paper frames fairness as the assumption that makes progress reasoning possible.Source: §5.2 · p. 11

6 Related Work

The related work contrasts existing low-level contract verification with higher-level reasoning about behavior and communication, connecting concurrency abstractions to global contract properties.

6.1 Verifying contract implementations

  • Existing Solidity verification approaches cover safety properties such as invariant preservation, while the cited methods translate Solidity, EVM bytecode, or EVM semantics into verification frameworks.The paper characterizes these approaches as focused predominantly on low-level safety properties and invariant preservation.Source: §6.1 · p. 12
  • Communicating state-transition systems are proposed for proving trace and liveness properties, with refinement needed to connect the abstract system to contract code.More complex systems may be needed for contracts with preemptive concurrency.Source: §6.1 · pp. 12–13

6.2 Reasoning about global contract properties

  • The paper generalizes transaction-ordering dependency as unrestricted interference and contrasts a blockchain-supported read-modify-write primitive with a locking proxy that must be anticipated at deployment.The primitive avoids modifying deployed contracts but requires users to upgrade client applications.Source: §6.2 · p. 13

7 Conclusion

The conclusion presents the concurrent-object analogy as useful but bounded. It raises open questions about adapting concurrency concepts to multi-contract behavior and blockchain scheduling.

7 Conclusion

  • The analogy may help explain, debug, and verify contract behavior, but gas-bounded execution and fund management lack direct concurrency counterparts.The authors caution that the analogy should not be taken verbatim.Source: §7 · p. 13
  • The conclusion asks whether insufficient caution around the ABA problem could threaten state integrity in a multi-contract setting.This is presented as an open speculation, not an established smart-contract vulnerability.Source: §7 · p. 13
  • The authors speculate that the mining protocol sets transaction-scheduling priorities and ask whether thread-management insights could improve ledger implementations.They frame this as a question, not a demonstrated application.Source: §7 · p. 14
  • The conclusion asks whether an equivalent consistency notion to linearizability could specify composite contracts’ multi-transactional operations, such as BlockKing.Linearizability is described as a standard correctness notion for high-level behavior of lock-free objects.Source: §7 · p. 14
Loading 1702.05511v1…