董春燕，谭 良,2

1(四川师范大学 计算机学院，成都 610101) 2(中国科学院 计算技术研究所，北京 100190)

1 引 言

智能合约[1-4]已成为第二代区块链的核心功能，如以太坊、hyperledger、EOS等.狭义的智能合约可看作是运行在分布式账本上预置规则、具有状态、条件响应的，可封装、验证、执行分布式节点复杂行为，完成信息交换、价值转移和资产管理的计算机程序[5].由于分布式环境的复杂性以及智能合约涉及复杂的时间依赖和次序依赖关系，合约代码的不确定性和不一致性将导致智能合约本身存在漏洞，进而导致合约执行结果的不确定性，最终会导致法律责任的不确定性.因此，任意智能合约在上链之前应进行严格的安全测试和验证.否则，合约漏洞会给现实应用带来巨大的经济损失.如，2016年5月，史上最大的一个众筹项目The DAO由于智能合约没有进行严格的安全测试和验证，攻击者利用DAO.sol代码中“splitDAO”函数在递归发送模式上存在的漏洞盗取了大量的以太币[6].又如，2017年7月，Parity Wallet的多重签名钱包“multi-sig”合约代码中存在漏洞，使得攻击者可以任意重置现有钱包的所有权和使用参数，这致使Parity Wallet中的多个以太币账户被盗取[7].

Auction合约是一个公开拍卖的智能合约，广泛应用到竞拍、游戏和博彩等行业，如2016年开发的区块链游戏The King of the Ether Throne(缩写：KotET)[8].合约规定参与者一旦获得权限，将永远地被记录在区块链上，而且有权获得更多的以太币，因此该合约吸引了智能合约关注者的广泛参与.但在应用过程中，合约逐渐暴露出安全问题.不成功的转账，会使合约拥有者始终占据合约，其他参与者将无法参与拍卖，最终导致“庞氏骗局”.究其原因，包括两个方面，其一是编写完全正确的智能合约代码，对编程者的要求非常高，普通的编程者不容易做到；其二是合约部署到链上之前没有对它进行安全验证，而智能合约一旦部署上链就不可更改，所以当漏洞暴露后无法补救，除非合约自毁[9].

形式化验证[10-15]是保证部署到链上的合约完全正确的有效方法，是解决智能合约安全问题的重要手段.本文基于Colored Petri Net(缩写：CPN)[16-18]模型检测对Auction合约进行形式化验证.CPN技术是基于标准Petri Net进行扩展，并将传统Petri Net中一个位置里面的不同标记用不同的名字或者标识号来表示.在本文中，首先将Auction合约分成两层结构，第一层是Auction合约整体层，第二层是合约中的关键操作Bid，并将Bid操作分为无攻击模式和攻击模式.其次，借助CPN工具模型对合约两层结构进行建模.最后，通过仿真工具执行合约，观察合约整个执行过程，发现和准确定位Auction合约的逻辑漏洞.

2 相关工作

形式化验证是指利用精确的数学手段和强大的分析工具在合约的设计、开发、测试过程中验证合约是否满足公平性、正确性、可达性、有界性和无二义性等预期的关键性质，以规范合约的生成，提高合约的可靠性和执行力，并支持规模化智能合约的高效生成[17].形式化验证有多种方法，在智能合约领域中应用最多的是定理证明和模型检测[18].定理证明是指把被测试系统的行为和性质都用逻辑方法来表示，基于公理和推理规则组成的形式系统，证明系统是否满足期望的关键性质.目前，将定理证明应用于智能合约的形式化验证已有许多成果.例如在文献[19]中，Amaniet等人使用定理证明器Isabelle验证二进制以太坊字节码，在字节码的角度进行验证.在文献[20]中，Yang和Lei等人提出一种新的形式化符号过程虚拟机(FSPVM)来验证基于Coq中Hoare逻辑的智能合约的可靠性和安全性.模型检测[21]是一种基于状态机的自动化的形式化验证技术.模型检测首先对系统进行建模，然后对模型所有可能的状态进行有效的检测，以证明该模型是否满足形式规约.如果模型不满足所考虑的规约或属性，则模型检测器提供一个违反该属性的反例，可以有效的利用这些信息进行设计或规范.由于模型检测是基于有限状态机，所以它面对的最大的挑战是状态空间的爆炸.目前，模型检测在基于行为的智能合约的形式化验证已取得了不少成果.如在文献[22]中，Bigi等人将博弈论与形式化方法相结合，提出了一种验证智能合约的概率形式化模型.他们首先通过博弈论分析了智能合约的逻辑，然后构建了该合约的概率形式化模型，最后使用PRISM工具对模型进行了验证.此外，在文献[23]中，Abdellatif和Brousmiche等人提出了一种新的验证方法，该方法不仅考虑了用户与程序之间的交互，还考虑了环境和程序之间的交互.

