PaperlayerView exact revision on arXiv

Source-linked AI summary

How Effective are Smart Contract Analysis Tools? Evaluating Smart Contract Static Analysis Tools Using Bug Injection

Asem Ghaleb, Karthik Pattabiraman

arXiv:2005.11613v1cs.SE

TL;DR

Smart-contract security bugs can cause irreversible financial losses, yet static-analysis tools lack a systematic evaluation method. The paper proposes SolidiFI, which injects exploitable bug patterns throughout Solidity contracts and evaluates analysis tools. Across six tools, SolidiFI exposes substantial undetected bugs and many false positives, while identifying gaps useful for future tool development.

  • Problem

    Smart-contract bugs can cause irreversible financial losses, while existing static-analysis tools lack a systematic method for evaluating their effectiveness.

  • Method

    SolidiFI injects predefined exploitable security-bug patterns into all possible locations in Solidity contracts and analyzes the resulting contracts with static-analysis tools.

  • Results

    SolidiFI evaluated six tools and found substantial undetected bugs within claimed detection scopes, along with many false positives.

  • Takeaways & Limitations

    SolidiFI provides a reproducible set of tests that identifies gaps in current smart-contract static-analysis tools for developers of future tools.

  • Takeaways & Limitations

    The evaluation considers only six tools and seven bug types, and the current SolidiFI version works only with Solidity static-analysis tools.

Abstract

from arXiv · show

Security attacks targeting smart contracts have been on the rise, which have led to financial loss and erosion of trust. Therefore, it is important to enable developers to discover security vulnerabilities in smart contracts before deployment. A number of static analysis tools have been developed for finding security bugs in smart contracts. However, despite the numerous bug-finding tools, there is no systematic approach to evaluate the proposed tools and gauge their effectiveness. This paper proposes SolidiFI, an automated and systematic approach for evaluating smart contract static analysis tools. SolidiFI is based on injecting bugs (i.e., code defects) into all potential locations in a smart contract to introduce targeted security vulnerabilities. SolidiFI then checks the generated buggy contract using the static analysis tools, and identifies the bugs that the tools are unable to detect (false-negatives) along with identifying the bugs reported as false-positives. SolidiFI is used to evaluate six widely-used static analysis tools, namely, Oyente, Securify, Mythril, SmartCheck, Manticore and Slither, using a set of 50 contracts injected by 9369 distinct bugs. It finds several instances of bugs that are not detected by the evaluated tools despite their claims of being able to detect such bugs, and all the tools report many false positives

1 INTRODUCTION

Smart contracts create high-stakes security risks, while existing static-analysis tools lack systematic evaluation. SolidiFI addresses this gap by injecting exploitable bugs and evaluating six tools, revealing substantial undetected bugs and false positives.

  • Smart-contract bugs can cause irreversible financial losses because Ethereum transactions cannot be reverted and deployed contracts are difficult to update.
  • Existing static-analysis tools have been evaluated mainly by developers on ad-hoc datasets or datasets containing few bugs, leaving no systematic evaluation method.
  • SolidiFI systematically evaluates false negatives and false positives by injecting exploitable security-bug snippets into all possible Solidity source-code locations.
  • SolidiFI evaluates six Ethereum smart-contract static-analysis tools and provides analysis of undetected bugs, false positives, and their underlying reasons.
  • 129 to 4137 undetected bugs occurred across seven bug types, and all evaluated tools reported many false positives on 50 contracts.

2 BACKGROUND

Smart contracts are Solidity programs compiled to EVM bytecode and executed on blockchain networks, while automated static analysis tools inspect them for security bugs. The paper considers six freely available, annotation-free tools for this task.

  • Smart contracts: Solidity smart contracts are compiled into EVM bytecode, deployed in blockchain accounts, and executed by mutually untrusted miners under blockchain consensus.Users pay gas execution fees to miners who run submitted transactions.
  • Example contract: The example contract implements a public money-based guessing game in which incorrect guesses transfer funds to the last winner and correct guesses establish a new winner.Its constructor initializes the winner and start time when the contract is created.
  • Terminology: SolidiFI is an abbreviation for Solidity Fault Injector.The paper notes that the name is pronounced “Solidify.”
  • Analysis tools: The study considers six automated, freely available Solidity analysis tools that require no programmer annotations: Oyente, Securify, Mythril, SmartCheck, Manticore, and Slither.Four tools were selected partly because they had been used in many smart-contract analysis studies.

3 MOTIVATION AND CHALLENGES

