Effective Targeted Testing of Smart Contracts
Mahdi Fooladgar, Fathiyeh Faghih
TL;DR
The paper tackles the gap between test adequacy and test-data generation for Solidity smart contracts by introducing Griffin, a targeted symbolic execution framework. Griffin uses an enhanced CFG+ that captures EVM state and transaction history to find minimal satisfiable walks from a target line back to contract creation under safety constraints, powered by SMT solvers and SSA-based representations. It provides a complete prototype with Slither-derived IRs, a configurable heuristic (including Floyd-Warshall and state-variable-based strategies), and the ability to generate concrete EVM transactions to reach specific code lines while satisfying safety conditions. Evaluation on 12 real-world contracts demonstrates Griffin’s ability to identify required test data within reasonable timeframes, highlighting the impact of heuristic choice on performance and the potential to integrate with static-analysis alarms and mutation-testing workflows.
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.