区块链智能合约安全的逆向实时模型检测方法

李书霞，王国卿,庄 雷

(郑州大学 信息工程学院，郑州 450001)

1 引 言

区块链(Blockchain)是一种特殊的分布式数据库，由密码技术和去中心化机制共同维护数据的不可篡改.区块链的三个发展阶段：区块链1.0的核心是记录交易以及确保区块链数据本身的安全唯一性和不可篡改性[1]；区块链2.0阶段是可编程金融[2]，核心为智能合约.区块链3.0阶段代表着区块链上的各种应用.三个层次都处于分布式环境中.

智能合约是一经部署便自动执行的计算机程序，在物联网等领域都有广阔的应用前景[3].狭义来讲，智能合约是由事件驱动的、具备状态的、部署于可共享的分布式数据库上的计算机程序[4].

智能合约有不可篡改性、自动执行性等优点，但在实际生活中智能合约还存有安全性问题，即使很小的bug也会产生巨大的利益损失.2016年5月,TheDAO事件因合约中存有漏洞导致以太币被盗取[5].2017年7月19日，Parity Wallet的多重签名钱包“multi-sig”代码中发现了一个漏洞，这导致钱包中的以太币账户被盗取[6].据英国和新加坡的研究人员使用Maian(1)https://github.com/MAIAN-tool/MAIAN工具分析统计，在100万份智能合约中超过34000个都有可被利用的安全隐患[7].智能合约的安全性受到严重的威胁.

关于智能合约安全问题，文献[8]NCC Group总结出智能合约中高频出现的安全问题，但未对所出现的安全问题给出相应的对策；文献[9]ContractFuzzer是第一个基于以太坊平台的智能合约安全漏洞模糊测试框架，但未提出如何避免安全问题的发生.文献[10]在以太坊环境中对智能合约的安全问题进行了相关的研究，但并没有对智能合约进一步的进行验证是否达到合约功能及性能的需求；Luu[11]等人开发了一种基于符号执行的静态分析工具Oyente，可以检测出合约中存在的问题，但并不能验证所存在问题的性质如正确性.

智能合约安全问题的主要解决方法是形式化验证.智能合约的形式化验证是将数学方法和分析工具相结合在合约的设计、开发、测试过程中验证智能合约是否满足公平性、正确性、可达性等预期的关键性质,以规范合约的生成和执行,提高合约的可靠性和执行力,支持规模化智能合约的高效生成[12].形式化验证使用的核心方法是模型检测.模型检测是有穷状态系统的自动化验证技术.论文引入模型检测方法的主要原因是：1)在验证合约时不仅高度自动验证而且验证速度极快，提高了效率；2)当智能合约所验证的性质没有满足时，将结束搜索并给出反例.

针对智能合约的现状模型检测有两种方案：正向方法和逆向方法.正向分析主要从合约提出入手，如图1所示.

图1 正向分析过程图Fig.1 Forward analysis process diagram

大多数情况下，在以太坊上无法获取智能合约的原始需求及文本规范,只能获取智能合约的代码，因此，需要采用逆向方法对智能合约代码进行模型检测.逆向分析方法的思路：首先，通过静态分析法对合约代码进行分析，从而得到合约的功能模块图；其次，检查代码是否存有安全漏洞.若代码存有安全漏洞，则需要对合约代码进行优化；最后，使用模型检测工具UPPAAL对合约进行建模，对优化后的代码进行规约，进一步对代码所存在的问题进行性质验证，使合约更加安全.逆向方法主要从合约代码入手进行分析，如图2所示.

2 智能合约安全性的逆向验证方法

2.1 代码逻辑分析

在以太坊上拿到智能合约代码后，先对整个合约代码进行粗略读取，大致了解合约所要实现的功能，并画出合约的流程图；其次，对代码每个函数仔细研读，察看是否存在安全问题如代码重入、数据溢出等问题，若存在以上问题则对合约代码进行针对性优化；最后，将代码与流程图相结合，察看是否存在不符合实际的问题如整数溢出、是否有截止日期、越权访问、多次委托等显性问题并将其进行修正如防止整数溢出、设置截止日期、设置权限等.

