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

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

上述研究仅考虑了单一事务, 没有考虑对多个函数调用所组成的事务序列进行符号化分析. Mossberg 等人 [16]
基于 KLEE 构建了 Manticore 工具, 将事务的参数与携带的以太币数量等信息符号化, 重复地符号化执行事务从
而探索合约各个状态. Nikolić等人 [35] 构建了 Maian 工具, 提出贪心、自杀以及挥霍 3 种类型漏洞, 构建事务序列
并在符号执行过程中分析以太币转移和合约销毁相关的指令, 判断以太币转移的地址是否能被外部控制, 从而检
测安全漏洞. So 等人 [15] 提出了 SmarTest, 从已知存在漏洞的事务序列中得到统计模型, 并基于该统计模型判断候
选事务序列存在漏洞的概率, 选择概率较高的事务序列进行符号执行, 减少事务序列组合数量提高检测效率.
ConsenSys 构建了 Mythril 工具, 结合污点分析与符号执行技术, 能够对运行在 Ethereum、Hedera 和 Quorum 等兼
容 EVM 的区块链平台上的智能合约进行安全漏洞检测. Huang 等人 [36] 提出了动态符号执行框架, 构建了能够检
测整型溢出漏洞的 NOVA 和多事务漏洞的 MTVD, 为解决状态变量非均匀数据访问 (nonuniform data accesses) 不
精确的问题, 通过符号化状态变量的插槽序号, 生成具体值并结合哈希结果寻找状态变量存储的地址, 实验结果表
明 NOVA 和 MTVD 优于现有工具, 具有较高的召回率和较低的误报率.
Durieux 等人 [20] 以及 Ren 等人 [21] 的实证研究结果表明, 考虑了事务序列的符号执行方法相较于仅检测单一事
务的方法, 对代码的覆盖以及合约状态的探索更加充分, 通常能够检测出更多的漏洞. 但同时, 随着智能合约代码
规模的增长, 程序代码的分支数量以及事务序列的组合数量快速增多, 符号执行可能遇到路径爆炸问题, 导致约束
求解时间过长甚至失败, 对基于符号执行的安全漏洞检测方法的可扩展性以及漏洞检测能力产生较大的影响.
本文所提出的方法能够优化基于符号执行的智能合约安全漏洞检测, 通过目标制导符号执行技术缓解路径爆
炸问题对符号执行效率以及检测能力造成的影响, 剪枝与目标无关的路径与基本块, 减少需要被分析的代码规模、
调用约束求解的次数以及事务组合的数量, 提高了符号执行的检测效率.
2.2 目标制导符号执行技术
目标制导符号执行是一种能够有效缓解路径爆炸问题的技术手段, 利用静态分析等方式获得目标语句, 对控
制流图中各基本块的可达性进行分析, 剪枝与目标语句无关的基本块, 优化符号执行的路径探索策略, 高效地遍历、
分析并检测指定的基本块, 以提高符号执行的效率.
崔展齐等人 [30] 构建了 TARGET 工具, 将静态分析报告的疑似缓冲区溢出漏洞语句作为目标, 计算程序各分支
到可疑语句的可达性, 插桩待检测程序并进行目标制导动态符号执行检测, 实验结果表明相较于无目标制导的动
态符号执行方法, TARGET 能在更短的时间内发现更多的缓冲区溢出漏洞. 甘水滔等人 [28] 提出 OPT-SSE 方法, 根
据功能标签对程序进行切片, 分析程序控制流图并构建功能标签与基本块之间的映射关系, 对于给定的代码目标
点, 提取相关的功能标签切片并进行制导符号执行, 实验表明 OPT-SSE 能够提高符号执行的效率, 并且通过并行
的方式对多个程序功能切片进行符号执行能够提高整体分支和指令的覆盖率. Guo 等人 [37] 提出断言制导的剪枝框
架, 在符号执行过程中剪枝不会引发错误的路径, 并总结探索过程中无法覆盖错误语句的原因, 剪枝冗余路径减少
搜索空间, 同时针对并发程序提出了静态并发程序切片, 提高符号执行的效率.
目标制导符号执行技术还能够被应用于漏洞报告确认中, 减少误报率以及人工确认的成本, 同时生成能够复
现漏洞的测试用例. Ge 等人 [38] 构建了 DyTa 工具, 将静态分析和动态符号执行结合, 在静态分析阶段获得缺陷描
述以及潜在缺陷的位置, 基于缺陷描述中的预定义条件插桩被测代码; 在动态符号执行阶段, 当遇到需要对路径条
件翻转时, 根据静态分析的结果以及控制流图判断翻转后的路径是否能够达到存在潜在缺陷的代码, 若不能则不
进行翻转, 从而对探索状态空间进行剪枝. Li 等人 [39] 提出了静态内存泄露警报自动确认方法, 针对静态分析报告
的内存泄漏语句信息, 对目标程序进行控制流图分析并计算可达性, 生成制导信息, 在动态符号执行过程中监控内
存对象的状态, 判断内存泄漏是否发生, 减少确认漏洞报告的人工成本. 李筱等人 [40] 在文献 [39] 所提出方法的基
础上补充了与其他内存泄漏动态测试工具的对比试验, 并尝试将高覆盖率的测试用例作为动态符号执行的输入,
实验结果表明方法能够有效降低需要人工验证的警报数量, 并且在测试用例质量提高的情况下警报分类的准确性
更高. 鲍铁匀等人 [29] 同样利用目标制导符号执行技术对静态缓冲区溢出报告进行自动确认, 剪枝与漏洞无关的路
径, 制导符号执行沿特定确认路径执行, 能够减少 59.9% 的缓冲区溢出误报.