PaperlayerView exact revision on arXiv

Source-linked AI summary

Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar

arXiv:1801.04032v1cs.PL

TL;DR

Callbacks complicate modular reasoning by allowing external objects to mutate local state, as illustrated by the DAO vulnerability. The paper defines ECF, develops dynamic and static checking techniques, and evaluates online detection in Ethereum. ECF supports modular verification, while the Ethereum monitor identifies the DAO vulnerability with near-zero false positives and very small runtime overhead.

  • Problem

    Callbacks can unexpectedly mutate an object's local state, compromising modular reasoning and security in environments such as Ethereum.

  • Method

    The paper defines dynamic and static ECF, proves decidability for finite-local-state programs, and develops a polynomial online detector based on conflict analysis and commutativity.

  • Results

    The Ethereum monitor detected the DAO and other buggy executions as non-ECF, with near-zero false positives and very small runtime overhead.

  • Takeaways & Limitations

    ECF enables modular reasoning about reachable local states without analyzing other objects and can help prevent callback-based bugs in Ethereum.

  • Takeaways & Limitations

    General static ECF checking is undecidable for Turing-complete contract languages, while the paper establishes decidability for finite local states.

Abstract

from arXiv · show

Callbacks are essential in many programming environments, but drastically complicate program understanding and reasoning because they allow to mutate object's local states by external objects in unexpected fashions, thus breaking modularity. The famous DAO bug in the cryptocurrency framework Ethereum, employed callbacks to steal $150M. We define the notion of Effectively Callback Free (ECF) objects in order to allow callbacks without preventing modular reasoning. An object is ECF in a given execution trace if there exists an equivalent execution trace without callbacks to this object. An object is ECF if it is ECF in every possible execution trace. We study the decidability of dynamically checking ECF in a given execution trace and statically checking if an object is ECF. We also show that dynamically checking ECF in Ethereum is feasible and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contracts, excluding the DAO or contracts with similar known vulnerabilities, are ECF. Finally, we show that ECF, whether it is verified dynamically or statically, enables modular reasoning about objects with encapsulated state.

1 INTRODUCTION

The paper introduces Effectively Callback Free objects to preserve modular reasoning despite callbacks, and develops dynamic and static analyses for this property. It applies online detection to Ethereum, finding the DAO vulnerability while reporting low false positives and negligible overhead.

  • Motivation: Callbacks can mutate an object's encapsulated state unexpectedly, compromising modularity and contributing to the DAO theft of $150M.The DAO attack used an adversarial contract that called back to mutate the DAO's state.
  • ECF concept: ECF permits callbacks when they cannot affect an object's serial, non-interruptible behavior or local reachable states.Such objects can be analyzed independently of client environments and external object code.
  • ECF concept: A dynamically ECF execution has an equivalent callback-free execution with the same initial and final states, while static ECF requires every execution to satisfy this property.Dynamic checking is applicable to blockchain environments because static ECF is undecidable in general.
  • Modular reasoning: The paper shows that ECF objects support modular reasoning because their reachable local states can be determined without analyzing other objects.The paper demonstrates this by verifying an invariant of the DAO contract.
  • Decidability: Static ECF checking is undecidable for Turing-complete contract languages but decidable for languages with finite local states.The decidability result handles unbounded call nesting because any high-depth non-ECF execution also occurs at depth 2.
  • Online detection: The polynomial online detector, integrated into the EVM, identified the vulnerable DAO and other buggy contracts as non-ECF, with near-zero false positives and very small runtime overhead.It was retroactively run across Ethereum's available history and could have prevented the DAO exploit without invalidating legitimate executions.

2 OVERVIEW

