PaperlayerView exact revision on arXiv

Source-linked AI summary

eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts

Clara Schneidewind, Ilya Grishchenko, Markus Scherer, Matteo Maffei

arXiv:2005.06227v1cs.PLcs.CR

TL;DR

Smart-contract vulnerabilities are difficult to analyze because deployed code is immutable, EVM bytecode exposes little static information, and runtime interactions with other contracts are often unknown. eThor addresses this with a Horn-clause abstraction of EVM semantics and provides a sound automated static analysis evaluated on real-world contracts.

  • Problem

    Smart-contract security analysis matters because vulnerabilities can cause catastrophic financial consequences and deployed blockchain code cannot be fixed, while Solidity semantics, low-level EVM bytecode, and unknown runtime interactions make analysis difficult.

  • Method

    eThor abstracts EVM bytecode semantics with Horn clauses and expresses security and functional properties as reachability queries, using a staged analysis for control-flow reconstruction and precise property analysis.

  • Results

    eThor is presented as the first automated tool implementing a sound static analysis technique for EVM bytecode and was evaluated against the official Ethereum test suite and real-world contracts.

  • Takeaways & Limitations

    The approach provides a principled basis for reasoning about arbitrary contract executions while supporting security and contract-specific functional properties through reachability analysis.

  • Takeaways & Limitations

    The stated soundness theorem applies only to contracts whose code does not contain DELEGATECALL or CALLCODE, while unknown and dynamically accessed contract behavior remains challenging to over-approximate.

Abstract

from arXiv · show

Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode and an experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 95% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.

1 INTRODUCTION

Ethereum smart contracts are valuable but difficult to analyze reliably because vulnerabilities can be catastrophic and immutable, while Solidity, EVM bytecode, dynamic control flow, and unknown blockchain data complicate sound verification. eThor addresses this gap with a principled, sound static-analysis approach for EVM bytecode.

  • Motivation: Smart-contract vulnerabilities can cause catastrophic financial losses, and deployed blockchain code cannot be fixed.The paper cites the DAO hack as a $60M loss and notes that smart-contract bugs recur.
  • Challenges: Sound analysis is difficult because Solidity has non-standard semantics, EVM bytecode exposes little static information, and runtime blockchain data is often unknown.The challenge includes reasoning about callers, callees, and other environment inputs that are unavailable statically.
  • State of the art: Existing smart-contract analyzers divide mainly between interactive machine-checked proof frameworks and automated heuristic bug-finding tools.Intermediate approaches claim automated soundness, but the paper reports that they fail to provide the intended guarantees.
  • Design goal: Sound analysis must combine provable over-approximation with abstractions that remain efficiently encodable and precise enough to assess contract safety.The paper identifies this balance as a central practicality challenge for automated analysis.
  • State of the art: Prior tools face weaknesses in formal semantics, security-property definitions, control-flow reconstruction, benchmarking, and ground-truth validation.The paper reports unsoundness findings and unreliable or incomparable evaluation datasets in prior work.
  • Contribution: The paper introduces eThor as a sound, performant EVM-bytecode analyzer based on Horn-clause reachability analysis and formalized EVM semantics.Its contributions include proving soundness, supporting security and functional properties, implementing HoRSt and eThor, and evaluating real-world contracts.

2 ETHEREUM