图2 逆向分析过程图Fig.2 Reverse analysis process diagram

2.2 模型检测的验证方法

模型检测技术应用到智能合约解决安全问题的三个步骤：合约建模、性质刻画规约、自动验证.

2.2.1 智能合约建模

若对系统验证是否满足要求，则需为其设计模型来验证系统的功能行为是否达到所需期望.首先，建模中存有状态及状态迁移.状态是指系统在某个时刻，系统中变量的取值.

定义 1.状态迁移

构建一个四元组(S,S0,R,L),其中，S是有限的状态集合，S0⊆S是初始状态的集合，R是状态发生变化的事件集合，L⊆S×R×S是状态发生状态迁移的集合.

Si→Sj的状态迁移意味着在事件A的触发下，状态由Si转为Sj，若这样的转移成立，则说明Sj经状态Si迁移而来的，那么Si的可达状态为Sj.在合约系统中，由状态S0开始，i⊆1…n,j⊆1…n,经过n次的状态迁移后，将构成整个系统的可达状态空间.

时间自动机添加了时钟因素，满足实时系统验证的需求，并能准确的描述状态迁移.

定义 2.时钟约束

若设φ为时钟约束即：

φ::=ni≤c|ni≥c|nic|φ∧φ

其中，φ∈(C),时钟集合C={n1,n2,n3,…，nn}，(C)表示C上的时钟约束集合.

定义 3.时钟自动机[13]

定义为一个六元组(C,L,l0,R,I,E).其中：C为时钟变量集；L为有限状态集合；l0∈L为初始状态位置；R是状态发生变化的事件集合；I为映射，I使每个状态都有一个时钟约束；状态转换集为E⊆L×R×(C)×2C×L，表示在合约系统中，若状态l0的时钟满足时钟约束φ，则在触发事件A下状态由l0→l并重置时钟.

合约建模，首先，为每个模块设置不同的名字，在作用域内进行参数、变量声明；其次，将每个模块抽象成所处的各种状态即系统在某个时间段内，变量的值；进而，根据合约代码的作用，为每一条边设置不同的迁移规则，如条件约束、时钟约束等；最后，将每个模块结合起来，考虑整体的智能合约系统的状态迁移集合.模板可以通过系统定义进行实例化得到具有相同特征和不同实参的状态机.根据以上的步骤就可以为每个系统的每个模块建立时间自动机的模型.

定义 4.层次自动机[14]

层次自动机定义为一个八元组(V,C,Ch,L,L0,ε,I,E).其中：V、C、Ch分别为变量、时钟、通道的集合；L为有限的状态集合；L0∈L为初始状态集合；I:L→Invariant，使每一个状态位置都有一个时钟约束；E⊆L×(Guard×Ch×Reset×{true,false}×L)是状态迁移关系，其中guard为卫式集合，reset为时钟重置集合.

2.2.2 合约规约性质刻画

在建模后，需要声明智能合约必须满足的安全性质.代码逻辑分析时，合约代码中可能会存有显性的漏洞如越权问题、截止日期问题.不仅要对其进行代码修改，还要对其进行性质验证.根据所出现的问题，将改过后的代码进行性质刻画.在模型检测中经常使用时序逻辑规约系统的性质，时序逻辑规约能时刻表现出系统随时间的变化而变化.结合智能合约简单介绍一下计算树逻辑树(computation tree logic，CTL)的性质.

CTL公式由路径量词和时序运算符构成.CTL有5个基本运算符分别是：X表示下一状态性质的满足；F表示路径中将来某个状态性质满足；G表示路径上的所有状态性质都满足；U表示两个性质的关系，其中第二个性质满足的条件是第一个性质满足；R表示U运算的逻辑非.路径量词有E和A，其中E为存在一条路径，A为所有的计算路径.

2.2.3 自动利用UPPAAL进行验证

模型检测的验证是由工具自动完成，无须人参与.时间自动机添加了时钟元素，适合实时系统，结合CTL，确定工具采用UPPAAL.

