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

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

由 mint、approve 以及 transferFrom 这 3 个函数调用所组成的其他 26 种事务序列同样可能触发第 72 行所示
的漏洞. 本文所提出的目标制导符号执行方法能够减少事务序列的组合数量, 具体描述和讨论见本文第 4.4 节.
上述示例中, 第 71、79 和 90 行的语句为第 72 行目标语句的目标依赖语句. 通过符号化执行目标依赖语句,
可以更准确地判断目标语句的可达性. 为了更准确地描述目标依赖语句, 本文参考 Wang 等人 [42] 关于依赖关系的
定义, 对智能合约中的数据依赖和控制依赖进行了定义.
定义 1 (数据依赖). 对于智能合约中的语句 stmt i 和 stmt j , 若 stmt i 对变量 进行赋值, stmt j 读取 v, 且由 stmt i
v
到 stmt j 的路径中不存在语句 stmt k 对 v 进行赋值, 即 stmt j 读取的变量数值依赖于 stmt i 的赋值操作, 称 dataDep(stmt i ,
( )
stmt j ) = T; 否则 dataDep stmt i , stmt j = F.
定义 2 (控制依赖). 对于智能合约中的语句 stmt i 和 stmt j , 其中 stmt j 是函数 func 中的语句, 若 (1) stmt i 为
stmt j ; 或 (2) stmt i 为函数修饰器中的分支语句, 且对应判定条
func 中的分支语句, 且对应判定条件满足时才能执行
( )
件满足时才能执行函数 func, 即 stmt j 的执行受到 stmt i 的控制, 称 controlDep stmt i , stmt j = T; 否则 controlDep(stmt i ,
stmt j ) = F.
需要注意的是, 智能合约的函数修饰器能够改变函数的行为, 从而影响语句的执行. 例如图 3 中函数 abort 函
数被函数修饰器 onlySeller 所修饰 (https://docs.soliditylang.org/en/latest/structure-of-a-contract.html#function-
modifiers). onlySeller 通过 require 判断函数的调用者是否为 seller, 若不是则引发异常并输出信息, 若满足条件则
继续执行 abort 函数. 因此, 在智能合约中函数内的语句能否执行, 不仅受到函数内分支语句的控制, 同时还被函
数修饰器的分支条件所影响.

1 address public seller;
2 modifier onlySeller() {
3 require(msg.sender == seller, "Only seller can call this.");
4 _;
5 }
6 function abort() public view onlySeller {
7 //do somethings…
8 }
图 3 包含函数修饰器的智能合约代码示例

由上文中智能合约符号执行的分析过程可知, 为了更准确地判断目标语句可达性, 需要预先执行合约中的部
分语句, 其与目标语句之间存在由控制依赖和数据依赖构成的传递闭包关系. 本文称这类语句为目标依赖语句.
(
)
定义 3 (目标依赖语句). 对于智能合约中的语句 stmt i 和目标语句 stmt j , 若 transitiveDep stmt i , stmt j = T , 其中
transitiveDep 表示 stmt i 和 stmt j 之间存在由控制依赖和数据依赖构成的传递闭包, 则称 stmt i 为 stmt j 的目标依赖
语句.
根据上述 3 个定义, 可对智能合约 C 中目标语句 target 的目标依赖语句进行分析, 分析过程如算法 1 所示. 第
1, 2 行初始化目标依赖语句集合 ret 和待分析语句队列 queue, 第 3–9 行对 queue 中的待分析语句 stmt j 进行分析,
其中第 4–6 行获得与 stmt j 存在数据依赖的语句 stmt D 并添加到 ret 和 queue, 第 7–9 行则获得与 stmt j 存在控制依
赖的语句 stmt C 并添加到 ret 和 queue, 通过循环进行迭代分析, 最后在第 10 行输出目标依赖语句集合.
算法 1. 分析目标依赖语句.

输入: 智能合约 C; 目标语句 target;
输出: 目标依赖语句集合.

1. ret = ∅
2. queue = Queue( target)
3. while stmt j = queue.pop() != None:
4. stmt D = getDataDep( stmt j ,C) //数据依赖
ret.add( stmt D ) //添加到目标依赖语句集合
5.