The overview presents the DAO callback vulnerability, defines ECF as a criterion for harmless callbacks, and develops dynamic and static checking methods. It connects ECF with modular verification of contracts with encapsulated state.

  • 2.1 The DAO Bug: The DAO stores per-object credits and a balance satisfying the invariant that total credits equal the current balance.Its deposit and withdrawal methods manipulate these states.
  • 2.1 The DAO Bug: A malicious callback can reenter withdrawAll before the DAO state is safely updated, transferring GoodClient’s funds to the attacker.The attack depletes the DAO’s funds and violates its representation invariant.
  • 2.2 Effectively Callback Free Contracts: ECF permits callbacks when an equivalent callback-free execution can reproduce the object’s behavior and final state; sECF requires this for every possible execution.The definitions distinguish dynamic checking of executions from static checking of objects.
  • 2.2 Effectively Callback Free Contracts: The corrected DAO is ECF because its traces can be reordered to avoid callbacks, whereas the original DAO is not ECF.The callback-free reordering may omit calls whose effects are unnecessary for reproducing the relevant behavior.
  • 2.3 Online Detection of ECF Executions: Online ECF checking uses conflict detection and commutativity rather than enumerating exponentially many trace permutations.The algorithm was integrated into the EVM and applied to blockchain executions, with negligible reported instrumentation overhead.
  • 2.4 Deciding ECF Contracts: Static ECF checking is undecidable for Turing-complete contract languages but decidable for contracts with finite local states, even with an unbounded stack.For ECF contracts, reachable local states depend only on the contract’s code, supporting modular verification with tools such as Dafny.

3 PROGRAMMING LANGUAGE

SMAC is a simple imperative object language whose operational semantics model encapsulated contract state, private invocation locals, calls, returns, and executions as transition sequences.

  • 3.1 Syntax: SMAC contracts have unique identifiers, fields, local variables, and one nameless method composed of primitive or compound commands.Primitive commands include assignments, assertions, calls, and skips; compound commands include sequencing, conditionals, and loops.
  • 3.2 Operational Semantics: Contract state is encapsulated: each contract accesses only its own fields, while local variables belong to the current invocation.The operational semantics use a store for object fields and stack frames for activation records.
  • 3.2 Operational Semantics: State depth is the number of stack frames, allowing invocations and active versus quiescent states to be characterized operationally.An invocation’s depth is determined by the surrounding transition stack depth.
  • 3.2 Operational Semantics: A frame records an object, its remaining command, and a local environment; calls push frames and returns pop them, restoring control to the caller.A call’s return value is assigned to the caller’s designated local variable.
  • 3.3 Executions and Traces: Executions are finite, well-formed sequences of transitions whose adjacent states match, and complete executions begin and end in quiescent states.Runs concatenate complete executions in one code context; execution traces record object-command events and can be projected onto an object.

4 EXECUTION EQUIVALENCE

The paper defines two object-centered execution equivalences and supports modular reasoning by projecting executions onto one object and abstracting external calls with havoc transitions.

  • 4.1 Object-Final-State Equivalence: Final-state equivalence requires matching initial and final stores for the object and agreement on that object’s code.The surrounding code contexts may differ as long as they map the object to the same code.
  • 4.2 Object Conflict-Equivalence: Two primitive commands conflict when they access the same field and at least one access writes.Because fields are object-private, conflicting commands must have the same active object.
  • 4.3 Modular Executions: Modular well-formed executions replace external method invocations with havoc transitions assigning arbitrary return values while preserving the caller’s state structure.This safely overapproximates what the active object may observe from another object’s invocation.
  • 4.4 Projected Executions: Projection onto an object retains exactly the transitions whose active object is that object, and its event trace equals the corresponding trace projection.A proposition establishes that modular projected executions can be reversed into well-formed executions in an adjusted context.
  • 4.2 Object Conflict-Equivalence: Conflict equivalence preserves object code, trace length, event multiplicity, and the ordering of every pair of conflicting events.The correspondence between traces is expressed as a permutation that preserves conflict order.

5 CORRECTNESS CONDITIONS