UPPAAL[15]是一种适用于实时系统的验证工具，具有高效性和实用性等优点[16].UPPAAL的编辑器是根据系统进行建模；UPPAAL的模拟器是模拟所有可能出现的状态.UPPAAL的验证器用于验证系统是否符合用户输入的表达式所体现的性质.

UPPAAL验证器中使用BNF语言对合约模型的功能进行验证.在对合约进行验证时，主要针对代码分析时所出现的问题进行针对性验证，输入语法后出现“满足该性质”，则表明此时验证性质满足该要求；若出现“不满足该性质”，则表明该性质与要求不符合，需要对该合约模型进一步修改优化，直到满足性质通过验证为止.BNF的路径公式如表1所示.

表1 路径公式Table 1 Path formula table

如果在UPPAAL验证器中，合约系统模型满足性质，则说明系统达到了功能与性能的要求及时间约束的活性合理；若没有满足性质，则将给出一个反例，可以找出错误发生的位置对其进行改正，从而确保了合约的安全性与可靠性.接下来以一个投票合约实例具体介绍逆向方法.

2.3 合约改进

合约代码中一般存在两种问题即显性问题和隐性问题.显性问题可由代码逻辑分析得出，并进行改进.隐性问题需要利用模型检测工具UPPAAL得出.在验证合约性质时，若工具给出一个错误的轨迹即检测性质的反例，则证明合约中存有隐性问题.分析错误轨迹并对合约进行改进，改进后的合约仍需要重新进行模型检测，重新验证，直到验证通过.

3 投票智能合约代码的形式化分析

3.1 合约代码功能分析

投票合约源代码来自Solidity语言文档中的案例(2)https://solidity.readthedocs.io/en/latest/solidity-by-example.html..通过对投票合约代码分析得知：投票合约中含有不同的投票活动，每个投票活动由不同的提案构成.合约中的主席即合约的创建者，通过地址为用户授权.经授权的用户有两种投票方式即亲自投票，或委托他人投票.若用户亲自投票，则在选中的提案票数加上自己的票权；若用户委托他人投票将分两种情况：

图3 投票合约系统流程图Fig.3 Voting contract system diagram

如果被委托人已投票，则在已投票的提案上直接加上委托人的票权；若被委托人没有投票，则将两人的票权加一起进行投票.用户只有一次投票或委托的权力，一旦投票，该用户不再享有投票或委托权力.投票活动结束时，将返回最高票数的提案.整个计票的过程都是系统自动执行并且公开透明.合约投票系统的流程图如图3所示.

3.2 合约代码漏洞分析

3.2.1 整数溢出

在投票合约中，提案的票数等于该提案投票的总数.投票合约经静态分析发现，当投票的总数大于2254时，数据发生溢出将导致合约的票数从零开始计数.

3.2.2 无截止日期

投票合约未设置投票的截止日期，将无法判断用户是否已经全部结束投票.若合约中的用户没有投票，合约将一直处于执行状态.

3.2.3 越权访问

合约委托函数中，未对被委托对象进行限定.若合法用户授权于一个非法用户，则非法用户(被委托人)将成为合法用户.破坏者可以通过此操作将合法用户的权限授予非法用户，让这些非法用户，影响了整个投票议程.

3.2.4 多次委托

投票合约中未对委托人和被委托人的委托次数进行限制，将发生两种缺陷.

1)U2已授权于U1，U3委托U2,…，Un委托Un-1，依次类推将形成一条委托链向前并且最终委托于U1.U3委托U2意味U3仅信任U2.

2)U1已授权于U2，U2委托U3,…，Un-1委托Un，依次类推将形成一条委托链向后并且最终委托于Un.整个过程中U1委托对象一直处于修改状态直至最后委托成功.

3.3 合约代码优化

3.3.1 整数溢出

合约代码中加入safemath函数对加法运算进行防溢出判断.当加法的结果值溢出时候，将产生回滚且不消耗gas.

3.3.2 时效性