Ethereum is a transaction-based state machine whose contract executions run as EVM bytecode over account state, stack-machine state, memory, storage, gas, and nested call contexts. Its small-step semantics models local instructions and transaction-initiating instructions, whose dynamic environments make analysis challenging.

  • Ethereum background: Ethereum transactions alter a global state of externally owned and contract accounts containing balances, storage, and code.Contract execution is governed by the EVM, with gas limiting the otherwise quasi Turing-complete computation.
  • EVM bytecode: Contracts are published as stack-based EVM bytecode containing operations for computation, control flow, memory, storage, and internal transactions.Each instruction has a potentially environment-dependent gas cost, and exceeding the gas limit causes exceptional halting and reversion.
  • Formal semantics: The EVM bytecode semantics is a small-step relation over callstacks under a transaction environment.The transaction environment summarizes static transaction information such as block data, gas price, and gas limit.
  • Callstacks: A callstack contains regular execution states or terminal HALT and EXC states representing pending or terminated internal transactions.Regular states track the machine, execution environment, global state, and transaction effects.
  • Machine state: The local machine state records gas, program counter, memory, active memory size, and stack, with each new internal transaction starting from a fresh machine state.Local instructions update this state, as illustrated by ADD consuming two stack values, advancing the program counter, and subtracting gas.
  • Internal transactions: CALL, CALLCODE, DELEGATECALL, and CREATE dynamically modify execution environments across calls and may invoke code unavailable at analysis time.These instructions are difficult to analyze because their arguments and cross-call environments must be tracked precisely.

3 STATIC ANALYSIS OF EVM BYTECODE

eThor abstracts EVM executions with contract-specific constrained Horn clauses and uses sound reachability reasoning to analyze security and functional properties. Its abstraction over-approximates executions while modeling unknown environments, reentrancies, storage, memory, and selected instruction behaviors.

  • Analysis approach: eThor formulates a Horn-clause abstraction of contract executions and reasons about an abstracted property instead of concrete small-step executions.Soundness follows when every concrete execution is modeled by an abstract execution and the abstract property over-approximates the target property.
  • Analysis approach: The abstraction translates concrete configurations into ordered sets of predicate applications over abstract domains.Abstract configurations represent one or several concrete configurations, with precision induced by the lifted order on arguments, predicates, and configurations.
  • Main abstractions: Unknown blockchain state and external-contract behavior are over-approximated because the execution environment and interacting contracts are not statically known.This introduces many unknown environment inputs, while external contracts may interact with the analyzed contract in multitudinous ways.
  • Main abstractions: The analysis abstracts gas, byte-indexed memory, and the callstack, including a two-level distinction between original execution and reentrancies.Memory is represented as a word array, and callstack abstraction reflects uncertainty about the initiator and prior internal transactions.
  • Abstract semantics: The instruction abstraction maps each contract instruction to Horn clauses that over-approximate its execution semantics, including specialized handling of CALL.CALL models call parameters, return values, memory effects, and persistent storage after successful calls.
  • Soundness and properties: Every concrete execution satisfying the theorem’s contract and environment conditions can be mimicked by an abstract execution derived through the Horn clauses.The soundness theorem applies to contracts whose code excludes DELEGATECALL and CALLCODE.
  • Soundness and properties: Reachability analysis is sufficient to express relevant smart-contract security properties, while fixed-point SMT engines can support automated pre- and postcondition checking with loops.The paper specifically identifies single-entrancy validation and contract-specific functional properties as supported uses.

4 HORST: A STATIC ANALYSIS LANGUAGE

HoRSt is a high-level language and compiler framework for specifying Horn-clause abstractions and producing optimized SMT encodings. It combines readable specifications with transformations intended to improve solver performance while avoiding clause blow-ups.

  • Framework: HoRSt provides a high-level specification language for Horn-clause abstractions and a compiler that generates optimized smt-lib encodings for SMT solvers.The framework is designed to support principled and robust static-analyzer development.
  • Specification language: HoRSt specifications use algebraic data types, pattern matching, bounded iteration, user-defined predicates, and parameterized Horn clauses.A Java back-end supplies domain-specific infrastructure such as contract parsing and contract-specific program-counter sets.
  • Compilation pipeline: The HoRSt compiler resolves high-level constructs, optionally applies optimizations and transformations, and emits standardized smt-lib output.The resulting clauses are restricted to a fragment supported by z3.
  • Optimizations: Predicate unfolding eliminates predicates while preserving satisfiability, but exhaustive application can cause an exponential increase in Horn clauses and runtime.HoRSt therefore uses transformations such as linear folding, which merges clauses for sequential basic-block steps and runs linearly.
  • Optimizations: HoRSt also performs constant folding and value encoding to reduce SMT output and map custom data types to primitive encodings efficiently handled by z3.These transformations complement the clause-unfolding and folding strategies.

