2008年, Satoshi Nakamoto首次提出了区块和链的概念^[1], 指出了当前的线上交易几乎都需要依赖可信第三方, 这增加了交易成本且扩大了不必要的交易规模.因此, 中本聪提出了一种点对点的数字货币交易系统, 也就是比特币系统, 这也标志着区块链时代的到来.区块链本质上是分布式的数据账本, 使用了加密算法、共识机制等技术, 保证了用户的隐私且在交易期间不再依赖可信第三方的支持.早在1994年, Nick Szabo就提出了智能合约的概念^[2], 并将其定义为可以自动执行复杂业务操作的数字合约.但由于无法保证在没有第三方介入的情况下正确执行合约条款, 因此智能合约一直没有在实际中应用, 直到区块链的出现.区块链所具备的去中心化、公开共享、可信性、集体维护以及不可篡改的特质, 使其成为智能合约天然的执行平台.

目前, 智能合约已在许多区块链系统上成功实现, 比较著名的系统有以太坊(Ethereum)^[3]和超级账本(hyperledger)^[4].以太坊在2013年由俄罗斯学者Vitalik Buterin所推出的《以太坊: 下一代智能合约和去中心化应用平台》^[5]中被首次提出, 是目前最大的区块链平台.在以太坊中, 大多数智能合约程序由图灵完备语言Solidity编写^[6], 然后编译为以太坊虚拟机(Ethereum virtual machine, 简称EVM)的字节码, 并运行在EVM之上.随着区块链技术的出现和发展, 智能合约已经被应用于医疗(如存储电子病历和基因数据)、金融(如P2P网络借贷)、资产管理等领域, 但其安全性问题却层出不穷^[7].2016年, 攻击者利用The Dao智能合约的脚本代码漏洞^[8], 从中窃取了300多万以太币.2018年, BEC智能合约出现重大漏洞, 攻击者利用批量转账函数中的整数溢出问题无限生成代币, 造成了约60亿人民币的损失.

在实际应用中, 智能合约涉及了大量用户的数字财产, 一旦出现漏洞, 就会造成无法挽回的损失.因此, 在智能合约被部署到区块链平台之前, 需要对其进行漏洞排查.传统的测试方法不能达到保证智能合约正确性和高可靠性的需求, 国内外许多学者提出了使用形式化方法对智能合约进行验证的方式, 主要包括定理证明、符号执行以及模型检测这3种.

本文提出一种基于时序逻辑语言(modeling, simulation and verification language, 简称MSVL)的智能合约安全性的模型检测方法: 首先, 使用MSVL对智能合约程序进行建模, 为了减少建模时大量的人工操作, 开发了将智能合约语言Solidity转换为MSVL的转换器工具SOL2M, 实现了智能合约建模程序的自动化生成; 然后, 使用命题投影时序逻辑(propositional projection temporal logic, 简称PPTL)公式描述该智能合约的安全性性质; 最后, 在统一模型检测器(unified model checker for MSVL, 简称UMC4M)中自动化验证建模程序是否满足给定的安全性性质, 并通过实例说明该方法运用到智能合约验证中的可行性和实用性.

本文第1节将回顾MSVL与PPTL相关理论.第2节将介绍Solidity语言特性以及智能合约的安全问题.第3节将给出SOL2M转换器的研究与实现.第4节将给出使用MSVL对智能合约建模和验证的应用实例.第5节将给出相关工作.第6节将给出总结及展望.

1 MSVL与PPTL 1.1 MSVL

MSVL的初始版本是Framed Tempura^[9], 在引入了等待语句和非确定选择语句之后, 得到了建模、仿真与验证语言MSVL.MSVL是投影时序逻辑(projection temporal logic, 简称PTL)的可执行子集, 具有与高级程序设计语言类似的语法.下面介绍MSVL的基本语句.

(1) 区间长度语句: empty, skip, len(n);

(2) 区间框架语句: frame(x);

(3) 并行语句: p||q;

(4) 顺序语句: p; q;

(5) 非确定选择语句: p or q;

(6) 合取语句: p and q;

(7) 等待语句: await(b);

(8) 立即赋值语句: x < =e;

(9) 下一状态赋值语句: x: =e;

(10) Always语句: alw(p);

(11) Next语句: next p;

(12) 循环语句: while b do p;

(13) 条件语句: if b then p else q;

(14) 投影语句: (p₁, …, p_m) prj q;

(15) 函数调用语句: fun(e₁, …, e_m).

其中, x为变量, e为算数表达式, b为布尔表达式p₁, …, p_m, p, q为MSVL程序.

