PaperlayerView exact revision on arXiv

Source-linked AI summary

Harvey: A Greybox Fuzzer for Smart Contracts

Valentin Wüstholz, Maria Christakis

arXiv:1905.06944v1cs.SEcs.CR

TL;DR

Smart-contract greybox fuzzing must handle narrow input checks and state-dependent transaction sequences without losing tractability. HARVEY addresses these challenges with lightweight input prediction and demand-driven sequence fuzzing, and its evaluation on 27 contracts reports higher coverage and vulnerability-detection effectiveness, often orders-of-magnitude faster.

  • Problem

    Greybox fuzzers randomly mutate inputs, making narrow checks difficult to satisfy, while stateful contracts require transaction sequences whose search space can grow exponentially.

  • Method

    HARVEY predicts concrete inputs from prior executions and fuzzes transaction sequences on demand, avoiding sequences that cannot further increase coverage.

  • Results

    On 27 real-world contracts, HARVEY’s techniques significantly increased coverage and vulnerability-detection effectiveness, often orders-of-magnitude faster; branch-condition input prediction achieved 99% success in one iteration.

  • Takeaways & Limitations

    Input prediction and demand-driven sequence fuzzing significantly improve HARVEY’s effectiveness for fuzzing real-world smart contracts.

  • Takeaways & Limitations

    The results may not generalize to all smart contracts or program types, and comparisons focus on a single fuzzer.

Abstract

from arXiv · show

We present Harvey, an industrial greybox fuzzer for smart contracts, which are programs managing accounts on a blockchain. Greybox fuzzing is a lightweight test-generation approach that effectively detects bugs and security vulnerabilities. However, greybox fuzzers randomly mutate program inputs to exercise new paths; this makes it challenging to cover code that is guarded by narrow checks, which are satisfied by no more than a few input values. Moreover, most real-world smart contracts transition through many different states during their lifetime, e.g., for every bid in an auction. To explore these states and thereby detect deep vulnerabilities, a greybox fuzzer would need to generate sequences of contract transactions, e.g., by creating bids from multiple users, while at the same time keeping the search space and test suite tractable. In this experience paper, we explain how Harvey alleviates both challenges with two key fuzzing techniques and distill the main lessons learned. First, Harvey extends standard greybox fuzzing with a method for predicting new inputs that are more likely to cover new paths or reveal vulnerabilities in smart contracts. Second, it fuzzes transaction sequences in a targeted and demand-driven way. We have evaluated our approach on 27 real-world contracts. Our experiments show that the underlying techniques significantly increase Harvey's effectiveness in achieving high coverage and detecting vulnerabilities, in most cases orders-of-magnitude faster; they also reveal new insights about contract code.

I. INTRODUCTION

HARVEY addresses two challenges in smart-contract fuzzing: narrow input checks and the large search space of state-dependent transaction sequences. It combines lightweight input prediction with demand-driven sequence fuzzing and improves coverage and vulnerability detection on 27 real-world contracts.

  • Motivation: Smart-contract reliability is critical because bugs may jeopardize digital assets, motivating automated vulnerability detection.Automatic test generation includes random testing, greybox fuzzing, and dynamic symbolic execution.
  • Challenge #2: Smart contracts can transition through many states, so vulnerability detection may require sequences of invocations whose number grows exponentially.A gambling contract, for example, may require sequences of bets from multiple players.
  • Approach: HARVEY predicts concrete inputs from execution information, using lightweight cost metrics to target executions that satisfy desired properties such as flipping branch conditions.Costs measure proximity to a property at a program location and guide iterative input prediction.
  • Evaluation: 99% success in flipping branch conditions in a single iteration demonstrates effective input prediction.The experiments evaluated HARVEY on 27 Ethereum smart contracts; coverage increased by up to 3x and vulnerability detection was often orders-of-magnitude faster.
  • Approach: HARVEY uses demand-driven sequence fuzzing to avoid generating transaction sequences when they cannot further increase coverage.Transactions can change contract state and thereby affect later invocations.
  • Evaluation: 74% of bugs in real smart contracts require more than one transaction to be found.This result supports pruning the transaction-sequence search space during fuzzing.

II. BACKGROUND