根据2.1.2小节情况，合约中设置全局变量--timeLimit，创建合约时由主席设置投票活动的截止日期，将由函数修改器对合约有效期进行判定如Require(now<=deadline).

3.3.3 用户权限判定

合约中通过语句require(voters[_address].weight!=0)来判断用户权限，若票权大于0,则为合法用户.反之，则为非法用户.

3.3.4 拒绝多次委托

为投票用户设置布尔变量delegated，用于确认用户是否处于委托或被委托.当且仅当用户状态为false时，方可进行委托和被委托；反之，不能进行委托和被委托的操作.

4 投票智能合约的逆向形式化验证

4.1 形式化表示

根据3.2小节对合约进行改进，并对其进行建模，投票合约系统可以表示为：

BallotSystem≡Voter‖Chairperson‖Sys‖Proposal

其中，Voter表示投票用户，Chairperson表示投票主席，Sys表示系统，Proposal表示提案.模型的状态、同步通道和变量的名称及其含义分别如表2-表4所示.

根据层次时间自动机[15]语义，将voter模块形式化模型为Voter=(L1，L11，δ1，V1，C1，CH1，I1，E1),其中：

L1={Idle,Initial,L_voted,L_delegating,L_delegated}

L11={Idle}

表2 模型中状态位置的含义Table 2 Meaning of state position in the model table

表3 模型中同步通道的含义Table 3 Definition of synchronization channels in the model

表4 模型中变量的含义Table 4 Definition of variables in the model

δ1是映射函数，如图4所示.

V1={weight，flag，voted,tempWeight，tempCount}

C1={Ø}

CH1={right?,vote!,reset?,delegate?}

I1={Ø}

E1={(Idle,Ø,right？,weight=_weight,Initial),(Initial,flag==1,delegate？,weight+=tempWeight,L_delegated),(L_delegated,voted==false&&flag==1,vote!,tempCount=weight&&voted=true,L_voted),(L_voted,Ø,reset？,weight=0,Idle),(L_delegated,Ø,reset？,weight=0,Idle),(Initial,Ø,voted!,flag==1&& tempCount=weight,L_voted),(Initial,Ø,delegate!,flag==1 && weight=0&&tempWeight=weight,L_delegating),(L_delegating,Ø,reset？,weight=0,Idle),(Initial,Ø,reset？,weight=0,Idle)}

Chairperson状态模型、Sys状态模型、Proposal状态模型给合图容易得出，篇幅有限不再详述.

图4 Voter状态模型Fig.4 Voter state model

4.2 合约建模

投票合约主要有4个状态机分别是：Voter，Chairperson，Sys，Proposal,如图5～图7所示.因4个状态机是同步状态，不单独介绍.

图5 Chairperson状态模型Fig.5 Chairperson model model

图6 Sys状态模型Fig.6 Sys state model

图7 Proposal状态模型Fig.7 Proposal state model

投票合约中设置了4个用户，并对其进行实例化为voter1，voter2，voter3和voter4，4个用户设置了不同的票权(_weight)分别为1，2，3，和4.实例化4个提案，分别为proposal1，proposal2，proposal3，proposal4.初始票数voteCount=0.

在chairperson状态模型中，由ChairPerson发出changState!命令，并将初始状态的标志变量flag=0和resetFlag=0改为flag=1及resetFlag=1.投票合约Sys状态机中，初始状态的Idle接受changeState?命令后，由Idle状态转为Work工作状态.当ChairPerson发送right！命令，此时合约中Voter的初始化状态为Idle，当系统接收到right？命令，开始执行命令，对票权进行更新并将Idle状态转为Initial状态.处于Initial状态的用户，若用户发送delegate！命令，并且voted=true，则状态由Initial转为L_delegating；若用户接收delegate？命令，此时需要将票权和被委托人的票权相加，并由Initial状态转为L_delegated状态.当flag==1和voted=true,同时发送vote!命令，Initial和L_delegated状态的用户能进行投票，并转为L_voted状态.在ProposalAdd状态机中，接收vote？命令，并对voteCount进行更新.若授权、投票和委托状态，接受reset？命令且伴随flag==1时，若出现异常，则由Chairperson停止投票操作但不影响已投的票数.当异常情况被处理后，Chairperson将恢复投票功能.Chairperson发送changeState！命令，将把flag=0改为flag=1.同时，处于Sys状态机中的Stop状态接收changeState？命令，将由Stop状态转为Work状态.在投票活动结束时，主席发送reset！命令 ，flag=0，此时，另三个状态机状态也会随之回到初始状态.