区间长度语句empty, skip, len(n)分别声明了当前区间长度为0, 1, n; 并行语句p||q表明p与q在当前状态下同时开始执行, 并有可能在不同时间结束; 非确定选择语句p or q表示在当前状态下可以执行p或q中的任意一个; 顺序语句p; q表示p与q按照顺序执行; 合取语句p and q表示p与q在当前状态下同时开始执行并同时结束; 等待语句await(b)将会循环判断表达式b的真假, 直到b为真时结束循环; 立即赋值语句x: =e与下一状态赋值语句x < =e分别表示在当前状态和下一状态对变量进行赋值; alw(p)表示在所有状态下执行p; next p表示在下一状态执行p; while b do p; if b then p else q以及函数调用语句的用法与其他高级程序设计语言相同.MSVL不仅包含赋值语句、循环语句、条件判断语句等基本语句, 还加入了框架结构和投影结构, 为描述软硬件系统提供了更强的表达能力.区间框架语句frame(x)使得变量x的值能够在区间上自动遗传, 否则, 变量x仅在被赋值时的状态下有确定的值, 在其他状态下变量值是不确定的; 投影语句(p₁, …, p_m) prj q使得p₁, …, p_m与q能够并行执行, 且p₁, …, p_m顺序执行, 而q在另一个状态区间上执行.

1.2 PPTL

本文描述智能合约性质使用的PPTL是PTL^[10]的一个可判定子集, 具有完备的公理系统^[11], 与MSVL均属于PTL的子集, 可以共同完成对软硬件系统的形式化验证.在表达能力方面, PPTL等价于完全正则表达式, 严格强于LTL, 能够很好地描述智能合约的性质.PPTL的语法和语义介绍如下:

(1) PPTL的语法

Prop代表原子命题集合, p代表原子命题, 且$ p \in { Prop } ; P, P_{1}, \ldots, P_{m}$以及Q代表PPTL公式; O(next)和prj (projection)是PPTL中的时序操作符.PPTL公式的归纳定义如下:

$ P,Q:: = p|\neg P|P \wedge Q|OP|\left( {{P_1}, \ldots ,{P_m}} \right)prj\;Q. $

(2) PPTL的语义

● PPTL的状态: 状态s被定义为集合Prop到{true, false}的一个映射关系s: Prop$ \to ${true, false}, 表明一个原子命题在状态s上可以为真或为假.假设命题p在状态s上的布尔值定义为s[p], 若s[p]=true, 表明是p在状态s上为真, 否则为假;

● PPTL的区间: 令符号σ代表由一个或多个状态s组成的状态序列, 即区间状态.|σ|代表区间长度, 当区间中的状态为有限个时, |σ$\vDash $状态数-1, 此时, 区间为有穷区间; 当区间中的状态为无限个时, 区间长度|σ$\vDash $ω, 此时, 区间为无穷区间.为了统一有穷区间和无穷区间的表达, 需要扩展非负整数集.令N₀代表非负整数集, N_ω代表N₀ $ \cup $ {ω}, 已知ω=ω, 对于任意的i∈N₀, 都满足i < ω.令$\preceq $代表≤-{(ω, ω)}, 区间σ=⟨s₀, s₁, …, s_|σ|⟩, 区间σ_(i-1)(0≤i$\preceq $j≤|σ|)为σ的子区间.区间操作符·可以将两个区间σ=⟨s₀, s₁, …, s_|σ|⟩和$\sigma ' = \langle {s'_0}, {s'_1}, ..., {s'_{|\sigma |}}\rangle $连接为$\sigma \cdot \sigma ' = \langle {s_0}, {s_1}, ..., {s_{|\sigma |}}, {s'_0}, {s'_1}, ..., {s'_{|\sigma |}}\rangle $, 但前提是前一个区间σ必须为有穷区间;

● PPTL公式的解释: 令三元组I=(σ, k, j)表示PPTL公式的解释, 其中, σ代表区间, k和j为整数且满足: 0≤k $\preceq $ j≤|σ|.令P代表一个PPTL公式, 那么P的解释I就定义为P解释在σ的子区间σ(k…j)上并且在区间上满足.这里令$I_{prop}^k$代表在状态;

● s_k上的解释, 令$\vDash $表示可满足关系, 则公式P与解释I的可满足关系如下:

➢ I$\vDash $p: 当且仅当${s_k}[p] = I_{prop}^k[p] = true$;

➢ I$\vDash $¬p: 当且仅当I $\nvDash $ p;

➢ I$\vDash $P₁$ \wedge $P₂: 当且仅当I$\vDash $P₁并且I$\vDash $P₂;

