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

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

首先, 智能合约是具有状态的程序 [15,31] , 与 C/C++语言从单一程序入口 (即 main 函数) 开始执行程序不同, 智
能合约对外界提供多个函数接口, 通过不同的事务序列 (即函数调用序列) 对合约内的状态变量进行修改, 从而使
合约达到不同状态. 若仅将疑似漏洞所在语句作为目标, 可能会导致无法满足目标语句 (即漏洞语句) 所在分支的
约束条件, 使符号执行错误地判断目标语句的可达性. 然而, 如果将状态变量假设为任意值, 会降低目标语句所在
分支可达性判断的准确性, 导致产生误报增加人工确认的成本.
其次, 可达性分析是目标制导符号执行技术中的关键步骤, 该步骤对控制流图进行剪枝以优化符号执行的路
径探索策略. 然而, 智能合约的控制流跳转信息无法直接获取, 需要根据字节码分析堆栈以构建控制流图; 并且, 静
态分析或人工标注通常仅提供目标语句的行号, 因此需要对目标信息进行处理, 基于编译器提供的映射关系定位
到目标基本块, 进而结合控制流图进行可达性分析.
针对上述挑战, 本文提出了一种基于目标制导符号执行的智能合约安全漏洞检测方法, 以 Solidity 语言编写
的智能合约为例, 借鉴现有目标制导符号执行技术的思想, 将其适配并应用到智能合约领域中. 针对目标语句所在
分支需要状态变量满足一定约束条件的情况, 本文通过分析目标依赖语句, 补充事务序列以添加相关变量的符号
约束, 提高目标语句所在分支可达性判断的准确性. 在可达性分析中, 根据字节码划分基本块并构建控制流图, 解
析源代码与字节码之间的映射关系, 定位目标语句并剪枝控制流图以生成制导信息, 优化符号执行的路径探索策
略, 减少时间开销并快速生成测试用例.
本文的主要贡献如下.
● 提出一种基于目标制导符号执行的智能合约安全漏洞检测方法. 该方法能够降低符号执行的时间开销, 提
高安全漏洞检测效率, 并能够快速生成覆盖指定目标的测试用例, 达到复现漏洞的目的.
● 提出目标依赖语句分析, 定位与目标语句存在控制依赖或数据依赖关系的语句, 补充事务序列以添加相关
变量的符号约束, 提高目标语句所在分支可达性判断的准确性.
● 实现了原型工具 Smart-Target (https://github.com/yagol2020/Smart-Target), 在 SB Curated (https://github.com/
smartbugs/smartbugs/tree/master/dataset) 人工标注数据集上与非目标制导的 Mythril 符号执行工具进行对比实验,
分析并评估了所提出方法的有效性.
本文第 2 节介绍相关工作. 第 3 节通过示例说明现有符号执行方法的局限性, 并引出本文所提方法的动机.
第 4 节给出智能合约语句、函数以及事务的符号化表示, 并详细介绍目标依赖语句分析、可达性分析以及目标制
导符号执行的具体流程. 第 5 节描述实验设计, 并对实验结果进行分析. 第 6 节讨论方法的泛用性以及有效性威
胁. 最后, 第 7 节总结全文, 并对未来工作进行展望.

2 相关工作

本节将从基于符号执行的智能合约安全漏洞检测方法和目标制导符号执行技术这 2 个方面介绍相关工作.
2.1 基于符号执行的智能合约安全漏洞检测方法
符号执行 [32,33] 在安全漏洞检测以及测试用例生成等领域被广泛应用 [34] . 基于符号执行的智能合约安全漏洞检
测方法将函数调用中的参数、调用者和携带以太币的数量等信息, 以及区块时间戳、块号和哈希值等区块链环境
信息使用符号值作为替换, 符号化执行智能合约的字节码指令, 收集路径分支的约束条件, 通过约束求解器对路径
条件进行求解, 判断路径分支的可达性, 并根据预先定义的漏洞模式判断路径条件是否满足漏洞触发条件, 从而进
行安全漏洞检测并输出触发漏洞的测试用例.
Luu 等人 [17] 构建了 Oyente 工具, 对智能合约中的重入、整型溢出以及时间戳依赖等漏洞进行了描述, 并通过
符号化表示各个漏洞模式, 从而能够利用符号执行对安全漏洞进行检测. 在 Oyente 的基础上, Chen 等人 [18] 构建
了 DefectChecker 工具, 在符号执行过程中构建堆栈事件, 提取金钱调用、循环体和支付函数 3 种特征检测安全漏
洞. Tsankov 等人 [19] 构建了 Securify 工具, 使用特定领域语言作为中间表示, 分析合约依赖关系以及语义信息, 利
用符号执行检查是否违反了预先定义的模式, 相较于 Oyente 能够达到更高的代码覆盖率.