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

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

需要注意的是, 算法 3 中第 2 行和第 4 行的 trans_queue.pop 函数和 state_queue.pop 函数分别对应事务序列
的生成策略和合约状态的探索策略, 这 2 种策略的优化方法是符号执行以及智能合约研究工作中的重点 [43] , 如
SmarTest [15] 基于语言模型判断事务序列触发漏洞的概率, 优先执行较高概率的事务序列以缓解组合爆炸问题;
Smartian [31] 基于数据依赖关系生成事务序列, 通过随机插入函数调用等策略对事务序列进行变异, 以增加模糊测
试过程中对智能合约代码的覆盖率; Mythril 可选择深度优先、广度优先或随机路径选择等策略遍历合约状态;
KLEE [44] 采用随机路径选择并结合覆盖率优化搜索策略探索程序路径空间等.
本文所提出的方法不依赖于特定的事务序列生成策略或合约状态探索策略, 在算法 3 中可尝试应用不同的事务
序列生成策略或合约状态探索策略以达到更高的安全漏洞检测效果. 在算法 3 中, 目标制导符号执行策略主要体现
在第 8 行和第 12 行, 即在探索合约状态时剪枝无法到达目标语句的基本块, 减少需要被探索的合约状态数量, 以达
到优化合约状态探索策略的目的. 同时, 若通过可达性分析判断某一函数与目标语句无关, 则制导信息中会将该函数
对应的基本块设置为不可达, 不会将该函数添加至事务序列, 从而减少事务组合的数量以提高安全漏洞检测效率.
接下来以 Mythril 使用的事务序列生成策略为例, 描述目标制导符号执行方法如何优化现有的事务序列生成
策略. Mythril 默认采用广度优先策略, 根据字节码中函数基本块出现的顺序对各函数进行探索, 在遇到 REVERT
或 RETURN 等终止指令后, 记录当前符号状态并选择另一个函数继续执行. 当合约内所有函数均被符号化执行
后, Mythril 还原首个函数执行后的符号状态, 并再次根据函数基本块的顺序进行探索, 直到代码覆盖率无法提升
或达到事务序列的最大长度.
图 4 中红色矩形表示已经符号化执行的函数调用, 蓝色矩形表示候选函数调用. 若蓝色矩形右上角存在“ ⊗ ”
符号标记, 则表示该函数与目标语句无关, 无需对其进行符号化执行. 由图 4 可以看出, func2 函数被标记为与目标
语句无关, 因此在符号执行过程中不会对该函数进行探索. 具体来讲, 当事务序列长度为 2 时, 若采用 Mythril 默认
2
2 2 = 4 种事务序列即可. 随着事务
策略, 则需要执行 3 = 9 种事务序列; 而通过目标制导过滤无关函数后, 仅需执行
序列长度的增加, 目标制导所带来的效率提升会更加明显.

func1 func1
func1
func1 func2 func1 func2 func1
init func2
init func2 func3 init func2 func3 ··· func2
func3
func3 func3 func3
事务序列长度=1 事务序列长度=2 事务序列长度=n
图 4 目标制导符号执行事务序列生成策略示意图

4.5 示例分析

本节以第 2 节中图 1 所示的代码为例, 说明本方法的主要流程. 根据 CVE 的信息, 我们将第 72 行和第 90 行
语句作为目标, 然后进行目标依赖语句分析、可达性分析以及目标制导的符号执行.
首先进行目标依赖语句分析, 通过分析源代码得知, 第 72 行的目标依赖语句为第 71、79、88、89 和 90 行,
第 90 行的目标依赖语句为第 88 行和第 89 行. 由此可知, 第 72 和 90 行这 2 条目标语句的目标依赖语句为第 71、
79、88 和 89 行.
第 2 步进行可达性分析, 将源代码编译为字节码并划分基本块, 通过分析跳转指令构建控制流图, 图 5(a) 为该
合约代码的控制流图, 其中每个节点对应各个基本块, 节点上的序号为基本块中首个指令的序号. 然后, 通过编译
器提供的 Source Mappings 定位目标语句以及目标依赖语句的基本块, 定位的结果如表 4 所示, 即 1371、1826、
1837、2529、2542 和 2634 共 6 个基本块为目标基本块. 根据上述定位的 6 个目标基本块遍历并剪枝控制流图,
剪枝后的控制流图如图 5(b) 所示, 其中红色节点表示目标语句所在的基本块, 绿色节点表示目标依赖语句所在的