Page 375 - 《软件学报》2025年第12期

5756 软件学报 2025 年第 36 卷第 12 期

augmented with symbolic constraints for the relevant variables. Second, the control flow graph (CFG) is constructed based on the bytecode
of smart contracts, with the basic blocks containing the target statements and the dependentstatements located. The CFG is then pruned to
generate guidance information. Third, path exploration in symbolic execution is optimized by reducing the number of basic blocks to be
analyzed and reducing the time required for solving path constraints. With the guidance information, vulnerabilities are efficiently detected,
and test cases capable of reproducing the vulnerabilities are generated. Based on this approach, a prototype tool named Smart-Target is
developed. Experiments conducted on the SB Curated dataset in comparison with the symbolic execution tool, Mythril, demonstrate that
Smart-Target reduces time overheads by 60.76% and 92.16% in vulnerability detection and replication scenarios, respectively. In addition,
the analysis of target statementdependencies enhances vulnerability detection capability by identifying 22.02% more security vulnerabilities.
Key words: smart contract; symbolic execution; target-guided testing; security vulnerability detection; security vulnerability reproduction

1 引 言

随着区块链技术的发展, 众多领域都在探索利用区块链解决实际问题. 智能合约是运行在区块链平台上的计
算机程序 [1,2] , 能够按照预先定义的代码自动执行, 具有无需第三方信任、去中心化以及不可篡改的特性 [3] , 在金
融、物联网 [4] 以及智慧医疗 [5] 等领域被广泛应用. 然而, 由于其管理和存储数字资产, 吸引大量攻击者企图利用智
能合约中的安全漏洞非法窃取利益, 如 2016 年 TheDAO 合约被攻击, 造成价值 6 000 万美元的以太币被恶意转
移 (DAO 攻击事件, https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human); 2017 年 Parity 合约被
攻击, 导致价值 3 000 万美元的以太币被冻结或窃取 (Parity 攻击事件, https://hackingdistributed.com/2017/07/22/
deep-dive-parity-bug). 此外, 与传统软件不同, 智能合约一旦部署在区块链平台后将无法更新代码 [6] , 难以通过补丁
等方式对安全漏洞进行修复, 因此在部署智能合约前进行全面的安全漏洞检测尤为重要.
目前, 已有一些研究基于区块链以及智能合约的特点, 将静态分析 [7–9] 、模糊测试 [10,11] 、机器学习 [12,13] 、形式
化验证 [14] 以及符号执行 [15–19] 等软件分析与测试中较为成熟的技术应用到智能合约安全漏洞检测中, 已取得了较
好的检测效果. Durieux 等人 [20] 对 9 种静态分析和符号执行工具进行了实证研究, 结果表明静态分析工具 Slither [9]
和符号执行工具 Mythril (https://github.com/ConsenSys/mythril) 能够检测出较多的漏洞, 具有较好的漏洞检测能力.
Ren 等人 [21] 在 Durieux 等人的基础上更全面地从查准率、查全率等方面评估了 9 种静态分析、符号执行和模糊
测试工具的漏洞检测能力, 发现虽然 Slither 能够找到较多的漏洞, 但具有较高的误报率.
结合其他相关实证研究 [22] 及综述 [23–27] 可以发现: 基于静态分析的方法通常分析控制流、数据流或调用关系
等信息, 结合预先定义的漏洞模式或比较相似度等方式检测漏洞, 具有查全率高以及检测效率较快的优势, 但由于
对合约状态、路径条件或调用方式等进行了假设, 导致误报率较高; 基于符号执行或模糊测试的方法符号化或实
际部署并执行被测合约, 在检测过程中根据收集到的符号约束或执行信息判断是否存在安全漏洞, 具有更高的精
确度且能够生成复现漏洞的测试用例, 但检测所消耗时间较多.
目标制导符号执行能够利用静态分析查全率高以及符号执行精确度高的优势, 将静态分析报告的语句或函数
作为目标, 剪枝与目标无关的控制流路径, 优化符号执行的路径探索策略, 从而高效地覆盖和分析指定目标, 并检
测安全漏洞. 此外, 在漏洞复现场景中, 还可利用符号执行能够生成测试用例的特点, 将人工标注的漏洞语句作为
目标, 快速地生成能够触发漏洞的测试用例, 从而帮助开发或测试人员复现漏洞.
目标制导符号执行技术在缺陷检测以及确认等场景已有较多的研究与应用. 甘水滔等人 [28] 从程序功能文档
提取功能标签, 结合控制流信息构建各功能标签和程序基本块之间的映射关系, 针对给定的目标点对程序进行切
片, 并剪枝无关的功能分支提高制导效率. 鲍铁匀等人 [29] 根据静态分析的缺陷报告剪枝控制流图中与缓冲器溢出
无关的路径, 制导符号执行沿着特定路径探索, 通过约束求解对静态分析的报告进行确认. 我们在前期研究中将静
态分析所报告的可疑语句作为目标, 制导动态符号执行并生成覆盖待检测缺陷语句的测试输入, 提高了缺陷检测
的效率 [30] . 然而, 上述研究主要针对基于 C/C++等语言编写的软件, 智能合约则是由 Solidity 等程序设计语言编写,
且运行在区块链环境中, 与 C/C++等语言编写的程序在语法、语义、运行平台和运行机制上具有较大差异. 将目
标制导符号执行技术应用到智能合约中面临两个研究挑战.