Effective Targeted Testing of Smart Contracts

TL;DR

This paper introduces Griffin, a targeted symbolic execution framework for smart contract testing that efficiently generates test data to reach specific code lines or safety conditions, addressing a gap in existing testing methods.

Contribution

The paper presents Griffin, a novel targeted symbolic execution tool tailored for smart contracts, including an enhanced CFG+ structure and heuristics for efficient test data generation.

Findings

Griffin effectively finds test data for smart contracts within reasonable time.

CFG+ improves the accuracy of control-flow analysis for Solidity.

Experimental results show Griffin's efficiency on real-world smart contracts.

Abstract

Smart contracts are autonomous and immutable pieces of code that are deployed on blockchain networks and run by miners. They were first introduced by Ethereum in 2014 and have since been used for various applications such as security tokens, voting, gambling, non-fungible tokens, self-sovereign identities, stock taking, decentralized finances, decentralized exchanges, and atomic swaps. Since smart contracts are immutable, their bugs cannot be fixed, which may lead to significant monetary losses. While many researchers have focused on testing smart contracts, our recent work has highlighted a gap between test adequacy and test data generation, despite numerous efforts in both fields. Our framework, Griffin, tackles this deficiency by employing a targeted symbolic execution technique for generating test data. This tool can be used in diverse applications, such as killing the survived mutants in mutation testing, validating static analysis alarms, creating counter-examples for safety conditions, and reaching manually selected lines of code. This paper discusses how smart contracts differ from legacy software in targeted symbolic execution and how these differences can affect the tool structure, leading us to propose an enhanced version of the control-flow graph for Solidity smart contracts called CFG+. We also discuss how Griffin can utilize custom heuristics to explore the program space and find the test data that reaches a target line while considering a safety condition in a reasonable execution time. We conducted experiments involving an extensive set of smart contracts, target lines, and safety conditions based on real-world faults and test suites from related tools. The results of our evaluation demonstrate that Griffin can effectively identify the required test data within a reasonable timeframe.