➢ I$\vDash $OP: 当且仅当k < j并且(σ, k+1, j)$\vDash $P;

➢ I$\vDash $(P₁, …, P_m) prj Q: 当且仅当存在k=r₀≤...≤r_m-1$\preceq $r_m≤j, 使得对于所有的1≤l≤m, 有(σ, r_l-1, r_l)$\vDash $P_l且对于下面情况有(σ', 0, |σ'|)$\vDash $P:

(1) r_m < j且σ'=σ$ \downarrow $(r₀, ..., r_m)·σ(r_m+1, …, j);

(2) r_m=j且σ'=σ $ \downarrow $ (r₀, ..., r_h)(其中, 0≤h≤m).

1.3 UMC4M统一模型检测器

面向MSVL和PPTL的模型检测^[12]是建立在形式化建模和形式化规约基础之上的.形式化建模采用MSVL程序M对待验证的系统进行建模, 形式化规约一般采用PPTL逻辑公式P描述待验证系统需要满足的性质.由于MSVL和PPTL均是PTL的子集, 因此可同时将模型M与性质P统一在PTL框架下.验证M$ \to $P是否成立来验证系统的正确性, 根据逻辑公式推理可得M$ \to $P等价于¬(M$ \wedge $¬P).在传统模型检测方法中, 只需判定M$ \wedge $¬P是否成立便可验证性质满足性: 如果公式成立, 则模型违反性质; 否则, 模型满足性质.

UMC4M工具对传统模型检测方法进行了改进, 基础架构如图 1所示.首先, 将PPTL公式P取反, 并转换为MSVL程序M'; 再将MSVL建模程序M与M'合取为MSVL程序M and M', 即: 将(M$ \wedge $¬P)是否成立转化为M and M'是否能够正确执行的问题; 然后, 通过MSVL编译器(MSVL compiler, 简称MC)^[13]执行M and M'程序, 并生成可执行文件M_and_M'.exe和中间代码$M{M'_{IR}}$(intermediate representation); 接着, 通过KLEE⁺处理$M{M'_{IR}}$并生成验证用例(verification case, 简称VC); 最终, 运行M_and_M'.exe并接受VC, 然后依据执行结果判定性质是否满足.

2 Solidity

Solidity是用于开发智能合约的高级语言, 其语法与Javascript相似.相比于高级程序设计语言, Solidity缺少多线程以及并发等高级特性.使用Solidity语言编写的智能合约通过编译生成二进制字节码, 并运行在以太坊虚拟机EVM上.

Solidity源文件的后缀为sol, 主要由版本标识语句、导入其他源文件以及合约的定义这3部分组成.其中: 版本标识语句使用保留字pragma声明Solidity的版本号, 例如, pragma solidity^0.4.0, 表明源文件不允许低于0.4.0版本的编译器编译; 导入其他源文件部分使用保留字import, 相当于将多个源文件写到一个文件中, 例如, import “filename”将“filename”中所有的全局符号导入到当前全局作用域中; 合约的定义部分由关键字contract进行声明, 例如, contract{...}, {…}中封装了合约, 实现了合约的具体功能.

Solidity中的合约contract类似面向对象高级语言中的类Class, 包含状态变量(state variables)、函数(functions)、事件(events)、结构体(struct)等.状态变量能够描述系统状态, 类似于整个代码中的全局变量; 函数是指包含一系列操作的可执行单元, 能够完成特定的功能, 由关键字function声明; 结构体是指包含任意成员变量的自定义类型, 由关键字struct声明, 与高级程序设计语言中的结构体类似; 事件是调用以太坊虚拟机EVM日志功能的接口, 使用关键字event声明.

以下通过一个Solidity实例进行简单介绍(如图 2所示).

合约Demo包含变量声明和函数两部分, 声明了一个类型为无符号整数uint的状态变量v, 声明了一个set函数用于修改变量v的值, 声明了一个get函数用于查询变量v的值.

3 SOL2M转换器的研究与实现

本文使用MSVL对智能合约Solidity程序进行建模, 为减少建模过程中大量的人工操作, 开发了一种能够实现Solidity语言到MSVL语言的等价转换工具SOL2M, 实现了建模过程的自动化, 其具体结构以及工作流程如图 3所示.

SOL2M转换器主要分为4个部分.

(1) 预处理: 处理Solidity源程序中的版本标识语句和导入其他源文件语句;

(2) 词法分析: 通过JavaCC工具生成词法分析器, 对Solidity程序进行词法分析, 将源程序识别为特定的单词流;

(3) 语法分析: 通过JavaCC工具生成语法分析器, 对Solidity程序进行语法分析, 把词法分析生成的单词流识别为程序语句;

