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

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

数将根据状态变量判断当前合约状态是否满足分支的条件约束 [15,31] . 因此, 若仅符号化执行控制流图中可到达目
标语句的基本块, 缺少相关变量的符号约束, 将无法满足目标语句所在分支的条件约束, 使符号执行错误判断路径
的可达性, 影响对目标语句的安全漏洞检测.
本文将影响目标语句可达性判断的语句称为目标依赖语句, 接下来将以图 1 中第 72 行的整型溢出漏洞为例,
具体描述利用符号执行对智能合约进行安全漏洞检测的具体过程, 以及目标依赖语句的作用.
T 的过程中, 会收集变量的符号约束. 当存在漏洞模型预定义的操作时, 将在路径条件
在符号化执行事务序列
中添加相应的漏洞检测符号约束, 如图 1 中在第 72 行进行加法运算前添加符号约束 ¬(a+v > a). 如果事务序列 T
执行语句的路径条件约束求解的结果为可满足, 则该事务序列中存在整型溢出漏洞, 约束求解的结果可以作为复
现该漏洞的测试用例.
若仅将漏洞语句作为目标, 由于漏洞语句位于函数 transferFrom
中, 因此事务序列 T only 可表示为:
T only = {init,transferFrom(p 1 , p 2 , p 3 )},
其中, p 1 、 p 3 分别表示参数_from、_to T only 执行语句的路径条件S only 展开可得:
p 2 和 和_value 的符号化表示. 将
′
′
S only = balances = 0∧allowed = 0 (s1)
[ ]
′
∧balances p 1 ⩾ p 3 (s2)
[ ][ ]
′
∧allowd p 1 sender(transferFrom(p 1 , p 2 , p 3 )) ⩾ p 3 (s3)
∧ p 3 > 0 (s4)
[ ] [ ]
′
∧¬(balances p 2 + p 3 > balances p 2 ) (s5)
′
其中, s1 为第 41 行和第 42 行对合约状态变量的初始化, s2–s4 为第 71 行的 require 语句判断条件, s5 则为整型溢
S only 可以看出, 由于 s1、s2 和 s4 S only 无法满足, 导
出漏洞的检测条件. 从 无法同时满足, 因此约束求解器将判断
致符号执行未能检测出整型溢出漏洞.
若将漏洞语句作为目标的同时, 定位与其存在依赖关系的其他语句, 补充事务序列以添加相关变量的符号约
束, 能够更准确地判断路径可达性. 从图 1 可以看出, 第 72 行目标语句受到第 71 行分支语句的控制, 分支语句读
取了变量 balances 和 allowed, 第 79 行 (位于 mint 函数) 和第 90 行 (位于 approve 函数) 分别对这两个变量进行赋
值. 将这 2 个函数作为事务序列 T only 的补充, 可得到由 mint、approve 以及 transferFrom 共 3 个函数调用所组成的
事务序列. 当事务序列的长度限制为 3 时共有 3 = 27 种组合方式, 其中一种事务序列 T sv 为:
3

T sv = {init,mint(p 4 ),approve(p 5 , p 6 ),transferFrom(p 1 , p 2 , p 3 )},
其中, p 4 为函数 mint 的参数 amount 的符号化表示, p 5 和 p 6 为函数 approve 的参数_spender 和_value 的符号化表
示. 将 T sv 执行语句的路径条件S sv 展开可得:

′
S sv = balances = 0∧allowed = 0 (s1)
′
+
∧ p 4 ⩾ 0∧ sender(mint(p 4 )) = owner ′ (s2 )
[ ] [ ]
+
′
∧(balances sender(mint( p 4 )) + p 4 > balances sender(mint(p 4 )) ) (s3 )
′
[ ] [ ]
+
′
∧balances sender(mint(p 4 )) ′′ = balances sender(mint( p 4 )) + p 4 (s4 )
′ ′ ′′ ′ +
∧(totalSupply + p 4 > totalSupply )∧totalSupply = totalSupply + p 4 (s5 )
[ ][ ]
+
′ (s6 )
∧allowed sender(approve(p 5 , p 6 )) p 5 = p 6
[ ]
′
∧balances p 1 ⩾ p 3 (s2)
[ ][ ]
′ (s3)
∧allowd p 1 sender(transferFrom(p 1 , p 2 , p 3 )) ⩾ p 3
∧ p 3 > 0 (s4)
[ ] [ ]
′
∧¬(balances p 2 + p 3 > balances p 2 ) (s5)
′
T sv 在 transferFrom 前执行了 mint 和 + s6 共 + 5
由于事务序列 approve 函数, 因此在 S only 的基础上, 新增了 s2 –
条路径条件, 添加了 balances 和 allowed 的符号约束, 使 S sv 可以满足, 即检测出整型溢出漏洞. 经约束求解, 可得
(
S sv 的一个可满足解为: mint(p 4 ) 的调用者为 owner, 2 255 −1 approve p 5 , p ) 的调用者为 owner, p 5 为任意
;
到 p 4 为 6
地址, p 6 为大于 0 的整型数值; transferFrom(p 1 , p 2 , p 3 ) 的调用者为 p 5 p 1 和 p 2 为 owner, p 3 为 p 6 .
,