Motivating examples show that static analyzers can miss vulnerabilities they claim to detect, motivating systematic bug injection. SolidiFI addresses injection challenges by targeting syntactically valid locations and constructing exploitable snippets aligned with bug types.

  • Motivating examples: The motivating contract contains two timestamp-dependency instances and one transaction-ordering-dependence bug.The timestamp issue concerns using a block timestamp in a transaction, while TOD concerns relying on contract state.
  • Motivating examples: Oyente and Mythril missed both timestamp-dependency instances, although their papers claim they should detect this bug; SmartCheck was also evaluated.The passage reports the tools’ claimed detection capability and observed misses.
  • Motivating examples: Securify detected the TOD bug, whereas Oyente did not, and injecting the same snippet into a larger bug-free contract produced similar results.Both tools were expected to detect this bug class.
  • Evaluation challenge: Manual injection into five contracts revealed additional undetected bugs but was tedious and error-prone, motivating an automated approach.The examples used code snippets for different bugs and were checked with the analysis tools.
  • Injection challenges: Random injection is not cost-effective because injected bugs must satisfy exploitability guidelines and account for contract-specific control and data flow.Each bug should be injected into all potential code locations, while incorrect locations can cause compilation errors or dead code.
  • SolidiFI approach: SolidiFI parses Solidity into an AST to inject bugs at all syntactically valid locations and formulates exploitable snippets for each bug type.These mechanisms address location validity and alignment with the original contract’s semantics.

4 SOLIDIFI APPROACH AND WORKFLOW

SolidiFI evaluates smart-contract static-analysis tools by injecting targeted vulnerabilities into Solidity contracts, analyzing the resulting buggy contracts, and measuring missed and spurious reports.

  • Workflow: SolidiFI injects security-bug code snippets into potential locations throughout Solidity source code before running evaluated analysis tools.The injected snippets represent exploitable vulnerabilities, and the approach can also target tools analyzing compiled EVM bytecode.
  • Workflow: The workflow identifies injection locations, generates buggy contracts, scans them with static-analysis tools, and measures false negatives and false positives.Injection locations depend on the bug type, while tool results are inspected against the injected bugs.
  • Bug Injection: SolidiFI uses full code snippets to introduce vulnerabilities such as timestamp dependency, unhandled exceptions, integer overflow/underflow, tx.origin authentication, re-entrancy, unchecked send, and transaction-ordering dependency.The approach prepares multiple snippets for each bug under study and applies them at relevant code locations.
  • Bug Injection: Pattern-based transformation introduces integer overflow/underflow and tx.origin bugs while preserving the surrounding code’s functionality.The transformation replaces known code patterns with vulnerable patterns.
  • Bug Injection: Security-protection weakening introduces unhandled-exception bugs by removing mechanisms such as revert() after failed transfers.In the example, removing the revert() statement can leave the contract balance incorrectly set to zero after a failed transfer.

5 SOLIDIFI ALGORITHM

The SolidiFI algorithm derives bug-specific injection locations from a contract’s AST, injects bugs at all marked locations, and compares tool reports with the injected-bug log.

  • Algorithm: SolidiFI first identifies potential injection locations and creates an annotated AST marking them.The locations are determined by the bug type and code-snippet form.
  • Algorithm: It injects bugs into all marked locations to generate buggy contracts, using AST-derived information for text-based code transformation.The Bug Injector seeds a bug for each location specified in the bug injection profile.
  • Injection Locations: The algorithm’s location profile combines AST walks with searches for related security mechanisms and transformable code patterns.Algorithm 1 returns the bug injection profile after processing snippet forms and related code structures.
  • Injection Locations: Rules connect each bug type with compatible contract structures, including individual statements, stand-alone functions, and non-function blocks such as if statements.These rules guide the identification of locations without invalidating compilation.
  • Results Inspection: The resulting buggy contracts are passed to evaluated tools, whose reports are checked against the BugLog for injected but undetected bugs and false alarms.SolidiFI focuses on injected bugs that remain undetected during results inspection.

6 IMPLEMENTATION

SolidiFI automates compilation, bug injection, tool execution, and report inspection, using solc and Python components to support reusable analysis.

  • Implementation: SolidiFI is fully automated except for preparing the buggy snippets and manually validating filtered false positives.Automation covers compilation, buggy-contract generation, tool execution, and report inspection.
  • Implementation: The system uses solc to verify compilation and generate the original contract’s JSON-formatted AST.The supported compiler versions extend up to 0.5.12.
  • Implementation: The remaining SolidiFI components are implemented in Python in approximately 1500 lines of code.These components identify injection locations and perform the other stages of the injection workflow.

7 EVALUATION

The evaluation applies SolidiFI to a benchmark of smart contracts and injected bug types, then measures static-analysis false negatives, false positives, exploitability, and injection performance. Across the evaluated tools, substantial detection gaps and false-positive counts remained, while SolidiFI injected bugs in under a minute on average.

  • Evaluation setup: 50 contracts covering seven bug types were evaluated against six static analysis tools, with contract sizes ranging from 39 to 741 lines of code.The contracts averaged 242 lines of code; the selected tools were Oyente, Securify, SmartCheck, Mythril, Manticore, and Slither.
  • Evaluation setup: The experiments injected bugs, tested the resulting contracts with the evaluated tools, and inspected reports for undetected injected bugs and false positives.SolidiFI records injection locations so detected and undetected injected bugs can be compared against known ground truth.
  • False negatives: All evaluated tools produced significant false negatives, and none detected every injected bug correctly across the tested bug types.Slither achieved 100% coverage only for the individual Reentrancy and tx.origin bug types, while Slither had the fewest false negatives overall, followed by Securify.
  • False positives: False-positive counts ranged from 2 to 801 for most bug types, including substantial false-positive reporting by tools with fewer false negatives.Examples included reports for handled exceptions, protected reentrancy cases, and apparent integer overflows without integer calculations.

