PaperlayerView exact revision on arXiv

Source-linked AI summary

VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts

Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, Hakjoo Oh

arXiv:1908.11227v2cs.PLcs.CR

TL;DR

Arithmetic bugs threaten Ethereum smart contracts, while existing analyzers miss known vulnerabilities or raise false alarms. VeriSmart automatically infers transaction invariants during verification, achieving 100% recall and a 0.41% false-positive rate in its CVE evaluation.

  • Problem

    Arithmetic bugs are common in Ethereum contracts and can cause significant unexpected financial damage, while existing analyzers miss known vulnerabilities and raise false alarms.

    Source: §I · pp. 1–2

  • Method

    VeriSmart automatically discovers transaction invariants and uses them to verify smart contracts exhaustively without separately exploring all program paths.

    Source: §I · p. 1

  • Results

    100% recall and 0.41% false-positive rate; on 60 CVE contracts, VeriSmart detected all known vulnerabilities, while existing bug-finders missed >29.3% and had >5.4% false positives.

    Source: §I · p. 2, A. Comparison with Bug-finders · p. 9

  • Takeaways & Limitations

    VeriSmart’s results highlight the value of automatically inferring and using transaction invariants in arithmetic-safety verification.

    Source: §VII · p. 14

    The 60-CVE and 25-contract ZEUS benchmark sets might not be representative.

    Source: D. Threats to Validity · p. 12

Abstract

from arXiv · show

We present VeriSmart, a highly precise verifier for ensuring arithmetic safety of Ethereum smart contracts. Writing safe smart contracts without unintended behavior is critically important because smart contracts are immutable and even a single flaw can cause huge financial damage. In particular, ensuring that arithmetic operations are safe is one of the most important and common security concerns of Ethereum smart contracts nowadays. In response, several safety analyzers have been proposed over the past few years, but state-of-the-art is still unsatisfactory; no existing tools achieve high precision and recall at the same time, inherently limited to producing annoying false alarms or missing critical bugs. By contrast, VeriSmart aims for an uncompromising analyzer that performs exhaustive verification without compromising precision or scalability, thereby greatly reducing the burden of manually checking undiscovered or incorrectly-reported issues. To achieve this goal, we present a new domain-specific algorithm for verifying smart contracts, which is able to automatically discover and leverage transaction invariants that are essential for precisely analyzing smart contracts. Evaluation with real-world smart contracts shows that VeriSmart can detect all arithmetic bugs with a negligible number of false alarms, far outperforming existing analyzers.

I. INTRODUCTION

VERISMART targets arithmetic safety with exhaustive, precise verification that automatically discovers transaction invariants. Its motivating examples show how invariant reasoning can expose missed arithmetic bugs and distinguish real vulnerabilities from false alarms.

I. INTRODUCTION

  • Arithmetic over/underflows account for 95.7% (487/509) of CVEs assigned to Ethereum smart contracts, and exploited arithmetic bugs can cause unexpected financial damage.Smart contracts are also vulnerable because of characteristics such as openness and immutability.Source: §I · p. 1
  • Existing bug-finders may miss bugs by not considering all behaviors, while exhaustive verifiers can produce false positives, burdening developers with manual checks.VERISMART aims to be exhaustive yet precise.Source: §I · p. 1
  • The algorithm automatically discovers transaction invariants that hold under arbitrary transaction interleavings, avoiding separate exploration of every program path.It iteratively generates and validates candidate invariants in a feedback loop akin to CEGIS and can analyze safety properties beyond arithmetic safety.Source: §I · pp. 1–2
  • VERISMART detected all known vulnerabilities in 60 CVE-vulnerable contracts with a 0.41% false-positive rate; existing bug-finders missed >29.3% and had >5.4% false-positive rates.The evaluation also found VERISMART significantly more precise than ZEUS and SMTCHECKER.Source: §I · p. 2
  • VERISMART supports the full Solidity language; its evaluation compares six analyzers, and its tool and data are publicly available for reproducibility.The paper presents the implementation as a practical tool for Ethereum smart contracts.Source: §I · p. 2