ECF characterizes executions with callbacks that can be replaced by equivalent callback-free executions, using final-state or conflict equivalence; conflict ECF is stronger and supports efficient checking.

  • 5.1 Callbacks and ECF: A callback occurs when an object indirectly calls itself through another object, and an execution is callback-free when no such stack pattern occurs.ECF is defined relative to both an execution and a designated object receiving the callback.
  • 5.1 Callbacks and ECF: Dynamic final-state ECF requires a well-formed callback-free run that is final-state equivalent to the original complete execution for the object.The callback-free run serves as a witness for the execution’s dECF property.
  • 5.2 Conflict ECF: Conflict ECF requires a callback-free modular run that is conflict-equivalent to the callback-containing execution.Reordering a callback replaces its call transition with a havoc transition used to justify modular well-formedness.
  • 5.3 Relationship Between ECF Variants: Conflict ECF implies final-state ECF because conflict equivalence preserves the relevant behavior and yields a suitable callback-free witness.The implication is stated formally for every well-formed complete execution.
  • 5.4 Static ECF: Static ECF lifts the dynamic definitions from executions to objects by requiring every complete execution to satisfy the corresponding dynamic property.The paper distinguishes static final-state ECF from static conflict ECF.

6 DECIDABILITY

The paper separates undecidable dynamic final-state and general static checking from decidable finite-domain static conflict checking, using automata and a finite-state monitor.

  • 6.1 Undecidability: Static ECF is generally undecidable for Turing-complete contract languages, while single-execution conflict ECF is decidable by enumerating trace permutations.The static undecidability result applies to checking whether all executions are ECF.
  • 6.1 Undecidability: Checking dynamic final-state ECF for a single execution is undecidable, as shown by a reduction from the halting problem.The constructed contracts use a callback whose final state depends on whether an encoded Turing machine halts.
  • 6.2 Decidable Static ECF: For finite variable domains, the paper models an object with a pushdown automaton and a callback-free finite-state automaton to decide static final-state ECF.The decision procedure compares reachability between every pair of object states in the two automata.
  • 6.3 Decidable Static Conflict ECF: Static conflict ECF is decidable by reducing relevant executions to depth-two stack behaviors and checking them with a finite-state monitor.The monitor tracks depth plus read and write sets for prefixes and delayed callbacks.
  • 6.3 Decidable Static Conflict ECF: The monitor accepts exactly the depth-two executions satisfying dynamic conflict ECF and rejects the others, yielding a decision procedure for static conflict ECF.The depth-two characterization transfers the result to all executions of the original object.

7 OBJECT-LEVEL ANALYSIS

The paper uses ECF to reduce object-level verification to analysis of a callback-free most general client. Under ECF, reachable states and object assertions can be analyzed without modeling other objects' code.

  • Object-level analysis: ECF enables modular analysis of an object in isolation from other objects.The approach applies in environments with encapsulated object state.
  • Most general client: The most general client replaces calls to other objects with nondeterministic return values and repeatedly invokes the target object.Its executions are projected, callback-free executions that soundly approximate arbitrary contexts.
  • Soundness: If an object is ECF, object-level assertions can be soundly verified on its most general client.All states reachable in arbitrary code contexts are reachable in the system containing only the callback-free object.
  • Soundness: For an sECF object, the states reachable in the most general client include all states reachable in quiescent executions.Theorem 7.1 states R0 ⊃ R.
  • Runtime assumption: The analysis can assume ECF enforcement at runtime rather than proving ECF statically.This is motivated by the paper's efficient dynamic dECF verification method.

8 DYNAMIC VERIFICATION

The dynamic verifier instruments executions into object-based segments and invocations, then checks whether callback-related dependencies form cycles. An acyclic induced order certifies the projected execution as ECF.

  • Procedure: The procedure instruments executions between quiescent states and checks whether projected executions for participating objects are ECF.Instrumentation starts after leaving a quiescent state and ends upon reaching the next one.
  • Data structures: Segments summarize maximal adjacent transitions for one object with read sets, write sets, stack depth, and execution index.Executions are represented as linear sequences of these segments, from which invocations are determined.
  • Invocations and callbacks: Invocations group same-depth segments, and a callback is an invocation nested within another invocation's execution interval.The DAO example identifies the second withdrawAll invocation as a callback of the first.
  • Commutativity: The algorithm compares callback segments with caller prefixes and suffixes using read-write commutativity checks.Prefix and suffix sets partition caller segments before and after a callback; commutativity excludes conflicting reads and writes.
  • Certification: The complete algorithm computes an invocation-order conflict matrix and certifies ECF when the projected relation is acyclic.A cycle identifies invocations and callbacks that cannot be reordered.