到目前为止，在我们的参考文献范围内，还未发现采用定理证明法或模型检测法对Auction智能合约进行形式化验证的理论成果.为此，本文针对Auction智能合约，基于模型检测方法并采用CPN工具对其进行形式化验证.与本文所采用方法相近的工作是文献[15]，但文献[15]并没有针对Auction智能合约，除此以外，与文献[15]相比，本文通过模型检测法还发现了合约语言Solidity自身局限性，包括错误处理函数assert()、require()、revert()等，并提出可使用CPN工具中IN/OUT端口的不同达到错误处理函数的作用.

3 Auction智能合约的攻击分析

本节分析Auction智能合约代码，并展示对它的攻击.

3.1 Auction智能合约

Auction合约是基于KotET事件编写的拍卖智能合约.KotET是一个区块链游戏的简称，游戏中设立一个“赢家”，参与者们通过发送以太币参与竞选.竞选的大致流程是：用户A出价10 Ether成为“赢家”后，用户B出价20 Ether，那么合约会将10 Ether退还给用户A，并将“赢家”的位置转给用户B.合约如图1所示.

图1 Auction智能合约Fig.1 Auction smart contract

图1中代码第4行至第9行展示了用户的竞价流程.仔细分析该合约代码发现，该合约程序没有语法错误，从逻辑上看程序是正确的，从语义上看也是无漏洞的.但是在2016年2月6日至8日期间，很多参与者发现无论发送多少的以太币给Auction合约都不能竞选成功.经研究，发现该合约代码存在拒绝服务攻击漏洞，给攻击者创造了攻击条件.

3.2 Auction合约的攻击分析

为了说明Auction合约中的漏洞，我们将借助攻击者POC合约.POC合约图2所示.攻击者首先实例化Auction合约，然后调用合约的bid方法，发送一部分以太币.但攻击者要满足require(msg.value>highestBid)条件，才会成为“赢家”.当有其他用户参与竞争时，如果发送了多于上一个“赢家”的以太币，那么按照正常的流程，Auction合约将会调用POC的send()方法退回以太币，然后让攻击者让位.但是攻击者提前在回调函数中写了revert()，revert()函数的作用是从其他代码块中触发异常来标记错误并重置当前方法的调用，这就导致Auction合约中require(currentLeader.send(highestBid))永远执行不成功，所以其他用户无论投入多少以太币，服务器都没有响应，造成拒绝服务攻击.

图2 POC智能合约Fig.2 POC smart contract

4 Auction智能合约的CPN模型验证及结果分析

本节对Auction合约进行形式化验证，并对验证结果进行分析.我们采用的形式化验证方法是模型检测法.下面我们将首先定义Auction智能合约的属性规约，然后介绍该合约建模及执行过程，包括Auction合约的CPN模型、无攻击Bid-CPN模型和有攻击Bid-CPN模型.最后对形式化验证的结果进行对比分析.

4.1 属性规约