5 IMPLEMENTATION & EVALUATION

eThor combines a HoRSt-generated static analyzer with case studies and systematic evaluations of correctness, precision, and performance on Ethereum contracts.

  • Implementation: eThor is generated from HoRSt and implements the static analysis defined in Section 3.
  • Case study: The analysis supports functional correctness properties for SafeMath, including arithmetic overflow, underflow, and division-by-zero behavior.The properties were proved for all five functions within milliseconds.
  • Case study: The SafeMath case study also proves that a reinserted dynamic assertion is never violated.
  • Large-scale evaluation: The large-scale single-entrancy evaluation compared eThor with ZEUS on real-world contracts and used three Horn-clause-folding configurations.
  • Automated testing: 609 official EVM test cases were evaluated, including 604 properties relevant to single-contract settings.
  • Automated testing: 85% (513) of the test cases were solved precisely within one second, with a 99% (597) termination rate.

30 queries

The large-scale comparison evaluates termination and precision across real-world contracts, while showing that folding choices affect runtime differently across queries.

  • Termination: Results were obtained for all but 20 contracts after combining the different experiments.
  • Comparison with ZEUS: eThor achieved a 95.4% termination rate versus 98.3% for ZEUS, but required a 10-minute query timeout instead of one minute.
  • Precision: eThor achieved an F-measure of 88.9% compared with 20.4% for ZEUS.
  • Precision: ZEUS labeled only 22 contracts vulnerable, including one false positive, while the dataset contained 517 safe and 195 unsafe contracts.
  • Query runtimes: Both Horn-clause folding variants improve termination, but exhaustive folding is faster for simpler queries whereas linear folding often performs better on complex ones.

6 RELATED WORK & DISCUSSION

The discussion positions eThor against dynamic and heuristic static analyzers and emphasizes formal semantics, sound abstractions, and end-to-end guarantees as requirements for reliable analysis.

  • Prior approaches: Prior automated tools often focus on heuristic bug detection without theoretical guarantees or formal semantic characterizations of their target properties.
  • Soundness: Claims of sound automated analysis by Securify, ZEUS, EtherTrust, and NeuCheck are contrasted with missing proofs, semantics, or formal property definitions.
  • eThor’s design: eThor starts from formal EVM semantics, specifies a sound abstract semantics in HoRSt, and compiles it into an SMT encoding.
  • eThor’s design: Its control-flow preanalysis uses a sound relaxation of the abstract semantics, so the original soundness guarantees are inherited.

7 CONCLUSION

The paper presents eThor as an automated, sound static analyzer for EVM bytecode and introduces HoRSt to support maintainable Horn-clause-based analysis specifications. The conclusion highlights large-scale evaluation and future extensions to relational properties, precision, proof assistants, and automated pattern generation.

  • Conclusion: eThor abstracts EVM bytecode semantics into Horn clauses and expresses security and functional properties as reachability queries solved using z3.HoRSt generates optimized SMT-LIB implementations from high-level Horn-clause specifications.
  • Conclusion: A large-scale evaluation demonstrates the practicality of eThor and shows higher overall F-measure performance than ZEUS.The comparison is against the state-of-the-art analysis tool ZEUS.
  • Conclusion: Future work includes relational properties, multicontract abstractions, mechanized soundness proofs, and automated generation of analysis patterns.The stated goals include extending HoRSt and reducing domain knowledge required to design static analyzers.
  • A.1 HoRSt by Example: HoRSt predicate declarations support parameterized predicate families whose parameters are compiled into distinct predicate names for performance.The MState family uses a program-counter parameter to model contract state.
  • A.1 HoRSt by Example: HoRSt supports non-recursive operations over arbitrary types, including abstract addition and pattern matching over sum types.These operations help define abstract operations within the analysis specification language.
  • A.1 HoRSt by Example: Rule templates generate families of Horn clauses, while selector functions provide the concrete sequences over which those families range.Rules can be singleton instances or templates for arbitrarily many instantiations.