(4) 程序转换: 通过分析Solidity和MSVL的词法以及语法的异同, 制定出Solidity到MSVL的转换规则, 并将转换代码嵌套在语法分析的BNF范式中, 实现Solidity程序到MSVL程序的动态转换.

3.1 预处理模块

在预处理模块中, 需要处理版本标识语句和导入其他源文件语句.由于版本标识语句并不会影响Solidity源程序的正确性和逻辑性, 因此只需要对其进行移除.导入其他源文件是使用保留字import进行声明, 导入语句的作用是待导入文件的所有全局变量导入到当前文件中的全局作用域中, 以便于模块化代码.因此, 需要先将待导入文件的全局变量合并到当前文件中, 之后再进行词法分析.若不存在导入语句, 直接进行后续分析.

3.2 词法分析模块

词法分析模块顺序扫描Solidity源程序, 根据构词规则将其识别为具有特定含义的单词, 并按照属性对其进行分类和标识.本文使用JavaCC工具自动生成词法分析器.一般的词法分析器包含SKIP与TOKEN两部分: SIKP定义了源程序中需要忽略的部分, 如注释部分和空白部分等; TOKEN中使用正则表达式定义了需要特定识别的单词, 在扫描源程序的过程中对字符序列进行分割并识别为单词及其属性, 最终将所得到的TOKEN序列交给语法分析器.

SKIP部分定义了需要自动跳过的部分, 包括单行注释、多行注释、空格、缩进符、换行符以及回车符, 使用正则表达式描述其构词规则如图 4所示.

TOKEN部分定义了需要特定识别的内容, 主要包括保留字、标识符、常量以及运算符等.

(1) 保留字

如表 1所示: int与uint均可表示整型类型, 且可以限定整型变量的长度, 如int8到int256, 当省略后面数字时, 默认为int256;保留字public/private/internal用于表明函数或者变量的可见性, 但由于可见性并不影响程序的逻辑性和正确性, 因此予以忽略; 保留字event用于定义一个事件, 用于调用以太坊虚拟机日志功能的接口, 起到储存记录的作用, 并不影响程序的逻辑性和正确性, 因此忽略event保留字.

(2) 标识符

标识符包含用户自定义的合约名、函数名以及变量名等, 其首字母为下划线或字母, 其他部分为下划线、字母以及数字.当一个单词既能够被识别为保留字, 又能够被识别为标识符时, 将其首先识别为保留字.标识符的正则表达式如图 5所示.

(3) 运算符与界限符

运算符是语言固有的操作符号, Solidity语言中的运算符见表 2.

界限符主要用于分割不同语句或标识符, Solidity中的界限符见表 3.

(4) 常量

常量为不会发生改变的内容, 如整型常量、布尔常量、地址常量和字符常量, 这4类常量通常能满足大部分智能合约的要求, 如果合约需要更复杂的常量, 只需在JavaCC的常量定义部分进行扩充, 常量的正则表达式如图 6所示.

3.3 语法分析模块

语法分析建立在词法分析的基础之上, 对词法分析生成的单词序列按照语法规则组成有特定含义的语句, 并生成与源代码等价的语法树.本文使用BNF范式描述智能合约的语法规则.

首先, 智能合约由结构体、状态变量、函数以及事件4部分组成, 其BNF定义如图 7所示.合约以Start为开始, 以Procedure为终止.合约主体部分为ContractBlock声明, 包含Struct, Statedef以及Method, 分别用于声明结构体、状态变量与函数.

其次, 智能合约源程序由各种基本语句组成, 主要包括声明语句、表达式语句、条件判断语句、循环语句、转向语句、复合语句(也称语句块)以及空语句, 其BNF定义如图 8所示.非终结符Statement表示基本语句, IF, While, For分别定义了条件判断语句与循环语句, Block定义了复合语句, Statedef定义了声明语句, return与throw定义了两个跳转语句.

表达式结构包含了程序中的各类运算与操作, 其BNF最为复杂, 如图 9所示.第1行中的Literal表示可能出现的字面值, 包括变量、结构体、数组、整型变量和布尔变量等; 第2行的Unop表示单目运算; 第3行~第8行的Binop表示双目运算符: Assign表示赋值运算符, PLUS_MINUS表示自增自减运算符.除此之外, 还定义了[·], (·), .操作, 可以描述Solidity中成员函数的调用.

3.4 语义分析与程序转换模块

