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.
翻译:智能合约是部署在区块链网络上并由矿工运行的自主且不可更改的代码片段。它们最初由以太坊于2014年引入,此后被广泛应用于多种场景,如安全代币、投票、博彩、非同质化代币、自主身份管理、库存盘点、去中心化金融、去中心化交易所以及原子交换。由于智能合约具有不可更改性,其存在的缺陷无法修复,这可能导致重大的经济损失。尽管许多研究者致力于智能合约测试,我们近期的研究揭示了测试充分性与测试数据生成之间存在差距,尽管这两个领域均已付出大量努力。我们的框架Griffin通过采用定向符号执行技术来生成测试数据,以应对这一不足。该工具可应用于多种场景,例如在变异测试中清除存活变异体、验证静态分析警报、为安全条件生成反例,以及到达手动选定的代码行。本文探讨了在定向符号执行中智能合约与传统软件的差异,以及这些差异如何影响工具结构,从而促使我们提出了一种针对Solidity智能合约的增强版控制流图——CFG+。我们还讨论了Griffin如何利用自定义启发式方法探索程序空间,在合理执行时间内考虑安全条件的同时,找到能够到达目标代码行的测试数据。我们基于现实故障及相关工具的测试套件,开展了涉及大量智能合约、目标代码行和安全条件的实验。评估结果表明,Griffin能够在合理时间范围内有效识别所需的测试数据。