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

杨慧文 等: 基于目标制导符号执行的智能合约安全漏洞检测 5771

在时间消耗方面, Slither 漏洞检测所需时间为 25.83 s, Smart-Target 所需的时间为 92 174.76 s, Mythril 所需的
时间为 234 884.44 s. 相较于 Slither 仅分析源代码的语法语义, Mythril 逐条指令进行符号化执行, 收集路径条件并
对其进行求解以分析可达性, 因此 Mythril 所需的时间远大于 Slither. 而 Smart-Target 通过目标制导优化符号执行
的路径探索策略, 跳过了与目标语句无关的基本块, 减少了需要分析的指令数量以及路径条件求解的次数, 因此相
对于非目标制导的 Mythril, Smart-Target 节省了 60.76% 的时间开销.
在安全漏洞检测能力性能比较上, Slither 的 F1 值为 0.828, Mythril 的 F1 值为 0.793, Smart-Target 的 F1 值为
0.788. 其中, Smart-Target 与 Mythril 的 FP 相同, TP 相差 1. 分析发现, Smart-Target 比 Mythril 少检测到的漏洞为
未检查低级调用漏洞, 该漏洞语句 (ClockAuction#1496, https://github.com/smartbugs/smartbugs/blob/master/dataset/
unchecked_low_level_calls/0x663e4229142a27f 00bafb5d087e1e730648314c3.sol#L1496) 没有被 Slither 报告为漏洞,
因此 Smart-Target 没有将其设置为目标, 导致漏报. 当把该漏洞语句作为目标时, Smart-Target 能够检测出该漏洞.
上述结果表明, Smart-Target 在安全漏洞检测能力上与 Mythril 相同, 并没有因为剪枝控制流图而降低漏洞检测能力.
从表 7 可以看出, Slither 比 Mythril 和 Smart-Target 能够检测出更多漏洞. 但是在安全漏洞分析、定位和修复
的应用场景上, 由于 Slither 仅能报告漏洞类型以及漏洞所在行数, 相较于 Mythril 和 Smart-Target 缺少生成测试用
例复现漏洞的能力. 实验结果显示, Smart-Target 和 Mythril 分别生成了 95 和 96 个测试用例, 其中除了生成触发人
工标注的漏洞 (即 TP) 之外, 还在重入以及时间操作的漏洞检测过程中为 4 个未被数据集标注的语句生成了测试
用例. 分析发现, 其中 1 个测试用例触发了未涉及以太币转移的重入行为, 另外 3 个触发了人工标注的漏洞, 但由
于人工标注的语句不完整 (如仅标注函数调用语句或时间戳的声明语句), 导致报告的漏洞位置未能与数据集中人
工标记的语句匹配. 上述结果表明, 相较于 Slither 仅提供漏洞所在位置, Smart-Target 和 Mythril 能够生成测试用
例触发相应的安全漏洞, 并且 Smart-Target 能够为 Slither 检测出的 111 个安全漏洞中的 91 个生成对应的测试用
例, 成功生成测试用例的比例达 81.9%.
表 7 中最后一列统计了各工具生成和执行事务序列的数量, 从中可以看出, 静态分析工具 Slither 相较于符号
执行工具 Mythril 和 Smart-Target 缺少生成并执行事务序列的能力, 因此在检测存在多个函数的复杂智能合约时,
难以为开发或测试人员复现、理解和修复漏洞提供有效的帮助. 相较于 Mythril 共执行了 4 635 条事务序列, Smart-
Target 在仅执行了 2 414 条测试用例的情况下, 检测出与 Mythril 相同数量的安全漏洞, 这是因为 Smart-Target 能
够通过可达性分析将与目标语句无关的函数基本块设置为不可达, 因此在目标制导符号执行过程中能够过滤掉无
关函数, 从而减少事务的组合数量以及需要执行事务序列数量. 随着需要执行的事务序列数量减少, 符号执行的时
间开销也相应减少, Smart-Target 的时间开销相较于 Mythril 减少了 60.76%.
此外, 由于 Slither 未考虑上下文约束, 相较于 Mythril 和 Smart-Target 产生了较多误报. 图 6 为一个 Slither 误
报的重入漏洞代码示例 (spank_chain_payment, https://github.com/smartbugs/smartbugs/blob/master/dataset/
reentrancy/spank_chain_payment.sol). Slither 报告了第 803–806 行存在重入漏洞, 但实际上 804 行的外部函数调用
需要满足第 802 行的 if 条件, 该条件需要 tokenbalanceA 或 tokenbalanceI 不为 0. 当 channel.token.transfer 函数存
在重入行为时 (channel.token 存储 HumanStandardToken 类, 该类的 transfer 函数可能由攻击者重写, 从而引发重
入), 由于第 794 行和第 795 行已将值设置为 0, 因此 tokenbalanceA 和 tokenbalanceI 均为 0, 无法满足第 802 行的
函数条件, 即无法引发重入漏洞. 由于 Slither 未考虑语句的上下文, 因此误报了 803 行的漏洞. 而 Mythril 和 Smart-
Target 能够收集 channel 结构体中各个成员变量的符号值, 在第 1 次执行第 792–795 行时, 将 channel 中相关的成
员变量数组的符号值置为 0, 在重入过程中判断第 802 行的路径条件无法满足, 因此能够正确判断该智能合约中
不存在重入漏洞.
还需要注意的是, Smart-Target 是基于 Mythril 实现的安全漏洞检测工具, 仅在 Mythril 的基础上优化了路径
探索的策略, 而没有改变或增强漏洞检测逻辑 (Oracle), 因此 Smart-Target 的安全漏洞检测能力依赖于 Mythril. 若
将本文所提出的目标制导符号执行方法应用到其他符号执行工具中, 如 SmartTest [15] 、Manticore [16] 或 Oyente [39] 等,
可能会取得更高的安全漏洞检测能力.
综上所述, 我们对 RQ1 的回答是: 在安全漏洞检测场景中, 相较于静态分析工具 Slither, Smart-Target 减少了