语义分析是编译过程中的一个逻辑阶段, 其功能为对源程序进行上下文有关性质的分析, 审查是否存在语义错误, 最终将源程序翻译为机器能够读懂的语言.本文对语法分析之后得到的Solidity源程序进行语义分析, 根据每条语句的实际含义制定出Solidity与MSVL之间的等价转换规则, 并在语义分析的过程中实现程序转换.

通过分析和对比Solidity语言与MSVL语言, 制定了两者之间的转换规则.下面从合约以及基本语句的转换规则两方面进行介绍, 部分转换规则见表 4.

智能合约主要由状态变量、结构体和函数构成.Solidity中的int8, uint256等声明整型变量转换为MSVL程序后均使用int.同理, Solidity中的bytes转换为MSVL的char类型, 地址变量address转换为char类型.在Solidity中, 结构体的声明与MSVL的用法相同, 只需要在结构体内部加入相应的时序操作即可.Solidity与MSVL中函数声明的用法也相同, 但函数中需要加入frame框架操作来保证变量值的遗传.

基本语句包括声明语句、表达式语句、条件判断语句、循环语句、转向语句、复合语句以及空语句.若MSVL当中存在Solidity某个语句的近似语句时, 可以直接替换, 例如while语句和if语句等; 若MSVL中不存在近似语句, 则需要对该语句进行抽象表达, 例如throw语句.当抛出异常时后面的语句不再执行, 由于在MSVL中不存在抛出异常的语句, 转换时将throw语句与将要执行的语句一并转换为skip, 其区间长度为1, 并在下一状态执行空语句empty.

根据JavaCC的特性, 本文采用在语法分析过程中进行语义分析的方法来实现程序转换, 根据制定的转换规则在每个语法分析函数中预定义了转换的语义动作.程序转换的基本流程如图 10所示: SOL2M转换器首先读取Solidity源程序文件(solidity.sol); 然后进入语法分析阶段, 提取Solidity程序语法单元的语义信息, 并根据制定的转换规则将Solidity代码转换为与其功能等价的MSVL代码; 转换后的MSVL代码被暂存在预先创建的Java集合对象中, 待语法分析结束后, 遍历暂存集合并写入到MSVL程序文件(msvl.m)中.设m表示Solidity程序中变量声明的数量, n表示语句数, p表示每条语句中包含表达式的平均数, 不难证明, SOL2M转换流程的时间复杂度是O(n×p+m).通常, Solidity程序中一条语句的表达式数量、变量声明数量均不会超过一个常数, 因此, SOL2M转换流程的时间复杂度为O(n).UMC4M验证MSVL程序基于PPTL的判定算法^[10]: 设PPTL公式的长度为l, 包含的命题组成集合$\varphi $, 则该算法的时间复杂度为O(l×2^{|$\varphi $|}).

4 实例验证

本文使用SOL2M转换器对智能合约进行自动化建模, 并提出了一种面向MSVL和PPTL的形式化验证方法.MSVL是PTL的可执行子集, PPTL是PTL的可判定子集, 因此可以将MSVL与PPTL统一在PTL的框架中进行自动验证.验证流程如图 11所示, 具体为: 使用MSVL对智能合约进行自动建模, 存放在m文件中; 使用PPTL描述智能合约待验证性质并存放在p文件中; 将建模程序与待验证性质输入统一模型检测器UMC4M进行验证; 若智能合约模型出错, 则对m文件进行修改; 若是待验证性质出错, 则对p文件进行修改; 若验证成功, UMC4M检测器会给出模型是否满足性质的结果, 或给出反例以便排查智能合约漏洞.

本节将通过两个具体智能合约实例, 使用SOL2M转换器对合约进行建模, 使用PPTL公式描述合约需要满足的性质, 最后在UMC4M统一模型检测器中完成验证.

4.1 投票智能合约的建模与验证

本小节以投票智能合约为例, 给出SOL2M对其进行建模的详细流程以及验证过程.如图 12所示, 该投票协议主要包括状态变量、结构体和函数这3部分.合约名称为voteContract, 合约内部首先声明了候选者Candidate结构体, 包含候选者名称与所获票数两个成员变量; 其次创建了一个从候选者到票数的映射类型, 以及使用结构体类型的数组Candidate[]来存储所有候选者; 合约内还声明了两个函数——vote()函数实现了为特定候选者投票的功能, winner()函数从所有候选者中选择出票数最高的获胜者.

首先对投票智能合约进行建模, 将投票智能合约作为SOL2M转换器的输入被自动存入solidity.sol文件中, 如图 13所示, 将Solidity代码转换为MSVL代码, 结果存放在msvl.m文件中.建模之后, 使用PPTL描述投票智能合约的性质, PPTL公式中常用的时序操作符见表 5.本文将智能合约的性质归纳为3个层面: 功能一致性、逻辑正确性以及合约完备性.下面从这3个方面描述投票智能合约应该满足的性质.