基于以上合约，我们将分析Auction合约应该满足的属性规约.假设合约为C，规约为φn(n=1，2，3，4…)，生成对应的合约模型M，然后证明规约φn在合约模型M中成立，这样就证明了合约C满足规约φn，进而证明合约C符合预期性质.

模型M用一个八元组表示，M=(Pn,W,K，Pn_fund,W_fund,K_fund,Action[],T),其中n=1,2,3,4….Pn代表参与者们，W代表赢家，K代表在位者，Pn_fund代表参与者投入的资金数，W_fund代表赢家投入的资金数，K_fund代表在位者的资金数，Action[]代表调用合约的某个操作，T代表某一刻时间.

我们规定该合约需要满足的规约如下：

1)Φ1=(Pn→Action[Bid])，代表任何用户都可参与竞选；

2)Φ2=(W,T)，代表在某一时刻，Auction合约中只能存在一位“赢家”；

3)Φ3=(Pn_fund>W_fund,K=Pn,K_fund=Pn_fund)，代表当前用户投入的资金数若大于当前“赢家”投入的资金数，则退回当前“赢家”的资金数，并把当前用户设置为新的“赢家”，更新资金数；

4)Φ4=(Pn_fund

若Auction合约满足以上规约条件，则证明该合约是安全无漏洞的.

4.2 合约建模及执行过程

为使模型能具体表达Auction合约的逻辑结构且更清晰，我们将使用CPN Tools进行由顶向下的开发方式.先对Auction合约整体进行建模，然后对Auction合约中主要操作Bid行为进行建模.为明确区分非攻击行为和攻击行为，我们又对Bid模型分为了无攻击Bid模型和有攻击Bid模型.为方便描述，我们将相关定义罗列如下：

定义1.P[place]：代表位置，其中place为位置名称；

定义2.T[transition]：代表变迁，其中transition为变迁名称；

定义3.CS[colorset]：代表颜色集，其中colorset为颜色集名称；

定义4.IM[initialmark]：代表初始标记，其中initialmark为初始标记名称；

定义5.ARC[arc]：代表弧上绑定的数据，其中arc为数据名称；

定义6.T[transition]≡{operation1,operation2,…}：代表执行变迁transition将完成的操作，operation1和operation2为操作名称；

4.2.1 Auction合约的CPN模型

Auction合约的整体建模如图3所示.通过对Auction合约的分析，我们将设置三个位置和一个替代变迁.

图3 Auction合约的CPN模型Fig.3 CPN model of Auction contract

·P[Competitor]：代表参与竞选的竞争者们；

·P[Auction]：代表“赢家”；

·P[Oldking]：代表“在位赢家”，说明当前Oldking正在Auction的位置上，这是为了方便演示之后模型中的退还操作；

·T[Bid]：替代标签，代表投标操作；

此外，为了演示整体模型的执行过程并说明结果，我们还将定义相关颜色集和初始标记.

·CS[COMPETITOR]=recordid:INT*bidnumber:INT；

·CS[AUCTION]=recordauc_id:INT*ownnumber:INT；

·CS[OLDKING]=recordold_id:INT*oldnumber:INT；

·IM[competitor]=1′{id=2,bidnumber=5};

·IM[auction]=1′{auc_id=1,ownnumber=4}.

4.2.2 无攻击Bid-CPN模型

无攻击Bid模型如图4所示.该模型是Auction模型中替代变迁Bid的具体实现.该模型设置了九个位置和五个变迁.除了在上节中定义的位置和变迁外，我们还定义如下位置，未定义变迁及触发操作将在执行过程中进行解释.

·P[Competitor_id]：代表竞争者的id；

·P[Competitor_bid]：代表竞争者的投标价格；

·P[King_id]：代表“赢家”的id；

·P[King_bid]：代表“赢家”的投标价格；

·P[oldking_bid]：代表“在位赢家”的投标价格；

·P[New_bid]：代表“新赢家”的投标价格.

接下来，我们将观察无攻击Bid-CPN模型的每步执行过程，如图5所示，每步执行过程我们将通过矩形框出，首数字代表第N(N=0,1,2,3)步执行步骤.

第一步执行触发的变迁操作为：

T[Start]≡ {
P[Competitor_id]=ARC[id],
P[Competitor_bid]=ARC[bidnumber]
};
T[Bind]≡ {
P[King_id]=ARC[auc_id],
P[King_bid]=ARC[ownnumber]
};

T[Start]和T[Bind]被先后触发点火，P[Competitor_id]和P[Competitor_bid]分别绑定竞争者的id和bidnumber(传递过程中id表示为accountid，bidnumber表示为accountBalance),P[King_id]和P[King_bid]分别绑定“赢家”的auc_id和ownnumber(传递过程中auc_id表示为kingid，ownnumber表示为kingBalance).

第二步执行触发的变迁操作为：

T[isGreaterThan]≡ {
P[New_bid]=P[Competitor_bid],
P[Oldking_bid]=P[King_bid]
}；

T[isGreaterThan]被触发点火，对比P[Competitor_bid]和P[King_bid],由于P[Competitor_bid]>P[King_bid]，所以将P[Competitor_bid]传递给P[New_bid]，P[King_bid]传递给P[Oldking_bid].

图4 无攻击Bid-CPN模型Fig.4 No-attack Bid-CPN model

图5 有攻击Bid-CPN模型Fig.5 Attack Bid-CPN model

第三步执行触发的变迁操作为：

T[Bid]≡ {
ARC[auc_id]=ARC[accountid],
ARC[ownnumber]=ARC[accountBalance]
};
T[Refund]≡ {
ARC[old_id]=ARC[kingid],
ARC[oldnumber]=ARC[kingBalance]
};

T[Bid]和T[Refund]被先后触发点火，T[Bid]将ARC[accountid]传递给ARC[auc_id],ARC[accountBalance]传递给ARC[ownnumber],T[Refund]将ARC[kingid]退还给ARC[old_id],ARC[kingBalance]退还给ARC[oldnumber].

4.2.3 有攻击Bid-CPN模型

有攻击的Bid模型如图5所示.该模型为了达到POC合约中revert()函数的效果，在图4的基础上将位置Oldking由OUT端口改为IN端口.

有攻击的Bid模型的前两步的执行过程与无攻击的Bid模型相同，不同之处在于第三步.标识1′4传递到P[Oldking_bid]处后就不可再传递，标识1′1传递到P[King_id]处就不再传递，标识1′5和标识1′2经传递到了P[King_bid]和P[King_id]处.

4.3 结果分析

在4.2节中，我们首先使用CPN中的建模工具分别对Auction合约整体、无攻击操作和有攻击操作进行建模，然后使用CPN中的仿真工具对合约的执行过程进行仿真.为方便观察模型执行过程及结果，我们绘制了无攻击Bid-CPN模型仿真过程标识传递图和有攻击Bid-CPN模型仿真过程标识传递图，如图6和图7所示.

图6 无攻击Bid-CPN模型仿真过程标识传递图Fig.6 No attack Bid-CPN model simulation process identification transfer diagram

此外，通过观察模型执行前后的结果，我们分别将无攻击Bid模式和有攻击Bid模式下Competitor、Auction、Oldking三个位置的标识变化进行总结，如表1和表2所示.

表1 无攻击Bid模式下Competitor、Auction、Oldking三者的标识变化Table 1 Changes label of Competitor,Auction and Oldking in non-attack Bid model

由表1可知，在无攻击Bid模式下，在模型执行前，位置Competitor初始ID为2，初始Ether为5，位置Auction初始ID为1，初始Ether为4，位置Oldking初始标记为0，初始Ether为0；模型执行后，位置Competitor的ID为0，Ether为0，位置Auction的ID为2，Ether为5，位置Oldking的ID为1，Ether为4.由此可知，该模型是按照Auction合约正常的逻辑流程执行的，竞争者的投标价格大于原“赢家”，所以竞争者的ID和投标价格存入Auction，成为新的“赢家”，原“赢家”则被退回ID和投标价格.

图7 有攻击Bid-CPN模型仿真过程标识传递图Fig.7 Attack Bid-CPN model simulation process identification transfer diagram

表2可知，在有攻击Bid模式下，在模型执行前，位置Competitor、Auction和Oldking初始标记与无攻击Bid模式下的相同；模型执行后，位置Competitor的ID为0，Ether为0，位置Auction的ID为1和2，Ether为4和5，位置Oldking的ID为0，Ether为0.由此可知，Auction合约中存在两个“赢家”，而没有退还Oldking，这不符合Auction合约的第二条规约：Φ2=(W，T)，在某一时刻，Auction合约中只能存在一位“赢家”.由此可见该合约存在漏洞.我们对此结果进行分析，由于标识1′4传递到P[Oldking_bid]处后就不可再传递，标识1′1传递到P[King_id]处就不再传递，我们可知原“赢家”拒绝接受退回的投标，因此就一直占位Auction.标识1′5和标识1′2经传递到了P[King_bid]和P[King_id]处，是因为CPN Tools是用来描述并发系统的工具，因此可以允许两个操作同时进行，但是由于Auction合约只允许接受一个“赢家”，所以Auction合约还是存储着原“赢家”的投标.

表2 有攻击Bid模式下Competitor、Auction、Oldking三者的标识变化Table 2 Changes label of Competitor,Auction and Oldking in attack Bid model

从以上形式化验证可以得出如下两个结论.

结论 1.Auction的CPN模型发现和定位了合约的逻辑漏洞.对比图4和图5可发现，在无攻击Bid模式下，模型将投标低价者的ID和ETH退回，并将投标高价者的ID和ETH更新到Auction合约，符合Auction合约的正常执行流程；在有攻击Bid模式下，模型并没有成功地将投标低价者的ID和ETH退回，可见合约是在投标退回过程中出现了问题，由此可将漏洞定位到Auction合约的退回操作中.

结论 2.Auction的CPN模型还发现了合约语言的局限性.通过图5，我们将漏洞定位到图1的第6行require(currentLeader.send(highestBid))，攻击者利用此漏洞，借助Solidity语言中fallback()函数的执行原则和revert()错误处理函数的作用，成功发动拒绝服务攻击.这是由于Solidity的局限性造成的.

5 总 结

自区块链诞生以来，由于其去中心化、匿名性等特性，已成为学术各界研究的重要课题.习近平总书记也指出：把区块链作为核心技术自主创新的重要突破口.在经历了以比特币为代表的区块链1.0时代，2013年底，以太坊创始人Vitalik Buterin发布白皮书《以太坊：下一代智能合约和去中心化应用平台》，使得区块链的研究方向逐渐往区块链2.0智能合约时代发展，使得区块链应用范围扩展到更多领域.但需要指出的是目前国内外对智能合约的理论和技术研究尚处于初始阶段，而且智能合约全流程均建立在代码之上，凡是代码，就可能存在漏洞，并且一旦部署完成，任何认为干预都将无法改变合约，这是智能合约的优势，同时也成为了智能合约不可逆的主要原因.基于以上原因，智能合约的安全性问题也成为了不可忽视的主要探讨课题.

针对智能合约漏洞方面的问题，本文采用形式化验证的方法对智能合约进行建模，及时发现漏洞位置所在.区块链智能合约的形式化验证是目前检测和防范智能合约漏洞最有效的方法，本文选取具有拒绝服务攻击漏洞的Auction智能合约，将形式化验证应用于验证智能合约的安全性.基于CPN模型，对智能合约Auction进行了形式化建模，并利用CPN模型中的仿真工具执行模型.结果表明，通过对智能合约进行CPN建模和模型仿真，可以完整呈现合约的执行过程并发现漏洞.因此，后续将会对智能合约的形式化验证方向做进一步研究.