B.2 Analysis Definition (continued)

This section formalizes abstract domains, predicate orders, and abstract operations used in the analysis definition. It also limits the presentation to operations used in the main analysis and refers to HoRSt for the complete operation set.

  • Abstract domains: The order on predicate arguments compares tuples pointwise while requiring equal tuple dimensions.The same orders are assumed for corresponding argument domains of different predicates.
  • Abstract domains: The formal development establishes that selected partially ordered argument domains have suprema.This supports the order-theoretic structure used by the abstract analysis.
  • Abstract domains: HoRSt orders abstract values so that the unknown value ⊤ is above every abstract value.Function-valued domains likewise admit the top-valued function as an upper bound.
  • Abstract operations: Abstract binary operations lift natural-number operations to the abstract domains used by the analysis.Abstract comparison operators are defined analogously for Boolean results.
  • Abstract operations: The appendix defines additional memory-access operations, including integer-fraction extraction and append.The presentation focuses only on operations used in the main analysis.

B.3 Proof of soundness

The soundness proof uses complete induction over the number of small steps rather than one-step reasoning alone. The presentation is a proof sketch that omits proofs of several auxiliary lemmas.

  • Proof strategy: The soundness theorem is proved directly by complete induction on the number of small-step executions.Monotonicity is proved separately to simplify individual cases, but the final argument proceeds by induction over execution length.
  • Proof strategy: The section presents only a proof sketch covering the most interesting and challenging cases.Auxiliary lemmas are stated without full proofs.
  • Proof strategy: The soundness reasoning relies on general properties of small-step execution and callstack shapes.Most such properties are omitted because they follow from straightforward case distinctions and inductions.

Auxiliary lemmas.

The auxiliary lemmas establish invariants about callstacks, annotations, contract code, and storage that support the soundness argument. Key results depend on collision-free executions and excluding CALLCODE and DELEGATECALL from the analyzed contract.

  • Callstack properties: Callstack evolution preserves the structure needed to identify intermediate execution states as call states.In regular executions, every non-top callstack element is a call state.
  • Annotation properties: Execution annotations remain consistent with the active contract throughout execution.Annotation consistency is preserved, and the active contract annotation persists across the relevant callstack evolution.
  • Execution assumptions: The soundness argument restricts executions to those without problematic hash collisions that overwrite the analyzed contract’s code or storage.The paper characterizes these as collision-free executions and notes that the collision probability is negligible in practice.
  • Contract invariants: For contracts without CALLCODE and DELEGATECALL, strong annotation consistency is preserved and the contract code remains persistent during execution.The result relies on the collision-free execution assumption.
  • Storage properties: The storage-evolution lemma relates the analyzed contract’s storage to a prior execution of that same contract.Its alternatives include storage from the last call originating from the contract or from a completed prior execution.
  • Proof sketches: The proof sketches proceed by complete induction over small steps and analyze cases such as local operations, SSTORE, and CALL.The SSTORE case uses the fact that only the active account’s storage is modified.

Main Proof.

