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

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

算法 2. 控制流图剪枝.
输入: 控制流图 cfg, 目标指令集合 target_ins;
输出: 剪枝过的控制流图.

1. visited = Set()
2. check(cfg.entrancy)
3. return cfg
4. Procedure bool check(bb):
5. if bb in visited:
6. return bb.targeted //若基本块被遍历过则返回目标值
7. visited.add(bb)
8. temp = false
9. for ins in target_ins:
10. if bb.start.pc ≤ ins ≤ bb.end.pc: //若目标指令位于该基本块中
11. bb.targeted = true //标记基本块的目标值为 true
12. temp = true //标记临时目标值为 true, 用于递归判断
13. break
14. for next_bb in bb.outgoing_bbs:
15. temp = check(next_bb) or temp //递归遍历, 并更新临时目标值
16. bb.targeted = temp //更新该基本块的目标值
17. return bb.targeted
算法 2 中第 1–3 行是算法的主体, 第 4–17 行是遍历控制流图的递归过程 check. 其中, check 以 cfg 的入口基
本块作为输入, 第 5–7 行判断该基本块是否被遍历过, 若遍历过则返回该基本块是否可达; 第 8 行声明临时变量
temp 用于表示基本块是否可达, 并赋初值为 false; 第 9–13 行遍历目标指令集合, 若该基本块包含目标指令, 则定
位该基本块为目标基本块, 标记该基本块为可达 (第 11 行), 并更新 temp 值为 true; 第 14, 15 行遍历跳转基本块,
递归调用 check 函数对其余基本块进行分析和标记可达性; 第 16, 17 行更新并返回该基本块的可达性.
算法 2 在递归过程中, 如果定位到目标基本块, 则 check 函数将返回 true. 根据 check 函数的返回值与临时变
量 temp 进行“或”操作 (第 15 行), 从而将目标基本块的所有父基本块均标记为可达, 得到从控制流图入口基本块
到目标基本块之间的路径. 各基本块的可达性信息可用于生成制导信息.
4.4 目标制导符号执行
目标制导符号执行指在符号执行判断跳转基本块是否需要被符号化执行前, 根据制导信息中对各基本块可达
性的标记情况, 跳过与目标语句无关的基本块, 减少求解路径条件的次数, 以及需要被分析的基本块数量, 达到提
高符号执行效率的目的.
如第 3.3 节所述, 智能合约中的控制流跳转由 JUMP 和 JUMPI 指令实现. 在符号执行的过程中, 遇到 JUMPI
指令时会复制当前路径条件, 分别添加分支条件为 true 和 false 的符号约束, 调用约束求解器分别对两个路径条件
的可满足性进行求解, 并将能够满足的路径条件所指示的基本块作为可达基本块, 进一步对该基本块进行符号化
执行. 本文在求解路径条件是否可满足之前, 根据制导信息中基本块的可达性进行判断, 若跳转基本块的可达性
为 false, 则不对其路径条件进行求解, 即剪枝该控制流路径.
智能合约目标制导符号执行的流程如算法 3 所示. 算法 3 的输入为第 3.3.2 节中得到的制导信息 target_info、
合约创建成功后的事务序列队列 trans_queue 以及事务序列的最大长度 limit, 算法 3 的输出为能够覆盖目标语句
的测试用例集合.