The background explains standard greybox fuzzing and the blockchain setting in which smart contracts execute. Greybox fuzzing records explored paths and retains inputs that discover new ones, while contract transactions can modify persistent state.

  • Greybox Fuzzing: Greybox fuzzing runs seeded inputs, records each execution path with a unique identifier, and assigns selected inputs an energy value for mutation.The path-to-input mapping stores an input that exercises each identified path.
  • Greybox Fuzzing: Mutated inputs are retained when they exercise previously unexplored paths, and the process repeats until an exploration bound is reached.The resulting test suite contains one test for each explored path.
  • Smart Contracts: Ethereum supports user and contract accounts that store balances, are owned by users, and reside publicly on the blockchain.Ethereum is described as a blockchain-based distributed-computing platform.
  • Smart Contracts: Contract accounts are managed by code and maintain persistent state, such as auction bids, that can encode agreements between users.Contract code is associated with the account and governs its behavior.
  • Smart Contracts: Smart contracts comprise contract accounts, their code, and persistent state; languages such as Solidity and Vyper compile to EVM bytecode.The paper uses this terminology for Ethereum contracts.
  • Smart Contracts: Users interact with contracts through transactions that call functions and require gas fees roughly proportional to the amount of code executed.Bidding in an auction is an example of a transaction-driven function call.

III. OVERVIEW

Harvey addresses narrow input checks and state-space explosion in smart-contract fuzzing with input prediction and demand-driven transaction-sequence fuzzing. The approach achieves high coverage and detects vulnerabilities efficiently on real-world contracts.

  • Challenge #1: Random Input Mutations: Greybox fuzzers struggle with narrow checks because random mutations repeatedly exercise existing paths instead of reaching rare values.For the example function, AFL generated about 311M inputs over 12 hours yet covered only four of five paths; the missing path required a = 42.
  • Challenge #1: Random Input Mutations: Input prediction adds lightweight instrumentation that estimates distances to desired executions and guides inputs toward branch flips or other cost-minimizing conditions.The technique avoids program analysis and constraint solving while using cost metrics to define optimal executions.
  • Challenge #1: Random Input Mutations: HARVEY explores all five paths of the example function in 0.27s after generating 372 inputs.This contrasts with AFL’s four-path result after 12 hours and about 311M generated inputs.
  • Challenge #2: State Space Exploration: Stateful contracts require transaction sequences because later invocations depend on persistent state established by earlier transactions.In the Foo example, the assertion requires SetY(42), CopyY(), and Bar(), or 42 calls to IncX before Bar().
  • Challenge #2: State Space Exploration: Demand-driven sequence fuzzing generates longer sequences only when state mutation could increase coverage for the final transaction, reducing redundant exploration.HARVEY computes path identifiers only for the last transaction and treats earlier transactions as state setup.

IV. FUZZING WITH INPUT PREDICTION

HARVEY extends greybox fuzzing by evaluating execution costs, predicting inputs, and retaining tests that explore new paths. Its worked example shows prediction reaching full path coverage with a compact test suite, though practical choices remain partly heuristic.

  • Algorithm: HARVEY augments seed-based greybox fuzzing with a cost function evaluated at encountered execution states.The cost function maps execution states to metrics used to guide input generation.
  • Algorithm: The algorithm compares an original and mutated input, identifies the changed parameter, and predicts a new value that minimizes a selected cost metric.If prediction is unavailable, standard mutation is used instead.
  • Algorithm: Predicted inputs are tested alongside seeds and mutations, and inputs exercising previously unexplored paths are added to the test suite.The output is a suite containing one test for each explored path.
  • Example: In the worked example, prediction covers paths with return values 3, 4, 2, and 5, achieving full path coverage with only 8 tests.The example’s table records inputs, paths, costs, prediction sources, and energy values.
  • Limitations: In practice, HARVEY achieved full path coverage of the example with 372 tests rather than the 8 tests shown by the illustrative algorithm trace.The algorithm includes random or heuristic choices for input selection, parameter selection, and cost selection.

B. Input Prediction

HARVEY predicts inputs by using cost changes from executions that differ in one parameter, then applying the Secant method to estimate a zero-cost value. The approximation is most precise for linear or piece-wise linear metrics.

  • Input Prediction: The prediction component compares two executions differing in one input parameter and selects a cost metric whose values differ between them.The corresponding inputs and cost vectors provide the data used for prediction.
  • Input Prediction: Using two input-cost points, HARVEY seeks an input value whose corresponding cost is zero and applies the Secant method through successive approximations.The goal is to find a root of the unknown but computable function relating the parameter to the cost metric.
  • Input Prediction: HARVEY fits a line c(i) = m ∗i + k through the two points and selects the x-coordinate where that line reaches zero cost.For points (−1, 43) and (7, 35), the line is c(i) = −i + 42, predicting a = 42.
  • Limitations: The approximation is precise for linear or piece-wise linear cost metrics; otherwise, HARVEY iterates the Secant step, although one iteration is typically sufficient for real contracts.The method can fail to minimize the cost metric when the linearity assumption does not hold.