8 DISCUSSION

The discussion explains why evaluated tools missed injected vulnerabilities, then draws implications for tool developers and smart-contract users while noting SolidiFI’s limitations and validity threats.

  • 8.1 Reasons for False-Negatives: Oyente missed multiple bug types because bounded, incomplete symbolic execution may fail to generate the execution paths needed to expose them.Its analysis compares symbolic traces and Ether flows to detect transaction-ordering dependencies.
  • 8.1 Reasons for False-Negatives: SmartCheck’s XPath-pattern approach missed most injected bugs because some vulnerabilities, including re-entrancy, are difficult to express as XPath patterns.The approach constructs an intermediate representation before searching it with XPath patterns.
  • 8.1 Reasons for False-Negatives: Mythril had the largest set of undetected bugs, and increasing its timeout from 15 to 30 minutes did not increase detections as symbolic-trace enumeration scaled poorly.Undetected bugs increased in large contracts because Mythril enumerates symbolic traces.
  • 8.1 Reasons for False-Negatives: Mythril also misreported injected re-entrancy as an unchecked call return value even though the send result was checked and the balance reset after success.This example raises questions about Mythril’s soundness for the reported bug type and completeness for re-entrancy detection.
  • 8.1 Reasons for False-Negatives: Manticore failed to detect re-entrancy and integer overflow/underflow, while crashing on 83 re-entrancy-injected and 73 integer-overflow-injected contracts.It also timed out, consumed substantial memory, and threw exceptions on many contracts.
  • 8.1 Reasons for False-Negatives: The evaluation found substantial tool failures: Securify missed bugs and failed on injected contracts, Slither missed unhandled exceptions, and all tools produced false positives.Securify’s reported undetected counts included 105 re-entrancy, 332 unchecked-send, 402 unhandled-exception, and 136 TOD bugs after excluding failed analyses.
  • 8.2 Implications: Tool developers should move beyond simple pattern matching and symbolic-trace enumeration toward analyses that incorporate Solidity and EVM semantics.The discussion identifies formal-methods combinations as one possible direction.
  • 8.2 Implications: Developers should not rely exclusively on static analysis; SolidiFI can help assess tools, build mutation-based test suites, and teach secure coding.The generated bugs and their code locations can support developer education.

9 RELATED WORK

Related work has evaluated bug-finding tools through mutation, taint analysis, and annotated vulnerable contracts. SolidiFI differs by systematically injecting exploitable bugs across all potential contract locations rather than relying on limited or tool-dependent samples.

  • Bug-Finding Tools Evaluation: Mutation-based evaluation frameworks have previously been applied to Android and traditional programs by inserting security operators or modifying vulnerable locations.These approaches provide precedent for evaluating static-analysis tools through injected defects.
  • Bug-Finding Tools Evaluation: LAVA injects guarded vulnerabilities triggered by specific inputs, whereas SolidiFI transforms otherwise invulnerable code into systematically exploitable code.LAVA uses dynamic taint analysis and supplies triggering inputs with injected bugs.
  • Bug-Finding Tools Evaluation: Akca et al. compared smart-contract analyzers using a single hard-coded injected bug, unlike SolidiFI’s injection into all potential contract locations.Their tool uses Fault Seeder to generate contract mutants.
  • Bug-Finding Tools Evaluation: Durieux et al. evaluated tools on 69 manually annotated contracts containing 112 bugs, but the repository sources were not agnostic to the evaluated tools and could bias results.The paper contrasts this with its systematic injection strategy.
  • Smart Contract Testing and Exploitation: Other related work addresses smart-contract testing, fuzzing, and automatic exploit generation rather than systematic static-analysis evaluation.Examples include mutation-based test generation, fuzz-testing services, and symbolic-execution-based exploit generation.

10 CONCLUSION

SolidiFI systematically evaluates Ethereum smart contract static analysis tools by injecting predefined bug patterns throughout contract ASTs. Future work will extend it beyond Solidity and automate the definition of new bug types.

  • SolidiFI analyzes smart-contract ASTs and injects predefined bug patterns at all possible AST locations.It was used to evaluate six smart contract static analysis tools.
  • The evaluation found cases of bugs that the assessed tools failed to detect despite their claimed detection capabilities.
  • Future work will expand SolidiFI to smart contract languages beyond Solidity.
  • Future work will automate the bug-definition process for injecting new bug types.
Loading 2005.11613v1…