The soundness proof establishes that the Horn-clause abstraction over-approximates concrete EVM executions under the stated contract-code assumption. The proof proceeds by induction over small-step executions and treats local operations, calls, returns, and halting cases.

  • Soundness theorem: Theorem soundness guarantees that abstract executions cover concrete executions for contracts without DELEGATECALL or CALLCODE.The theorem is stated for strongly consistent execution states and annotated callstacks with nonempty successor stacks.
  • Calls and halting: The proof covers call initiation, returning from calls, regular halting, and exceptional halting.The CALL cases distinguish existing callees and inductive halting cases, while return cases use the abstract CALL rules.
  • Inductive structure: The proof uses complete induction on the number of small-step reductions.The base case is the empty reduction sequence; the inductive case decomposes the execution into a prefix and final step.
  • Local operations: Local instructions preserve the abstraction through reflexivity, monotonicity, and soundness of abstract operations.The proof illustrates ADD and states that the same reasoning applies to other local instructions.
  • Calls: CALL soundness is handled by distinguishing whether the newly pushed callstack element is abstracted and by applying the corresponding abstract CALL rules.The argument tracks storage preservation and uses monotonicity of the contract semantics.
  • Applications: Reachability analysis is then used to implement security properties, functional-correctness queries, and automated soundness and precision testing.The section introduces HoRSt infrastructure for reachability properties and related query mechanisms.

C.1 From reachability properties to queries

The section reduces unreachability properties to non-derivability of query sets in the abstract semantics. This reduction is valid when the target property has a nonempty abstraction and supports practical HoRSt queries and tests.

  • Property form: Unreachability properties require that no execution from a strongly consistent initial state reaches a nonempty successor satisfying the target predicate.The property quantifies over executions and excludes reachable configurations matching R.
  • Abstract reduction: A sound abstract configuration covering the initial predicate must not derive every abstract configuration covering the target predicate.The proof replaces reasoning over all target abstractions with a query set sharing an element with each possible target abstraction.
  • Query construction: It is sufficient to query the most concrete abstraction of target configurations together with all predicatewise coarser abstractions.The construction is valid only when some target configuration has a nonempty abstraction.
  • Query construction: Non-derivability of the constructed query set implies the corresponding unreachability property.This consequence turns the theoretical reduction into an SMT-checkable condition.
  • HoRSt implementation: HoRSt queries invoke an SMT solver to test whether premises are derivable from initialization under the specified rules.The language supports reachability queries generated from selector functions, including a reentrancy query for CALL reachability at call level 1.
  • Functional correctness: The enhanced semantics propagates call data and models return data so analysis can reason about execution inputs and returned values.CALLDATALOAD accesses the modeled call-data array rather than always over-approximating the loaded value.
  • Automated testing: Automated testing uses Hoare-logic-style reasoning, while dynamic jump conditions may require arbitrary jump destinations when inputs are not statically determined.The testing setup illustrates both HoRSt capabilities and the control-flow uncertainty induced by dynamic values.

No writes after calls.

The no-writes-after-calls property is an inadequate proxy for single-entrancy. Examples show both false positives and false negatives because reentrancy can exploit guards or storage mechanisms not captured by the pattern.

  • Pattern limitation: The compliance pattern excludes storage writes after CALL, but misses storage changes performed through DELEGATECALL.Library calls can modify the caller’s storage without an SSTORE appearing in the analyzed contract.
  • Conclusion: The no-writes-after-calls property is neither sound nor complete for single-entrancy.Its semantic definition excludes only SSTORE reachability even though other instructions can manipulate storage.
  • False negative: A bank contract can be reentrant despite performing no writes after the call.A malicious address can reenter through a public setter and reset the balance guard before draining funds again.
  • False positive: A locking contract violates the no-writes-after-calls property while preventing further calls during reentry.Reentry triggers an exception, but the lock must later be released, producing a write after the external call.
  • Related property: The property requires all write accesses to be restricted by at least one address that cannot reach the corresponding write when initiating the call.This definition supplies the intended semantic criterion for restricted writes.

Restricted write.

The restricted-write property and its patterns can misclassify contracts because they focus on SSTORE reachability and caller dependence. Examples include both false alarms for internally restricted writes and missed unrestricted writes through libraries.

  • Property definition: The restricted-write property requires at least one initiating address that cannot reach each corresponding write access.Its compliance and violation patterns reason about SSTORE reachability and storage offsets.
  • False positive: A contract with an internally restricted write can be reported as unrestricted by the violation pattern.The example’s caller check limits access to the internal write, but the dependency analysis still reports a violation.
  • Related transfer limitation: The restricted-transfer analysis can also miss restrictions when money transfers occur inside caller-guarded internal functions.The tool fails to detect that sendM is reachable only after a sender check.
  • Scope limitation: The handled-exception property lacks a semantic definition, making the sufficiency of its patterns difficult to establish.Examples of correctly and incorrectly handled exceptions are nevertheless classified by the patterns.