(1) 功能一致性.

每一个智能合约应满足的基本要求, 是指智能合约的函数功能与合约设计要求之间的一致性, 即待验证合约的功能应当符合实际要求.对于投票智能合约来说, 其winner函数需要从所有候选者中选择出票数最高的赢家, 若最终存在比赢家的票数更高的候选者, 则说明winner函数没有实现实际要求, 即不满足功能一致性.因此, 描述性质1为: 投票结束后, 不存在比赢家票数更高的候选者.从原子命题、命题逻辑与时序逻辑这3个方面对性质1进行描述见表 6, 最终使用PPTL公式描述性质1为fin(!m).

(2) 逻辑正确性.

关乎智能合约的安全问题, 是指保证合约内函数的逻辑正确, 即不存在逻辑漏洞.对于投票智能合约来说, vote函数是整个合约的逻辑核心部分, 其逻辑为: 当投票者调用vote函数发起投票时, 其手中拥有的票数至少为1, 且当投票者手中有票时, 一定会投票成功.将该逻辑精简为性质2与性质3.

● 性质2:当投票者投票成功时, 则其手中一定有票.从原子命题、命题逻辑与时序逻辑这3个方面对性质2进行描述见表 7, 最终使用PPTL公式描述性质2为alw(q- > r);

● 性质3:当投票者调用vote函数且手中有票时, 在将来某一状态下一定投票成功.从原子命题、命题逻辑与时序逻辑这3个方面对性质3进行描述见表 8, 最终使用PPTL公式描述性质3为

$ {alw}((p \text { and } r)->{som} q) . $

(3) 合约完备性.

功能一致性与逻辑正确性的综合表达, 只有满足功能一致性与逻辑正确性, 才能认为合约满足完备性.对于投票智能合约来说, 其合约完备被描述为性质4:性质1~性质3同时满足.使用PPTL公式描述性质4为

$ {fin}(! m) \text { and }(a l w(q->r)) \text { and }({alw}((p \text { and } r)-> { som }~ q)). $

最后, 将MSVL模型与PPTL公式输入到UMC4M中进行验证.在验证之前, 需要在MSVL建模程序中加入对性质的定义, 类似于代码插桩技术.

投票智能合约应满足的PPTL公式fin(!m) and (alw(q- > r)) and (alw((p and r)- > som q))等价于fin(!m) and alw(!(q) or r) and alw(!(p and r) or (som q)).将上述性质输入到p文件中, 具体如下所示:

⟨/

define m: m_flag=1;  //定义命题m

define p: p_flag=1;  //定义命题p

define q: q_flag=1;  //定义命题q

define r: r_flag=1;  //定义命题r

fin(!m) and alw(!(q) or r) and alw(!(p and r) or (som q))

/⟩

运行UMC4M检测器的结果如图 14所示, 验证结果为模型满足性质, 总用时653ms.

4.2 银行转账合约的建模与验证

本小节以具体的银行转账智能合约与常见的重入攻击漏洞为例, 给出SOL2M对转账合约与重入攻击进行建模的详细流程以及验证过程.建模时, 在银行转账合约中抽象加入了重入攻击操作, 即将转账合约与重入攻击代码抽象为合约.如图 15所示, 其中, deposit函数的功能是用户把钱存入银行, withDraw函数实现了转账功能, 用户通过withDraw函数与send函数从银行取钱.Attack函数实现了重入攻击的功能, 其具体步骤为: 首先, 攻击者调用Attack函数, 通过deposit函数向银行转账合约中存入一些以太币; 之后调用withDraw函数, 从银行转账合约中取钱, 使用require语句判断用户余额以及银行总余额是否足够; 最后, 调用send函数给用户地址转账.问题出现在第10行与第11行: 合约执行send操作后修改用户余额, 当合约发送以太币给攻击合约时会执行回退函数, 建模过程中使用fallback模拟, 其中会再次调用withDraw函数取钱.当执行require语句时, 由于第11行还未执行, 用户余额未改变, require语句顺利通过, 银行转账合约继续向攻击合约转账.不断重复这些操作, 攻击者可以从合约中提取所有以太币.

对合约进行建模, 将银行转账合约与重入攻击合并为一个合约并作为SOL2M转换器的输入, 转换结果如图 16所示.

使用PPTL公式描述银行转账合约应满足的性质, 下面从功能一致性、逻辑正确性以及合约完备性3个层面进行详细描述.

(1) 功能一致性.