II. MOTIVATING EXAMPLES

  • In SmartMesh's proxyOverflow, fee+value can overflow and disable sanity checks, allowing a transfer to create a huge amount of tokens from nothing.Among the cited bug-finders, only OSIRIS finds this vulnerability; MYTHRIL and OYENTE miss it.Source: §II · p. 2
  • In Neo Genesis Token, the unchecked value * to.length product can overflow, and bug-finders handle this similar vulnerability inconsistently.OSIRIS detects the first example but fails on the similar second example; MYTHRIL reports no issue and OYENTE gives an imprecise warning.Source: §II · p. 3
  • BTX's transfer and transferFrom additions are safe because transaction invariants hold across arbitrary interleavings, but existing tools either raise false alarms or cannot prove safety.VERISMART automatically infers the hidden invariants and proves the contract safe without false alarms.Source: §II · p. 3

III. VERISMART ALGORITHM

The algorithm is presented in a general setting for safety properties, with arithmetic safety as its application. Its Solidity model and assertion-based goals define the verification task.

III. VERISMART ALGORITHM

  • The algorithm is presented for safety properties beyond arithmetic safety, which is its application in this paper.The paper says the algorithm is formally presented in a general setting.Source: §III · p. 3
  • The formal presentation focuses on a core Solidity subset, while the paper states that VeriSmart supports the full language through an extension.The subset models mappings as arrays, public or external functions, and 256-bit unsigned arithmetic.Source: §III · p. 4
  • The goal is to prove or disprove each assertion, with arithmetic-safety queries automatically generated for operations such as addition and multiplication.The examples check addition for overflow and multiplication for overflow using assertions.Source: §III · p. 4

A. Algorithm Overview

VeriSmart searches for contract-specific transaction and loop invariants, refining candidates through generator feedback until queries are proven or the search ends. Its validator checks invariant inductiveness and assertion safety over basic paths.

A. Algorithm Overview

  • VeriSmart applies a CEGIS-style algorithm to search for hidden invariants needed to verify smart-contract safety properties.The paper describes a domain-specific instantiation with validator, generator, and solver components.Source: A. Algorithm Overview · pp. 4–5
  • A transaction invariant holds after construction and remains valid across public-function executions, while loop invariants hold at loop entry and are preserved by the loop body.The algorithm seeks one global transaction invariant and a separate invariant for each loop.Source: A. Algorithm Overview · p. 4
  • The generator proposes candidate invariants, and the validator returns unproven queries as feedback for iterative refinement until proof succeeds or the time budget expires.At termination, unproven queries are reported as potential safety violations.Source: A. Algorithm Overview · pp. 4–5

B. Validator

  • The validator converts annotated programs into exhaustive basic paths and generates verification conditions for each path.Paths summarize transactions and loops using their invariants.Source: B. Validator · p. 5
  • Each path's verification conditions check both invariant inductiveness and the safety properties in assertions.The generated pair contains a condition for inductiveness and conditions for query safety.Source: B. Validator · p. 6
  • When inductiveness fails, the validator prioritizes refining invariants; once they are inductive, it collects paths with unproven safety queries.The solver checks verification-condition validity.Source: B. Validator · p. 6

C. Generator

The generator refines transaction and loop invariants using a domain-specific search space designed around common smart-contract patterns. It uses feedback from unproven paths to generate stronger candidates.

C. Generator

  • The generator uses unproven paths to refine either loop invariants or transaction invariants and produce new candidates.Loop and transaction invariants are refined separately based on the relevant path context.Source: C. Generator · p. 6
  • Its refinement relation is designed to balance search-space breadth against tractability for real-world smart contracts.The paper warns that overly general or overly specific relations make verification impractical.Source: C. Generator · p. 6
  • Candidate invariants use simple numerical forms such as variable comparisons and bounds, rather than nonlinear or compound formulas.The supported forms include x = y, x ≥ y, x = n, x ≥ n, and x ≤ n.Source: C. Generator · p. 6
  • The generator supports mapping-sum invariants and restricts candidates to quantifier-free conjunctive formulas without disjunctions or quantifiers.For example, sum(balance) can express that all balances add to totalSupply.Source: C. Generator · p. 6
  • Refinement adds a linear, quantifier-free atomic predicate, with transaction and loop searches using different variable and constant sets.Transaction search uses globals and constructor constants; loop search uses variables and constants from the enclosing function and current path.Source: C. Generator · p. 7