投票合约全局时钟从ChairPerson发出changState!命令开始计时，伴随ChairPerson的每个操作时钟都会随之增加一个时间单位.若time>LIMITTIME，状态机Sys现有的状态转为End.4.3 性质刻画

根据2.2.2小节介绍的CTL，结合投票合约案例，列出以下5条规约性质.

P1:G┑(vote∧delegate)

用户的vote和delegate仅使用其中一项.

P2：G ┑(right∧vote)

用户的right和vote只能使用其中一个.

P3：G ┑(right∧delegate)

用户的权限只能使用其中一个.

P4：G Intervention→F (time>LIMLTTIME)

当发生超时，投票合约将结束操作.

P5：G ┑deadlock

验证合约是否存在死锁.

4.4 自动验证

通过UPPAAL验证器，验证系统状态变化是否满足预期的性质.针对投票合约的特点，投票智能合约必须满足稳健性、唯一性和时效性的特点.使用需求规范语言的BNF语法对上述性质用表达式描述，再利用验证器进行验证，分析结果是否满足预期.

1)无死锁

A[] not deadlock;

结果：满足该性质，表明系统中不存在死锁.

2)唯一性

投票合约的唯一性是指用户仅有一次投票或委托投票的机会.

A[] Voter1.L_delegated imply Voter1.voted==false

A[] Voter1.L_voted imply Voter1.voted==true

A[] Voter1.L_delegating imply Voter1.voted==true

结果：满足该性质，表明用户投票或是委托都满足唯一性.

3)时效性

合约的时效性指用户投票或是委托需要在规定范围内进行.

E[]Voter1.Initial imply(Voter1.Idle && time>100)

E[]Voter1.L_delegating imply(Voter1.L_delegated && time<=100)

E[] Voter1.Initial imply time<=100

E[] Voter1.L_delegating imply time<=100

E[] Voter1.L_delegated imply time<=100

E[] Voter1.L_voted imply time<=100

结果：均满足性质.表明用户在规定时间内行使自己的权限.

UPPAAL验证器对以上3个性质的语句进行验证，验证结果如表5所示，原验证结果如表6所示.

表5 模型检测结果Table 5 Model test resultstable

表6 模型检测结果Table 6 Model test resultstable

由模型检测结果表5与未修的原代码实验结果表6相比，修改后3个性质都通过验证，所改进后的投票合约系统满足无死锁、唯一性、有效性.因为验证已通过，故不需要进一步改进.

5 结束语

为了保障区块链智能合约的安全性，根据以太坊只提供智能合约的实际，提出一种基于时间自动机的智能合约安全的逆向形式化验证方法.通过静态分析方法得到智能合约的逻辑流程并简单分析其安全隐患，对于显而易见的问题进行改进优化；采用模型检测的方法，根据智能合约的逻辑流程对智能合约进行建模、刻画及验证；若验证通过则说明智能合约满足安全性，否则需要根据验证工具给出的反例进一步改进合约，保障其安全.结合投票智能合约实例，对所提方法的具体步骤进行了阐述和说明，选择模型检测工具UPPAAL对合约系统的功能性和安全性进行了验证，结果表明改进后的合约系统满足无死锁、唯一性、有效性等安全性质，体现了区块链不可篡改性等优势.

下一步研究工作主要有两个方面：

1)分析智能合约的传输层和数据层，综合考虑一个合约从产生到用户实际使用各个区块的变化.

2)在上述多层次的分析中，研究合约可能出现的漏洞以及完善方法.