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

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

解, 将会减少安全漏洞检测的时间开销. 此外, 针对静态分析工具仅提供疑似漏洞语句位置, 但缺少测试用例而
难以复现漏洞的场景, 如果将漏洞语句作为目标, 可利用符号执行快速生成对应的测试用例, 以帮助开发或测
试人员确认漏洞.

4 基于目标制导符号执行的智能合约安全漏洞检测方法
针对现有工作中符号执行检测效率较低问题, 本文提出了基于目标制导符号执行的智能合约安全漏洞检测方
法. 图 2 为方法的流程图, 共包括 3 个步骤, 即目标分析、可达性分析以及目标制导符号执行. 首先进行目标分析,
从静态分析、人工标注等途径获取源代码中的漏洞目标信息, 包括目标语句所在的行号以及漏洞类型等, 再通过
目标依赖语句分析, 获得与目标语句存在数据依赖或控制依赖的其他语句. 然后进行可达性分析, 将源代码编译为
字节码并进一步翻译为指令, 根据指令模拟构建堆栈, 分析跳转指令并构建智能合约控制流图, 将目标分析步骤中
得到的目标语句以及目标依赖语句作为分析对象, 定位其所在的基本块, 对控制流图进行剪枝以生成制导信息. 最
后进行目标制导符号执行, 根据制导信息判断下一步跳转基本块的可达性, 制导符号执行跳过与目标语句无关的
基本块, 并输出漏洞检测报告以及用于复现漏洞的测试用例.

漏洞目标
行号 漏洞类型 数据依赖
静态分析
27 重入
35 整型溢出
控制依赖
... ...
人工标注
目标依赖语句分析
目标获取
目标分析 目标语句
目标依赖语句
STOP
1 1
contract Owner{ ...
function check { JUMPI 目标制导
... 2 3 2 3 目标 漏洞检测报告
} ... 符号执行
} 0x40
4 4
0x80
智能合约源代码
指令与堆栈分析 控制流图构建 制导信息生成
测试用例
可达性分析
图 2 基于目标制导符号执行的智能合约安全漏洞检测方法流程图

本节的余下部分首先给出智能合约语句、函数以及事务的符号化表示, 然后介绍智能合约目标依赖语句分析、
可达性分析以及目标制导符号执行.
4.1 智能合约语句、函数以及事务的符号化表示
Solidity 智能合约的代码由任意数量的状态变量、结构体、枚举、事件、函数以及函数修饰器组成. 表 1 为
智能合约各代码结构的中英文名称和描述. 其中, 状态变量是用于持久存储数据的变量, 通常存储合约管理者、参
与者或代币价格等信息; 结构体和枚举能够定义新的数据类型或有限的数据集合; 事件能够调用 EVM 的日志接
口, 将合约的运行情况反馈给调用者; 函数和函数修饰器由任意数量的语句组成, 前者定义了智能合约的执行逻
辑, 后者用于修饰函数的执行, 带有函数修饰器的函数需要先执行修饰器的内容, 例如在执行函数前检查执行条件
是否满足.
根据语句执行的操作不同, 可将语句分为变量操作语句、假定语句、函数调用语句以及跳转语句. 同时, 根据
智能合约中状态变量存储结构的长度是否固定, 可分为定长类型状态变量 (如 uint、address 等) 和非定长类型状
态变量 (如动态数组、映射表等, https://docs.soliditylang.org/en/latest/internals/layout_in_storage.html). 由于上述 2