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

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

然而, 现有的目标制导符号执行技术通常以 C/C++程序作为分析对象, 难以直接应用到智能合约领域中, 一方
面是因为智能合约具有状态变量且能够通过不同的事务序列对合约状态进行修改, 相较于单一入口的 C/C++程序
具有更多程序状态. 另一方面从智能合约字节码中无法直接提取控制流信息以及定位目标基本块, 需要进一步结
合编译器提供的信息进行分析. 本文通过分析目标依赖语句, 添加与目标相关变量的符号约束, 基于字节码构建控
制流图并分析编译器提供的 Source Mappings 定位目标基本块, 将目标制导符号执行技术适配、改进并应用到了
智能合约安全漏洞检测领域, 实验结果表明能够提高安全漏洞检测效率并高效生成测试用例.

3 研究动机示例

本节以一个真实的智能合约为例说明研究动机. 图 1 为存在整型溢出漏洞的智能合约代码片段 (PFG, https://
etherscan.io/address/0xa2c4f961b93fc7bc200d2c8e55b6fe6958366787#code), 根据 CVE 以及相关引用的信息 (CVE-
2018-13328, https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2018-13328), 该示例中第 72 行和第 90 行存在整
型溢出漏洞. 整型溢出漏洞指经过运算的结果超出了存储变量数据类型的最大存储范围, 第 41 行 balances 存储的
数据类型为 uint256, 即存储范围为 0 至 2 256 −1. 如果_value 或 amount 中存储的数值过大, 又或 balances 已存储较
大的数值, 都将可能引发整型溢出漏洞, 导致 balances 中记录的数据出现错误, 进而引发代码逻辑错误. 整型溢出
漏洞是智能合约中常见漏洞之一 [41] , 且由于智能合约能够存储和管理区块链上的数字资产, 因此数值类型的数据
更应被重视, 应在合约部署前对智能合约中的整型溢出、除零或算术符号错误等安全漏洞进行全面的检测.

41 mapping (address => uint256) balances;
42 mapping (address => mapping (address => uint256)) allowed;
70 function transferFrom(address _from, address _to, uint256 _value) public {
require(balances[_from] >= _value && allowed[_from][msg.sender] >= _value && _value >
71
0);
72 balances[_to] += _value; //整型溢出
73 balances[_from] -= _value;
74 allowed[_from][msg.sender] -= _value;
75 Transfer(_from, _to, _value);
76 }
78 function approve(address _spender, uint256 _value) public {
79 allowed[msg.sender][_spender] = _value;
81 }
87 function mint(uint256 amount) public {
88 assert(amount >= 0);
89 require(msg.sender == owner);
90 balances[msg.sender] += amount; //整型溢出
91 totalSupply += amount;
92 }
图 1 存在整型溢出漏洞的智能合约代码片段

此外, 该 CVE 中没有提供相应的测试用例用于复现所提到的安全漏洞, 难以判断引发整型溢出漏洞的具体原
因 (如未限制_value 大小、balances[_recipient] 在其他函数被错误赋值等), 对安全漏洞的修复缺少有效的帮助
信息.
符号执行能够有效地检测整型溢出等与数值相关的漏洞. 例如, 使用 Mythril 工具可在运行 560.8 s 后检测出
第 72 行和第 90 行存在整型溢出漏洞, 并生成了对应的测试用例. Mythril 在符号执行分析过程中, 约束求解器分
析路径条件所消耗的时间为 457.8 s.
然而, 并非该合约中所有的代码均与该漏洞相关, 该合约中未在图 1 展示的其余 2 个函数 (balanceOf 和
allowance) 以及 2 个事件 (Transfer 和 Approval) 用于输出合约的状态变量以及调用日志接口, 不会影响或触发
漏洞. 直接使用符号执行进行安全漏洞检测将会对该合约中的所有代码进行分析, 不能充分利用 CVE、人工
标注或静态分析提供的信息. 如果能在安全漏洞检测之前, 通过静态分析等方式获得疑似漏洞的位置, 将其作
为目标, 剪枝控制流图中与目标无关的路径, 仅对目标语句相关的基本块或路径条件进行符号执行和约束求