C. Cost Metrics

Harvey uses cost metrics to guide executions toward flipped branch conditions or assignments to arbitrary persistent-state addresses. These metrics support input prediction for coverage and vulnerability detection.

  • Harvey minimizes cost metrics designed either to flip branch conditions or to modify arbitrary persistent-memory locations.The metrics are selected according to whether the target execution should satisfy a branch objective or expose memory-access behavior.
  • Branch conditions: For ==, <, and <= comparisons, Harvey defines operator-specific cost functions from the operands of each branch condition.The instrumentation evaluates two cost metrics before every branch condition, with analogous functions supporting !=, >, and >=.
  • Branch conditions: Because the cost functions use comparison operands rather than program inputs, minimizing a cost definitely flips the corresponding branch.Approximation enters only when correlating a program input with the cost metric.
  • Memory accesses: The memory-access metric targets underflow-enabled out-of-bounds writes that can place persistent state at attacker-chosen locations.In the wallet example, popping an empty array underflows its unsigned length and disables array bound checks.
  • Memory accesses: For memory-access vulnerabilities, Harvey compares an assignment’s persistent-state address with an arbitrary address and minimizes their distance.The instrumentation evaluates this metric before each persistent-state assignment, excluding local-variable assignments.
  • Memory accesses: With input prediction enabled, Harvey detects the wallet vulnerability within a few seconds, whereas disabling prediction misses it within 12 hours.The address-matching strategy would otherwise find the vulnerability only by chance because arbitrary address matches are extremely unlikely.
  • Memory accesses: The arbitrary-address detector can produce false positives when the assignment intentionally targets that address, although none occurred during the experiments.The authors report that this situation is extremely unlikely in practice.

V. DEMAND-DRIVEN SEQUENCE FUZZING

Harvey generates longer transaction sequences only when aggressive state fuzzing indicates that they may increase coverage of the final transaction. This demand-driven strategy keeps sequence exploration targeted while supporting deep-state vulnerability discovery.

  • Harvey uses demand-driven sequence fuzzing to set up persistent state for the sequence’s final transaction and explore new paths there.The goal is to detect additional bugs without indiscriminately expanding transaction sequences.
  • Regular mode mutates transactions normally, while aggressive mode directly fuzzes persistent state with probability 0.125.Aggressively discovered inputs are discarded because direct state mutation may produce false positives.
  • Harvey creates longer sequences only when aggressive fuzzing discovers new paths for the final transaction.If aggressive fuzzing finds no additional paths, the tool does not prepend more transactions.
  • The sequence SetY(42), CopyY(), and Bar() reaches the example assertion in about 18 seconds.Harvey stops exploring longer sequences for Foo when aggressive state fuzzing cannot further increase coverage.
  • Input prediction helps Harvey find the required SetY argument, while single-transaction path identifiers determine whether longer sequences are warranted.Demand-driven expansion therefore relies on path identifiers that span no more than one transaction.
  • Mutation operations: Harvey mutates sequences by fuzzing a transaction, inserting a transaction before it, or replacing preceding transactions with another sequence.Transaction and sequence pools supply previously coverage-increasing state modifications for the latter two operations.

VI. EXPERIMENTAL EVALUATION

The evaluation tests Harvey on a diverse benchmark suite of 27 real-world smart contracts selected from popular, audited-oriented Ethereum projects. The setup follows published fuzzer-evaluation guidelines rather than indiscriminate blockchain scraping.

  • The evaluation compares Harvey configurations to assess its two fuzzing techniques while also examining insights about smart-contract code.The study first describes benchmark selection and experimental setup before comparing configurations.
  • 27 benchmarks were selected from 17 GitHub repositories, including popular Ethereum projects such as ENS auction, ConsenSys wallet, and MicroRaiden.The repository set had 4’857 total GitHub stars, with a median of 132 on 2019-05-07.
  • Benchmark descriptions report each contract’s public-function count and Solidity source-code size.The benchmark suite includes multiple contracts from repositories implementing complex systems such as auctions.
  • The benchmark selection follows published fuzzer-evaluation guidelines and excludes indiscriminately scraped blockchain contracts.The authors cite poor quality, duplication, dead code, and missing dependencies as reasons for avoiding simple blockchain scraping.
  • Most contracts contain a few hundred lines, but source size does not necessarily indicate the difficulty of covering all paths.A small example function left one of five paths unexplored after 12 hours of AFL fuzzing.