Handled exception.

The reviewed pattern-based analyses can misclassify contracts because syntactic checks do not reliably capture semantic behavior. Examples span exception handling, transaction ordering, and argument validation, while broader soundness and semantic-modeling problems remain.

  • Handled exception.: A call-return branch can satisfy the compliance pattern even when it does not affect the critical storage update.The SimpleBank example branches on success but updates storage regardless.
  • Handled exception.: Pattern-based checks may classify contracts incorrectly when syntactic conditions do not determine the relevant semantic behavior.The examples show false compliance and false violation results across several security properties.
  • Handled exception.: Library-outsourced branching can evade the corresponding exception-handling pattern despite influencing the post-call balance update.The return value is converted by Lib.toInt before updating the balance.
  • Handled exception.: Transaction-ordering patterns can miss vulnerable calls or flag safe calls because they inadequately model storage dependence and calling mechanisms.The examples respectively involve callcode using mutable price and a constant transfer amount labeled as TOD.
  • Handled exception.: Validated-argument patterns can accept unchecked writes or reject valid library-based validation because they rely on visible conditional branches.A check that does not control the write passes, while validation inside a library is not detected.
  • Handled exception.: The reviewed tools also lack reliable semantic and soundness foundations, including formalized properties, complete semantics, and sound handling of reentrant execution.The discussion identifies syntactic pattern limitations, missing formal connections, and an abstraction that assumes unchanged storage at reentry.

D.5 ZEUS

The ZEUS analysis translates Solidity through an intermediate language to LLVM bitcode and uses symbolic model checking, but the paper identifies gaps in its soundness claims and a faulty reentrancy treatment. A counterexample shows that identical function code can have different reentrancy behavior depending on other callable functions.

  • D.5 ZEUS: ZEUS translates Solidity to an abstract intermediate language and then LLVM bitcode for symbolic model checking.Security properties are expressed through reachability assertions, with some generic properties requiring additional contract modifications.
  • D.5 ZEUS: ZEUS lacks a formal soundness statement connecting Solidity policy compliance with its analysis results.The cited proof is described as sketchy and containing holes and flaws.
  • D.5 ZEUS: The intermediate-language call semantics omit the global-state revocation caused by failing EVM calls.The paper identifies this as a deviation from Solidity semantics.
  • D.5 ZEUS: ZEUS labels both contracts safe even though only one is protected against same-function reentrancy.The first contract exposes release before reentry, whereas the second omits that callable function despite identical drain implementations.
  • D.5 ZEUS: The authors could not empirically assess ZEUS directly because its sources or binaries were unavailable.They instead compared against a publicly available dataset reported by ZEUS.

Problems in the ZEUS dataset.

The ZEUS comparison dataset has substantial integrity and reproducibility problems: addresses are malformed or duplicated, many bytecodes cannot be retrieved, and no source or bytecode is provided for the listed contracts.

  • Problems in the ZEUS dataset.: Of 1,503 remaining entries, 397 addresses are truncated and the remaining 1,106 contain duplicates.Deduplication reduces the set to 1,033 addresses.
  • Problems in the ZEUS dataset.: Bytecode could not be obtained for 286 of the 1,033 deduplicated addresses.The cited reasons include self-destruction, absent recorded transactions, and one external account.
  • Problems in the ZEUS dataset.: The dataset was deduplicated on source level by its original authors, so identical bytecodes may still correspond to different source codes.This complicates interpreting address- and source-level uniqueness.
Loading 2005.06227v1…