D. Solver

The solver combines an off-the-shelf SMT solver with domain-specific preprocessing and validity checks. These checks target formulas involving mappings and arithmetic, while a syntactic invalidity test trades possible false positives for avoiding SMT calls.

D. Solver

  • The solver preprocesses verification conditions before using Z3, since domain-specific symbols such as sum are not understood by conventional SMT solvers.The paper reports that preprocessed formulas can still be too complex for efficient SMT solving.Source: D. Solver · p. 7
  • For mapping sums, preprocessing instantiates the sum with respect to the indices used on a path and adds constraints to preserve the sum and prevent overflow.The example handles equal and distinct indices separately and introduces a fresh variable for the remaining elements' sum.Source: D. Solver · p. 7
  • A free-variable test can reject an invalid implication syntactically when its premise omits a variable appearing in its conclusion, avoiding an SMT call.The authors report this improves scalability, but it can classify some valid VCs as invalid because it checks only a necessary condition.Source: D. Solver · p. 7
  • The free-variable test may produce false positives, but the paper states that it cannot treat an invalid VC as valid and thus can be used by sound verifiers.The authors report that the technique caused no false positives in their experiments.Source: D. Solver · pp. 7–8
  • Domain-specific validity templates can prove some formulas without an external SMT call, including a subtraction-underflow condition when n1 ≤ n2.The example template establishes x ≥ (x * n1)/n2 for a 256-bit unsigned integer x.Source: D. Solver · p. 8

IV. IMPLEMENTATION

VeriSmart implements its verifier for Solidity, with support for most language features except inline assembly. It handles skipped calls conservatively to retain exhaustive verification, while noting that this can reduce precision.

IV. IMPLEMENTATION

  • VERISMART supports the full Solidity language except inline assembly, desugaring most features into its core language.The implementation comprises about 7,000 lines of OCaml code.Source: §IV · p. 8
  • Function calls are inlined up to depth 2, except for large functions and inter-contract calls, which receive conservative handling.For skipped calls, VeriSmart weakens affected predicates and separately analyzes the non-inlined function bodies.Source: §IV · p. 8
  • Non-inlined public or external functions in the main contract receive transaction invariants, while internal, private, and other-contract functions are analyzed from over-approximated input states.Their entries and exits are annotated with true for verification-condition generation.Source: §IV · p. 8
  • Conservative function-call analysis preserves exhaustive verification but may reduce precision; the authors report that it remains precise enough in practice.The approach considers possible behaviors rather than omitting them.Source: §IV · p. 8
  • The implementation supports inheritance by copying parent functions and global variables while accounting for overriding and variable hiding, and encodes structures as arrays with member mappings that handle aliasing.Aliased structures share member values through the same mapping.Source: §IV · p. 8
  • Inline assembly may conceal bugs in embedded bytecode, which VeriSmart may miss, although it conservatively analyzes the remaining source code around assembly blocks.In the benchmarks, four contracts contained assembly blocks, none of which included arithmetic operations.Source: §IV · p. 9

V. EVALUATION

The evaluation compares VeriSmart with existing bug-finders and verifiers, and includes a case study on extending it to other vulnerability types. The experiments used then-current tool versions on a specified machine.

V. EVALUATION

  • The evaluation asks how precisely VERISMART detects arithmetic bugs relative to four bug-finders and how it compares with two existing verifiers.The bug-finders are OSIRIS, OYENTE, MYTHRIL, and MANTICORE; the verifiers are ZEUS and SMTCHECKER.Source: §V · p. 9
  • A case study examines whether VERISMART can be extended to support other types of vulnerabilities.Source: §V · p. 9
  • The experiments used the latest available versions of the tools as of May 1, 2019, on a machine with an Intel Core i7-9700K and 64GB RAM.Source: §V · p. 9

A. Comparison with Bug-finders

On a 60-contract CVE benchmark, VeriSmart detected all known vulnerabilities with low false-positive rates and outperformed the compared bug-finders on precision and recall. The analysis also identifies sources of false alarms and missed bugs, and reports six incorrect CVE vulnerability reports.