对于银行转账合约来说, 其deposit函数用于实现存钱操作.若用户调用了deposit函数, 但用户余额没有增加, 则说明deposit函数没有满足实际要求, 即合约不满足功能一致性.将该功能精简为性质5:在任何状态下, 若用户调用deposit函数, 则该用户余额在未来某一状态一定增加.从原子命题、命题逻辑、时序逻辑3个层面描述性质5见表 9, 最终使用PPTL公式描述性质5为

$ a l w(m->{som}~ n). $

(2) 逻辑正确性.

在银行转账合约中, 将以太币发送至地址需要提交外部调用.一旦被攻击者劫持, 将会迫使合约执行更多的代码(即fallback回退函数).攻击者在fallback函数中回调受攻击合约的任意函数, 即为重入合约.在本例中, 攻击者可以多次回调deposit函数实现无限取钱操作.无重入攻击的合约应当在执行完外部调用时保证没有调用合约内所有函数.可能导致恶意情况发生的内部函数有deposit函数和withDraw函数, 因此描述性质6为: 在所有状态下都不存在当withDraw函数执行完外部调用时, deposit函数或withDraw函数被再次调用.从原子命题、命题逻辑、时序逻辑这3个层面描述性质6见表 10, 最终使用PPTL公式描述性质6为

$ a l w(!(f \text { and }(h \text { or } r))) \text { . } $

除此之外, 当用户要求银行转账时, 若该用户余额大于转账金额, 则一定能够转账成功; 并且当转账成功时, 该用户余额一定大于转账金额.从原子命题、命题逻辑与时序逻辑这3个方面对性质7进行描述见表 11, 最终使用PPTL公式描述性质7为

$ a l w((p \text { and } q)->g) \text { and } a {lw}(g->q). $

(3) 合约完备性.

合约完备性是功能一致性与逻辑正确性的综合表达, 只有满足功能一致性与逻辑正确性, 才能认为合约满足完备性.对于银行转账合约来说, 其合约完备被描述为性质8:性质5~性质7同时满足.使用PPTL公式描述性质8为

$ {alw}(m->n) \text { and } {alw}(!(f \text { and }(h \text { or } r)) \text { ) and } {alw}((p \text { and } q)->g) \text { and } a l w(g->q) \text { . } $

将MSVL模型与PPTL公式输入到UMC4M中进行验证: 首先, 将性质的定义加入到MSVL程序中, 并把MSVL程序放在m文件中, PPTL公式alw(m- > som n) and alw(!(f and (h or r))) and alw((p and q)- > g) and alw(g- > q)等价于alw(!m or (som n)) and alw(!(f and (h or r))) and alw(!(p and q) or g) and alw(!g or q), 在p文件中输入待验证的PPTL公式, 具体如下所示:

⟨/

define m: m_flag=1;  //定义命题m

define n: n_flag=1;  //定义命题n

define f: f_flag=1;  //定义命题f

define h: h_flag=1;  //定义命题h

define r: r_flag=1;  //定义命题r

define g: g_flag=1;  //定义命题g

define p: p_flag=1;  //定义命题p

define q: q_flag=1;  //定义命题q

alw(!m or (som n)) and alw(!(f and (h or r))) and alw(!(p and q) or g) and alw(!g or q)

/⟩

运行UMC4M检测器, 验证结果为性质不满足.经过对性质5~性质7的分别验证, 发现性质5与性质7满足而性质6不满足, 表明存在重入攻击漏洞, 攻击者劫持了外部调用, 并在fallback回退函数中再次调用本合约中的函数, 实现了无限转账.

4.3 对比实验

实验环境为64位Windows 7系统, 3.2GHz Intel(R) Core(TM) i5处理器, 32GB内存.为了展示SOL2M工具将Solidity程序转换为MSVL程序的能力, 如表 12所示挑选了9个典型Solidity程序.程序列给出了Solidity程序的名称, LOC列给出了Solidity程序的规模(行), LOM列给出了从Solidity程序转换而来的MSVL程序的规模, 时间列显示了完成转换任务所花费的时间.实验结果表明: 对于这些典型的Solidity程序, SOL2M工具都可以有效地转换为MSVL程序, 生成的MSVL程序的规模约是Solidity程序的2.25倍.