B. Experimental Setup

The evaluation compares HARVEY configurations to measure input prediction and demand-driven sequence fuzzing across bug detection, coverage, and sequence exploration. Experiments use repeated runs on smart-contract benchmarks and standard greybox baselines.

  • Experimental protocol: 24 independent runs per configuration used fixed seed conditions and a one-hour time limit, with medians and Wilcoxon-Mann-Whitney tests reported.The evaluation ran on a 36-core Intel Xeon machine with 60GB RAM under Ubuntu 18.04.
  • Input prediction: Configuration B found 43 out of 47 bugs significantly faster than configuration A, with speedups up to 5’247 and a median of 25.96.B enabled input prediction while A disabled it; B also detected 10 more bugs on average.
  • Input prediction: 23 out of 27 benchmarks achieved significantly higher instruction coverage with input prediction, while path-coverage results were very similar.The comparison was between configuration A without prediction and B with prediction.
  • Iterative input prediction: For 45 of 47 bugs, configurations B and C showed no significant time difference, and instruction coverage also showed no significant difference.C omitted iterative application of the Secant approximation step when the basic step failed.
  • Iterative input prediction: One-shot cost minimization achieved a 97%–100% success rate with a median of 99% in experiments with C.The result suggests complex branch conditions are uncommon in real-world smart contracts.
  • Sequence fuzzing: 26 out of 35 bugs required more than one transaction, while spanning paths across transactions made the test suite orders-of-magnitude larger.Configuration A with demand-driven sequence fuzzing was compared against D, which eagerly explored all possible transaction-sequence paths.

D. Threats to Validity

HARVEY’s validity is bounded by external-generalization concerns and comparisons centered on a single fuzzer, while its techniques are positioned against related fuzzing and analysis approaches. The paper emphasizes lightweight input prediction and greybox-only demand-driven sequence fuzzing.

  • Threats to validity: Results may not generalize to all smart contracts or program types, although the evaluation used contracts from diverse domains.The authors provide contract versions and repository information to support further assessment of external validity.
  • Threats to validity: Comparisons focus on a single fuzzer because other related tools use fundamentally different bug-finding techniques or target different bug types.The baselines implement standard greybox fuzzing within HARVEY.
  • Related work: HARVEY predicts concrete input values from two previous executions using additional but lightweight instrumentation.The approach can be combined with other greybox-fuzzing techniques.
  • Related work: Input prediction avoids program analysis and constraint solving, although it uses more instrumentation than standard greybox fuzzing.The instrumentation captures distances from optimal executions at program points.
  • Future directions: HARVEY could benefit from complementary hybrid-fuzzing approaches such as static analysis and lightweight dynamic symbolic execution.This is identified as future work rather than part of the evaluated system.
  • Related work: Demand-driven sequence fuzzing relies only on greybox fuzzing and specifically targets smart contracts.The paper contrasts it with object-oriented method-call sequence generation using dynamic inference, static analysis, or evolutionary testing.

VIII. CONCLUSION

The conclusion presents HARVEY as an industrial greybox fuzzer for smart contracts that addresses two central fuzzing challenges. Its experiments report improved effectiveness from input prediction and demand-driven sequence fuzzing.

  • Contribution: HARVEY is an industrial greybox fuzzer for smart contracts.The paper presents it as the first greybox fuzzer for this domain.
  • Contribution: Input prediction and demand-driven sequence fuzzing alleviate the two key challenges encountered during HARVEY’s development.The techniques target input generation and stateful transaction-sequence exploration.
  • Findings: Experiments show that both techniques significantly improve HARVEY’s effectiveness and reveal insights about contract code.The conclusion states the result at the technique level without specifying a single benchmark metric.

APPENDIX

The appendix identifies the repositories used for the tested smart contracts and provides their changeset IDs and links.

  • Repository information: Appendix Table VI lists the smart-contract repositories used in the evaluation.The listed contracts are open source, with changeset IDs and repository links provided.
Loading 1905.06944v1…