A. Comparison with Bug-finders

  • VERISMART achieved a 0.41% false positive rate (2/492) and 100% recall across 976 queries, detecting all CVE vulnerabilities.The benchmark comprised 60 contracts with CVE vulnerabilities; the authors manually inspected the reported alarms and unreported queries.Source: A. Comparison with Bug-finders · p. 9
  • On the 60 benchmark programs, VERISMART took 1.1 hour (3,807 seconds), compared with 4.2 hours for OSIRIS, 14 minutes for OYENTE, 13.8 hours for MYTHRIL, and 31.4 hours for MANTICORE.The totals exclude timeouts and internal errors; MANTICORE sometimes failed to terminate within three days despite a 30-minute timeout.Source: A. Comparison with Bug-finders · p. 9
  • Of 37 false positives from bug-finders, 18 were attributed to missing transaction invariants and 19 to imprecise handling of conditional statements.VERISMART avoided the 18 false positives attributed to missing transaction invariants.Source: A. Comparison with Bug-finders · p. 10
  • OSIRIS and OYENTE falsely flagged a guarded subtraction as unsafe, while VERISMART analyzes conditional statements precisely and avoids such false alarms in that example.The subtraction is safe because the preceding guard ensures the relevant bound.Source: A. Comparison with Bug-finders · pp. 10–11
  • Bug-finders often missed vulnerabilities reachable through inter-contract calls; VERISMART detected an example involving additions that could overflow and bypass a token-limit check.The example’s three addition operations could overflow for some inputs.Source: A. Comparison with Bug-finders · p. 11
  • VERISMART identified six incorrectly reported CVE vulnerabilities and proved the associated queries safe with zero false positives; OSIRIS and OYENTE alarmed on all six safe queries.The authors manually confirmed the CVE reports were incorrect and submitted a revision request.Source: A. Comparison with Bug-finders · p. 11

B. Comparison with Verifiers

The comparison evaluates VeriSmart against SMTCHECKER and ZEUS on a limited ZEUS-derived dataset, then shows how VeriSmart can be applied to access-control bugs. The verifier comparison reports differences in coverage and false alarms, while the case study tests an automatically generated safety property.

B. Comparison with Verifiers

  • ZEUS could not be run on the dataset, and its public results lacked alarm details; the comparison therefore used 25 unique contracts drawn from its public evaluation data.SMTCHECKER was run with its default setting.Source: B. Comparison with Verifiers · p. 11
  • On the 25-contract ZEUS dataset, VeriSmart produced 34 true positives and 6 false positives; SMTCHECKER analyzed 13 contracts and produced 50 false positives among 55 alarms.Table IV reports the ZEUS-dataset evaluation; the prose gives the alarm classifications and coverage.Source: Table IV · p. 12, B. Comparison with Verifiers · p. 12
  • Without inferred transaction invariants, VeriSmart failed to verify 17 of the 25 contracts.The authors identify transaction invariants as key to VeriSmart’s high precision.Source: B. Comparison with Verifiers · p. 12

C. Case Study: Application to Other Types of Vulnerabilities

  • In the EtherCartel example, anyone could set the Ether beneficiary and potentially divert assets when users bought digital goods; the vulnerability was exploited about an hour after deployment.The example uses the DrugDealer and buyDrugs functions.Source: C. Case Study: Application to Other… · p. 12
  • VeriSmart generated assertions before assignments to global address variables, excluding constructor assignments, to check that the assigning caller matched the address.This extension detected the three listed CVE vulnerabilities and proved the bug scenario absent in 55 of 60 contracts; it could not prove safety for the other five because of specification imprecision.Source: C. Case Study: Application to Other… · p. 12

D. Threats to Validity

The paper notes limits to its evaluation and positions VeriSmart among automated and formal smart-contract analyses. It concludes that automatically inferring and using transaction invariants is central to its approach.

D. Threats to Validity

  • The evaluation may not generalize beyond its 60-CVE and 25-ZEUS contract datasets; results may also vary with Z3 performance and timeout settings.The authors also did not assess exploitability, and acknowledge that manual alarm classification can be challenging and sometimes subjective.Source: D. Threats to Validity · p. 12