下面通过与Oyente工具进行比较, 来分析UMC4M的有效性.从以上9个程序中挑选5个进行实验, 表 13给出了验证的实验结果.程序列给出了Solidity程序的名称, 堆栈深度攻击漏洞、交易订单依赖、时间戳依赖、可重入漏洞列给出了验证的安全性质, 每列下分别给出了UMC4M和Oyente的验证结果.√表示智能合约不存在该安全漏洞, 而×表示存在该安全漏洞.验证时间列给出了UMC4M和Oyente验证所花费的时间.实验结果表明: UMC4M和Oyente的验证结果大部分相同, 但前者能发现governmental.sol的堆栈深度攻击漏洞和时间戳依赖, 且能发现racecondition.sol的交易订单依赖, 后者均不能发现这些安全漏洞.另外, UMC4M的验证时间已经包含了Solidity程序到MSVL程序的转换时间, 只占Oyente的31%.

5 相关工作

目前, 国内外学者针对智能合约安全问题给出了多种形式化验证方法, 主要分为3类: 定理证明、符号执行以及模型检测.

Bhargavan等人提出了智能合约验证框架^[14]并开发了Solidity*工具, 将Solidity智能合约源代码转换为等价的F*程序, 在源代码级别上来验证合约安全性.同时开发了EVM*工具, 在字节码级别上反编译EVM字节码, 分析字节码属性并产生等价的F*程序, 然后进行交互式证明.杨霞等人提出一种面向智能合约的高度自动化的形式化验证系统及方法, 将智能合约开发语言自动化转换为中间层语言M+代码, 然后通过形式化验证辅助器对其进行验证.在此基础上, 提出一种基于定理证明的以太坊智能合约形式化验证方法, 使用辅助验证工具Coq与Isabelle分别实现对Solidity源代码以及以太坊智能合约字节码的形式化验证^[15].一方面, 在Coq工具中建立源代码的形式化模型; 另一方面, 基于形式化操作码集在Isabelle中建立智能合约字节码的形式化模型, 之后对合约中的安全属性进行定理证明, 验证其可满足性.以上方法属于定理证明, 需要一定的人工证明, 验证效率受到一定影响.

Luu等人提出一种基于符号执行的智能合约安全性漏洞检测方法^[16], 开发了符号执行工具Oyente, 并非针对智能合约语句Solidity, 而是直接将EVM字节码和当前以太坊的全局状态输入工具, 使用Z3求解器来判定可满足性.Oyente能够在合约部署前检测其漏洞, 该方法属于符号执行, 一般只考虑符号路径的可满足性, 自动化程度较高.当合约中的判断条件较多时, 符号执行路径数量就会呈现指数级增长, 且符号执行过度依赖约束求解器的求解能力, 从而影响验证效率.

Kalra等人开发了一种基于抽象解释和符号模型检测智能合约安全性的工具ZEUS^[17], 其中包含一个能够将合约源代码转换为LLVM位码的代码转换器, 同时也能够将XACML格式的待验证性质转换为LLVM位码.最后, 将与合约及其性质等价的LLVM程序作为输入, 使用CHCs工具进行了符号模型检测.胡凯等人提出了通过Promela建模语言结合SPIN工具对智能合约安全性进行验证的方法^[18], 使用Promela对智能合约进行建模, 使用LTL描述待验证性质, 在SPIN中自动化验证模型是否满足所期待的性质, 最终给出代码是否与需求一致的结论.以上方法属于模型检测, 由于自动化程度较高, 因此能够很好地避免验证成本较大和效率低下的问题.

K框架是一个语言无关、基于可达性的逻辑验证框架, KEVM使用K框架来描述智能合约的形式化语义^[19], 并实现了语义分析工具, 例如Gas分析工具、语义调试器、程序验证器等.KEVM较难实现完整的程序分析, 且需要投入较多的人力.本文采用基于MSVL的智能合约安全性的模型检测方法, 性质描述采用的时序逻辑PPTL具有完全正则表达能力, 严格强于LTL.验证过程由模型检测器UMC4M自动完成, 当状态空间过大时会产生状态空间爆炸问题^[20].但是智能合约一般并非大型软件系统, 因此该方法能够降低验证成本并提高验证效率.

6 总结与展望

为了更好地在智能合约部署之前对其进行安全验证, 本文提出了面向MSVL与PPTL对智能合约进行安全性验证的模型检测方法, 开发了SOL2M转换器, 用于将智能合约Solidity程序转换为MSVL程序, 即实现了对智能合约的自动化建模.使用PPTL公式从功能一致性、逻辑正确性以及合约完备性这3个方面描述了智能合约模型的性质.通过投票智能合约与银行转账智能合约两个实例来说明方法的可行性.目前阶段的转换是Solidity语言的子集, 因此仍需继续对SOL2M转换器进行扩展和完善.另外, 本文所给出的转换规则是基于两个语言的词法规则和语法规则所制定, 将来的研究工作包括从数学角度证明Solidity与MSVL在表达式和基本语句上的语义等价性.