9 EVALUATION

The Ethereum evaluation found very few non-ECF executions while imposing low runtime overhead. Detected cases largely corresponded to DAO-related, deliberately vulnerable, or erroneous contracts, with explicit scope limitations.

  • Detection accuracy: 10 executions out of about 100 million were legitimately non-ECF, and the monitor's false-positive rate was described as minuscule.The monitor was operated in detect-mode for statistics gathering.
  • Blockchain-wide detection: Less than 0.01% of executions were non-ECF in the primary blockchain experiment through March 30, 2017.The experiments checked all executions from blockchain creation through that date.
  • Non-ECF contracts: Non-ECF examples included the original DAO, related copies, an unrelated similar vulnerability, and deliberately constructed demonstrations.Contracts C6, C8, and C9 used a pattern described as inherently non-ECF, subject to a formal-definition qualification.
  • Performance: The monitor added 3.38% import-time overhead and 17% end-of-import memory overhead, while maximum memory remained 5.5GB.Monitor-off import took 16h 17m; monitor-on import took 16h 50m.
  • Non-ECF contracts: All non-ECF executions discovered in Ethereum Classic were copies of the DAO.The networks shared executions until July 20, 2016, after which the Ethereum Classic results were investigated separately.
  • Scope and limitations: The evaluation may miss other non-ECF contracts because creating and deploying exploits requires real-money investment and strong incentives.The authors identify Ethereum TestNet as a potentially more informative future setting, but did not run the experiment there.
  • Performance: The measured time overhead was about 3.5% in a RAM-disk benchmark, while an SSD-based run took about 20h.Network and disk costs were excluded from the benchmark and can vary in normal environments.

10 RELATED WORK

Related work situates ECF among modular reasoning, callback verification, and smart-contract security analyses. It contrasts ECF with existing idioms and bug classes while noting scope choices and practical analyses.

  • 10 RELATED WORK: ECF provides a sufficient condition for soundly reasoning about a single object independently of other objects.This complements prior modular call-graph and invariant-inference approaches.
  • 10 RELATED WORK: The Valid/state specification idiom tracks callback safety with a valid bit that is disabled during external calls.ECF instead relies on encapsulated state to ensure the object remains effectively valid.
  • 10 RELATED WORK: Logozzo’s approach uses abstraction to infer class invariants soundly for isolated and whole-program trace semantics, whereas ECF targets conditions for isolated verification.The paper explicitly distinguishes its goal from finding such invariants.
  • 10 RELATED WORK: ECF differs from Transaction-Ordering Dependence because non-ECF behavior can arise within one callback-containing execution, whereas TOD requires multiple client executions.The paper relates runtime ECF assertions to statically verifying similar guarded conditions.
  • 10 RELATED WORK: Oyente reported reentrancy false positives on ECF contract variations, while Why3 required whole-code analysis and user-supplied loop invariants.These examples illustrate limitations of alternative smart-contract verification approaches.
  • 10 RELATED WORK: The paper omits Ethereum exception and rollback semantics to obtain more general results and avoid extensive invocation-specific technical detail.This is an explicit scope limitation of the presentation.
  • 10 RELATED WORK: The authors manually analyzed a rock-paper-scissors contract and identified control paths where non-ECF executions could occur.The analysis found two registration paths and three additional collection paths in the reported contract.

11 CONCLUSION

The conclusion presents Effective Callback Freedom as a generic correctness condition that supports modular reasoning in local-state environments. It reports that ECF can help prevent bugs in Ethereum without drastically restricting programming style and can be checked online with low runtime overhead.

  • 11 CONCLUSION: Effective Callback Freedom is a generic correctness condition for callbacks that enables modular reasoning in environments with local-only mutable states such as Ethereum.The conclusion presents this as the paper’s central result.
  • 11 CONCLUSION: In Ethereum, ECF can help prevent bugs without drastically limiting programming style.The conclusion frames this as an application of the condition to smart contracts.
  • 11 CONCLUSION: ECF can be checked dynamically with low runtime overhead.This supports online checking in the Ethereum setting described by the paper.
Loading 1801.04032v1…