A. Analyzing Smart Contracts

  • Automated smart-contract analyzers include bug-finders based on symbolic execution or fuzzing and exhaustive verifiers, while Datalog-based analyzers cannot infer transaction invariants.The paper notes that bug-finders may miss critical vulnerabilities, and that ZEUS and SMTCHECKER lack inter-transactional reasoning.Source: A. Analyzing Smart Contracts · p. 13
  • Semi-automated formal methods can verify broad functional properties but require user-provided specifications or invariants; manual safety annotations can be error-prone and detect bugs only at runtime.The paper contrasts these approaches with compile-time verification.Source: A. Analyzing Smart Contracts · p. 13

B. Analyzing Arithmetic Safety of Traditional Programs

  • For arithmetic safety, VeriSmart uses a CEGIS-style algorithm and unbounded verification rather than abstract domains that may not capture smart-contract invariants.The paper distinguishes its smart-contract-specific approach from prior arithmetic-safety analyses and says its CEGIS-style application is new to its knowledge.Source: B. Analyzing Arithmetic Safety of… · p. 13

VII. CONCLUSION

  • VeriSmart implements automatic inference of hidden, especially transaction, invariants and uses them to verify arithmetic safety in Ethereum smart contracts.The conclusion presents this as the algorithm’s central feature and identifies inability to infer and use transaction invariants as a shortcoming of existing approaches.Source: §VII · p. 14

APPENDIX

The appendix preprocessing replaces sum equalities in verification conditions with constraints over mapping values and fresh variables. For indexed sums, it accounts for possible equalities among the index variables.

APPENDIX

  • For sum(x) = e, preprocessing uses fresh variables Rx and Bx when the index set is empty, and constraints involving x[i], Rx, and Bx when it has one index.The resulting constraints are conjoined as G1 and G2.Source: A. Preprocessing of Verification… · p. 16
  • With two or more indices, the preprocessing considers partitions of the index set to represent possible equality patterns, then constrains the distinct mapping elements.For example, {i, j} has two partitions, while {i, j, k} has five.Source: A. Preprocessing of Verification… · p. 16
  • For the indexed sum example, the transformation distinguishes i = j from i ≠ j and adds constraints for both the sum equality and absence of overflow.The transformed formula is satisfiable if and only if the original verification condition is satisfiable.Source: A. Preprocessing of Verification… · p. 16

B. Proof of Proposition 1

The proof derives a contradiction from the stated conditions by constructing a variant interpretation. It concludes that p does not imply q.

B. Proof of Proposition 1

  • The proof constructs an x-variant interpretation and combines it with the preceding conditions to contradict the assumed implication, concluding p does not imply q.The passage states the conclusion as p ⊭ q.Source: B. Proof of Proposition 1 · p. 16

C. More Examples of Validity Templates

The section gives additional validity templates for proving arithmetic verification conditions, assuming the formula is in CNF. The examples include mapping-sum constraints and a proof that avoids preprocessing and an SMT solver.

C. More Examples of Validity Templates

  • The examples assume F is in conjunctive normal form, with c ∈ F denoting that c is a clause of F.The section introduces these as three further examples relevant to performance.Source: C. More Examples of Validity Templates · p. 17
  • A mapping total of 100 and a lower bound on one entry suffice to prove that adding the bound to any entry cannot decrease it, without preprocessing or an SMT solver.The example instantiates the template with a[i] ≥ k and concludes a[j] + k ≥ a[j].Source: C. More Examples of Validity Templates · p. 17
  • A related template replaces sum(x) = n with sum(x) = y and y = n while retaining the conclusion that x[q] + v ≥ x[q].The example's mapping indexes are addresses and its values are unsigned 256-bit integers; n+n must not overflow.Source: C. More Examples of Validity Templates · p. 17
  • Another validity template proves 48 + (y%10) ≥ 48 for a 256-bit unsigned variable x when the integer constants n1 and n2 do not overflow when added.The passage identifies this as a proof using the validity template above.Source: C. More Examples of Validity Templates · p. 17
Loading 1908.11227v2…