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

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

种类型的状态变量在读取和赋值时寻址方式不同 [36] , 因此本文将变量操作语句分为定长变量赋值语句和非定长
变量赋值语句.

表 1 Solidity 智能合约代码结构

中文名称 英文名称 描述
状态变量 State variable 持久存储数据
结构体 Struct 定义由多种数据类型组成的结构
枚举 Enum 定义有限的数据集合
事件 Event 调用EVM日志接口
函数 Function 合约的可执行单元
函数修饰器 Function modifier 修改函数执行的语义

表 2 描述了 Solidity 智能合约语句类型, 并给出了对应的符号化表达式. 其中, x 表示变量, x[i] 表示非定长变
i
s
量 x 中位于位置 的元素, value 表示常量、变量或由变量组成的符号化表达式, symb(s) 表示符号化执行语句 的
结果, symb func ( f) 和 symb lib (l) 分别表示符号化执行函数 f 和库合约函数 l 的返回值, REVERT 表示回滚合约中的状
态变量. 根据表 2 中智能合约语句的符号化表达式, 可将函数调用 f 表示为六元组 (sender,value,data, sign, param,S ).
其中, sender 为函数的调用者地址, value 为函数调用携带的以太币数量, data 为函数调用携带的数据, sign 为函数
名称, param 为调用函数的参数, S 为此次函数调用过程中所执行的语句的路径条件, 即 S = s 1 ∧ s 2 ∧...∧ s n , 其中 s i 表
i 条语句后的符号约束条件, 各语句之间通过“合取”逻辑符
示符号化执行第 (即 ∧) 连接, 表示语句 s i 在 s 1 ∧ s 2 ∧...∧ s i−1
的基础上添加符号值约束. 对于变量操作类型中的赋值语句以及函数调用类型语句中涉及利用返回值赋值的语
句, 对被赋值对象添加上标以区分符号化执行赋值语句前后变量的符号值, 例如函数内语句 {a = param;b = a+2;a = b}
′
′
′
′′
′
经过符号化执行后, 其路径条件为 (a = param∧b = a +2∧a = b ).

表 2 Solidity 智能合约语句类型、示例以及符号化表达式

语句类型 示例 符号化表达式
uint a;
变量声明 －
uint[] b;
变量操作
定长变量赋值 a = 12; x := value
非定长变量赋值 b[2] = 3; x[i] := value
{
x = value∧ symb(s 1 )
条件判断 if(a == 20){s 1 ;}else{s 2 ;}
x! = value∧ symb(s 2 )
假定 {
require(a == 20); s 1 ; x = value∧ symb(s 1 )
条件约束
assert a == 10; s 1 ; x! = value∧REVERT
合约函数调用 b = foo(a); x := symb func ( f)
函数调用
库合约函数调用 c = lib(a, b); x := symb lib (l)
返回值 return a; －
跳转
抛出异常 revert(); REVERT

T 表示为
此外, 智能合约可通过事务序列改变合约的状态变量, 进而影响函数的执行逻辑. 我们将事务序列
∗
T = {init, f }. 其中, init 表示合约状态变量的初始化, f 为该事务序列中函数调用的次序, 即 f = { f 1 , f 2 ,..., f n }. 事
∗
∗
务序列 T 执行的语句的路径条件为 S T = S init ∧S 1 ∧S 2 ∧...∧S n , 其中, S init 表示初始化合约状态变量的路径条件, S i
表示函数调用 f i 所执行的语句的路径条件, S init 以及 S i 之间通过“合取”逻辑符连接, 即 S i 在 S init ∧S 1 ∧S 2 ∧...∧S i−1
对状态变量操作的基础上添加符号值约束. 此外, 在 S n 中根据预先定义的安全漏洞模型添加漏洞检测符号约束,
T 是否存在相应的安全漏洞.
从而检测事务序列
4.2 目标依赖语句分析
智能合约是具有状态的程序, 能够通过不同的事务序列改变合约的状态变量, 从而使合约处于不同的状态, 函