董春燕，譚 良,2

1(四川師范大學(xué) 計(jì)算機(jī)學(xué)院，成都 610101) 2(中國(guó)科學(xué)院 計(jì)算技術(shù)研究所，北京 100190)

1 引 言

智能合約[1-4]已成為第二代區(qū)塊鏈的核心功能，如以太坊、hyperledger、EOS等.狹義的智能合約可看作是運(yùn)行在分布式賬本上預(yù)置規(guī)則、具有狀態(tài)、條件響應(yīng)的，可封裝、驗(yàn)證、執(zhí)行分布式節(jié)點(diǎn)復(fù)雜行為，完成信息交換、價(jià)值轉(zhuǎn)移和資產(chǎn)管理的計(jì)算機(jī)程序[5].由于分布式環(huán)境的復(fù)雜性以及智能合約涉及復(fù)雜的時(shí)間依賴和次序依賴關(guān)系，合約代碼的不確定性和不一致性將導(dǎo)致智能合約本身存在漏洞，進(jìn)而導(dǎo)致合約執(zhí)行結(jié)果的不確定性，最終會(huì)導(dǎo)致法律責(zé)任的不確定性.因此，任意智能合約在上鏈之前應(yīng)進(jìn)行嚴(yán)格的安全測(cè)試和驗(yàn)證.否則，合約漏洞會(huì)給現(xiàn)實(shí)應(yīng)用帶來(lái)巨大的經(jīng)濟(jì)損失.如，2016年5月，史上最大的一個(gè)眾籌項(xiàng)目The DAO由于智能合約沒有進(jìn)行嚴(yán)格的安全測(cè)試和驗(yàn)證，攻擊者利用DAO.sol代碼中“splitDAO”函數(shù)在遞歸發(fā)送模式上存在的漏洞盜取了大量的以太幣[6].又如，2017年7月，Parity Wallet的多重簽名錢包“multi-sig”合約代碼中存在漏洞，使得攻擊者可以任意重置現(xiàn)有錢包的所有權(quán)和使用參數(shù)，這致使Parity Wallet中的多個(gè)以太幣賬戶被盜取[7].

Auction合約是一個(gè)公開拍賣的智能合約，廣泛應(yīng)用到競(jìng)拍、游戲和博彩等行業(yè)，如2016年開發(fā)的區(qū)塊鏈游戲The King of the Ether Throne(縮寫：KotET)[8].合約規(guī)定參與者一旦獲得權(quán)限，將永遠(yuǎn)地被記錄在區(qū)塊鏈上，而且有權(quán)獲得更多的以太幣，因此該合約吸引了智能合約關(guān)注者的廣泛參與.但在應(yīng)用過(guò)程中，合約逐漸暴露出安全問題.不成功的轉(zhuǎn)賬，會(huì)使合約擁有者始終占據(jù)合約，其他參與者將無(wú)法參與拍賣，最終導(dǎo)致“龐氏騙局”.究其原因，包括兩個(gè)方面，其一是編寫完全正確的智能合約代碼，對(duì)編程者的要求非常高，普通的編程者不容易做到；其二是合約部署到鏈上之前沒有對(duì)它進(jìn)行安全驗(yàn)證，而智能合約一旦部署上鏈就不可更改，所以當(dāng)漏洞暴露后無(wú)法補(bǔ)救，除非合約自毀[9].

形式化驗(yàn)證[10-15]是保證部署到鏈上的合約完全正確的有效方法，是解決智能合約安全問題的重要手段.本文基于Colored Petri Net(縮寫：CPN)[16-18]模型檢測(cè)對(duì)Auction合約進(jìn)行形式化驗(yàn)證.CPN技術(shù)是基于標(biāo)準(zhǔn)Petri Net進(jìn)行擴(kuò)展，并將傳統(tǒng)Petri Net中一個(gè)位置里面的不同標(biāo)記用不同的名字或者標(biāo)識(shí)號(hào)來(lái)表示.在本文中，首先將Auction合約分成兩層結(jié)構(gòu)，第一層是Auction合約整體層，第二層是合約中的關(guān)鍵操作Bid，并將Bid操作分為無(wú)攻擊模式和攻擊模式.其次，借助CPN工具模型對(duì)合約兩層結(jié)構(gòu)進(jìn)行建模.最后，通過(guò)仿真工具執(zhí)行合約，觀察合約整個(gè)執(zhí)行過(guò)程，發(fā)現(xiàn)和準(zhǔn)確定位Auction合約的邏輯漏洞.

2 相關(guān)工作

形式化驗(yàn)證是指利用精確的數(shù)學(xué)手段和強(qiáng)大的分析工具在合約的設(shè)計(jì)、開發(fā)、測(cè)試過(guò)程中驗(yàn)證合約是否滿足公平性、正確性、可達(dá)性、有界性和無(wú)二義性等預(yù)期的關(guān)鍵性質(zhì)，以規(guī)范合約的生成，提高合約的可靠性和執(zhí)行力，并支持規(guī)?；悄芎霞s的高效生成[17].形式化驗(yàn)證有多種方法，在智能合約領(lǐng)域中應(yīng)用最多的是定理證明和模型檢測(cè)[18].定理證明是指把被測(cè)試系統(tǒng)的行為和性質(zhì)都用邏輯方法來(lái)表示，基于公理和推理規(guī)則組成的形式系統(tǒng)，證明系統(tǒng)是否滿足期望的關(guān)鍵性質(zhì).目前，將定理證明應(yīng)用于智能合約的形式化驗(yàn)證已有許多成果.例如在文獻(xiàn)[19]中，Amaniet等人使用定理證明器Isabelle驗(yàn)證二進(jìn)制以太坊字節(jié)碼，在字節(jié)碼的角度進(jìn)行驗(yàn)證.在文獻(xiàn)[20]中，Yang和Lei等人提出一種新的形式化符號(hào)過(guò)程虛擬機(jī)(FSPVM)來(lái)驗(yàn)證基于Coq中Hoare邏輯的智能合約的可靠性和安全性.模型檢測(cè)[21]是一種基于狀態(tài)機(jī)的自動(dòng)化的形式化驗(yàn)證技術(shù).模型檢測(cè)首先對(duì)系統(tǒng)進(jìn)行建模，然后對(duì)模型所有可能的狀態(tài)進(jìn)行有效的檢測(cè)，以證明該模型是否滿足形式規(guī)約.如果模型不滿足所考慮的規(guī)約或?qū)傩?，則模型檢測(cè)器提供一個(gè)違反該屬性的反例，可以有效的利用這些信息進(jìn)行設(shè)計(jì)或規(guī)范.由于模型檢測(cè)是基于有限狀態(tài)機(jī)，所以它面對(duì)的最大的挑戰(zhàn)是狀態(tài)空間的爆炸.目前，模型檢測(cè)在基于行為的智能合約的形式化驗(yàn)證已取得了不少成果.如在文獻(xiàn)[22]中，Bigi等人將博弈論與形式化方法相結(jié)合，提出了一種驗(yàn)證智能合約的概率形式化模型.他們首先通過(guò)博弈論分析了智能合約的邏輯，然后構(gòu)建了該合約的概率形式化模型，最后使用PRISM工具對(duì)模型進(jìn)行了驗(yàn)證.此外，在文獻(xiàn)[23]中，Abdellatif和Brousmiche等人提出了一種新的驗(yàn)證方法，該方法不僅考慮了用戶與程序之間的交互，還考慮了環(huán)境和程序之間的交互.

到目前為止，在我們的參考文獻(xiàn)范圍內(nèi)，還未發(fā)現(xiàn)采用定理證明法或模型檢測(cè)法對(duì)Auction智能合約進(jìn)行形式化驗(yàn)證的理論成果.為此，本文針對(duì)Auction智能合約，基于模型檢測(cè)方法并采用CPN工具對(duì)其進(jìn)行形式化驗(yàn)證.與本文所采用方法相近的工作是文獻(xiàn)[15]，但文獻(xiàn)[15]并沒有針對(duì)Auction智能合約，除此以外，與文獻(xiàn)[15]相比，本文通過(guò)模型檢測(cè)法還發(fā)現(xiàn)了合約語(yǔ)言Solidity自身局限性，包括錯(cuò)誤處理函數(shù)assert()、require()、revert()等，并提出可使用CPN工具中IN/OUT端口的不同達(dá)到錯(cuò)誤處理函數(shù)的作用.

3 Auction智能合約的攻擊分析

本節(jié)分析Auction智能合約代碼，并展示對(duì)它的攻擊.

3.1 Auction智能合約

Auction合約是基于KotET事件編寫的拍賣智能合約.KotET是一個(gè)區(qū)塊鏈游戲的簡(jiǎn)稱，游戲中設(shè)立一個(gè)“贏家”，參與者們通過(guò)發(fā)送以太幣參與競(jìng)選.競(jìng)選的大致流程是：用戶A出價(jià)10 Ether成為“贏家”后，用戶B出價(jià)20 Ether，那么合約會(huì)將10 Ether退還給用戶A，并將“贏家”的位置轉(zhuǎn)給用戶B.合約如圖1所示.

圖1 Auction智能合約Fig.1 Auction smart contract

圖1中代碼第4行至第9行展示了用戶的競(jìng)價(jià)流程.仔細(xì)分析該合約代碼發(fā)現(xiàn)，該合約程序沒有語(yǔ)法錯(cuò)誤，從邏輯上看程序是正確的，從語(yǔ)義上看也是無(wú)漏洞的.但是在2016年2月6日至8日期間，很多參與者發(fā)現(xiàn)無(wú)論發(fā)送多少的以太幣給Auction合約都不能競(jìng)選成功.經(jīng)研究，發(fā)現(xiàn)該合約代碼存在拒絕服務(wù)攻擊漏洞，給攻擊者創(chuàng)造了攻擊條件.

3.2 Auction合約的攻擊分析

為了說(shuō)明Auction合約中的漏洞，我們將借助攻擊者POC合約.POC合約圖2所示.攻擊者首先實(shí)例化Auction合約，然后調(diào)用合約的bid方法，發(fā)送一部分以太幣.但攻擊者要滿足require(msg.value>highestBid)條件，才會(huì)成為“贏家”.當(dāng)有其他用戶參與競(jìng)爭(zhēng)時(shí)，如果發(fā)送了多于上一個(gè)“贏家”的以太幣，那么按照正常的流程，Auction合約將會(huì)調(diào)用POC的send()方法退回以太幣，然后讓攻擊者讓位.但是攻擊者提前在回調(diào)函數(shù)中寫了revert()，revert()函數(shù)的作用是從其他代碼塊中觸發(fā)異常來(lái)標(biāo)記錯(cuò)誤并重置當(dāng)前方法的調(diào)用，這就導(dǎo)致Auction合約中require(currentLeader.send(highestBid))永遠(yuǎn)執(zhí)行不成功，所以其他用戶無(wú)論投入多少以太幣，服務(wù)器都沒有響應(yīng)，造成拒絕服務(wù)攻擊.

圖2 POC智能合約Fig.2 POC smart contract

4 Auction智能合約的CPN模型驗(yàn)證及結(jié)果分析

本節(jié)對(duì)Auction合約進(jìn)行形式化驗(yàn)證，并對(duì)驗(yàn)證結(jié)果進(jìn)行分析.我們采用的形式化驗(yàn)證方法是模型檢測(cè)法.下面我們將首先定義Auction智能合約的屬性規(guī)約，然后介紹該合約建模及執(zhí)行過(guò)程，包括Auction合約的CPN模型、無(wú)攻擊Bid-CPN模型和有攻擊Bid-CPN模型.最后對(duì)形式化驗(yàn)證的結(jié)果進(jìn)行對(duì)比分析.

4.1 屬性規(guī)約

基于以上合約，我們將分析Auction合約應(yīng)該滿足的屬性規(guī)約.假設(shè)合約為C，規(guī)約為φn(n=1，2，3，4…)，生成對(duì)應(yīng)的合約模型M，然后證明規(guī)約φn在合約模型M中成立，這樣就證明了合約C滿足規(guī)約φn，進(jìn)而證明合約C符合預(yù)期性質(zhì).

模型M用一個(gè)八元組表示，M=(Pn,W,K，Pn_fund,W_fund,K_fund,Action[],T),其中n=1,2,3,4….Pn代表參與者們，W代表贏家，K代表在位者，Pn_fund代表參與者投入的資金數(shù)，W_fund代表贏家投入的資金數(shù)，K_fund代表在位者的資金數(shù)，Action[]代表調(diào)用合約的某個(gè)操作，T代表某一刻時(shí)間.

我們規(guī)定該合約需要滿足的規(guī)約如下：

1)Φ1=(Pn→Action[Bid])，代表任何用戶都可參與競(jìng)選；

2)Φ2=(W,T)，代表在某一時(shí)刻，Auction合約中只能存在一位“贏家”；

3)Φ3=(Pn_fund>W_fund,K=Pn,K_fund=Pn_fund)，代表當(dāng)前用戶投入的資金數(shù)若大于當(dāng)前“贏家”投入的資金數(shù)，則退回當(dāng)前“贏家”的資金數(shù)，并把當(dāng)前用戶設(shè)置為新的“贏家”，更新資金數(shù)；

4)Φ4=(Pn_fund

若Auction合約滿足以上規(guī)約條件，則證明該合約是安全無(wú)漏洞的.

4.2 合約建模及執(zhí)行過(guò)程

為使模型能具體表達(dá)Auction合約的邏輯結(jié)構(gòu)且更清晰，我們將使用CPN Tools進(jìn)行由頂向下的開發(fā)方式.先對(duì)Auction合約整體進(jìn)行建模，然后對(duì)Auction合約中主要操作Bid行為進(jìn)行建模.為明確區(qū)分非攻擊行為和攻擊行為，我們又對(duì)Bid模型分為了無(wú)攻擊Bid模型和有攻擊Bid模型.為方便描述，我們將相關(guān)定義羅列如下：

定義1.P[place]：代表位置，其中place為位置名稱；

定義2.T[transition]：代表變遷，其中transition為變遷名稱；

定義3.CS[colorset]：代表顏色集，其中colorset為顏色集名稱；

定義4.IM[initialmark]：代表初始標(biāo)記，其中initialmark為初始標(biāo)記名稱；

定義5.ARC[arc]：代表弧上綁定的數(shù)據(jù)，其中arc為數(shù)據(jù)名稱；

定義6.T[transition]≡{operation1,operation2,…}：代表執(zhí)行變遷transition將完成的操作，operation1和operation2為操作名稱；

4.2.1 Auction合約的CPN模型

Auction合約的整體建模如圖3所示.通過(guò)對(duì)Auction合約的分析，我們將設(shè)置三個(gè)位置和一個(gè)替代變遷.

圖3 Auction合約的CPN模型Fig.3 CPN model of Auction contract

·P[Competitor]：代表參與競(jìng)選的競(jìng)爭(zhēng)者們；

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

·P[Oldking]：代表“在位贏家”，說(shuō)明當(dāng)前Oldking正在Auction的位置上，這是為了方便演示之后模型中的退還操作；

·T[Bid]：替代標(biāo)簽，代表投標(biāo)操作；

此外，為了演示整體模型的執(zhí)行過(guò)程并說(shuō)明結(jié)果，我們還將定義相關(guān)顏色集和初始標(biāo)記.

·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 無(wú)攻擊Bid-CPN模型

無(wú)攻擊Bid模型如圖4所示.該模型是Auction模型中替代變遷Bid的具體實(shí)現(xiàn).該模型設(shè)置了九個(gè)位置和五個(gè)變遷.除了在上節(jié)中定義的位置和變遷外，我們還定義如下位置，未定義變遷及觸發(fā)操作將在執(zhí)行過(guò)程中進(jìn)行解釋.

·P[Competitor_id]：代表競(jìng)爭(zhēng)者的id；

·P[Competitor_bid]：代表競(jìng)爭(zhēng)者的投標(biāo)價(jià)格；

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

·P[King_bid]：代表“贏家”的投標(biāo)價(jià)格；

·P[oldking_bid]：代表“在位贏家”的投標(biāo)價(jià)格；

·P[New_bid]：代表“新贏家”的投標(biāo)價(jià)格.

接下來(lái)，我們將觀察無(wú)攻擊Bid-CPN模型的每步執(zhí)行過(guò)程，如圖5所示，每步執(zhí)行過(guò)程我們將通過(guò)矩形框出，首數(shù)字代表第N(N=0,1,2,3)步執(zhí)行步驟.

第一步執(zhí)行觸發(fā)的變遷操作為：

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]被先后觸發(fā)點(diǎn)火，P[Competitor_id]和P[Competitor_bid]分別綁定競(jìng)爭(zhēng)者的id和bidnumber(傳遞過(guò)程中id表示為accountid，bidnumber表示為accountBalance),P[King_id]和P[King_bid]分別綁定“贏家”的auc_id和ownnumber(傳遞過(guò)程中auc_id表示為kingid，ownnumber表示為kingBalance).

第二步執(zhí)行觸發(fā)的變遷操作為：

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

T[isGreaterThan]被觸發(fā)點(diǎn)火，對(duì)比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 無(wú)攻擊Bid-CPN模型Fig.4 No-attack Bid-CPN model

圖5 有攻擊Bid-CPN模型Fig.5 Attack Bid-CPN model

第三步執(zhí)行觸發(fā)的變遷操作為：

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]被先后觸發(fā)點(diǎn)火，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所示.該模型為了達(dá)到POC合約中revert()函數(shù)的效果，在圖4的基礎(chǔ)上將位置Oldking由OUT端口改為IN端口.

有攻擊的Bid模型的前兩步的執(zhí)行過(guò)程與無(wú)攻擊的Bid模型相同，不同之處在于第三步.標(biāo)識(shí)1′4傳遞到P[Oldking_bid]處后就不可再傳遞，標(biāo)識(shí)1′1傳遞到P[King_id]處就不再傳遞，標(biāo)識(shí)1′5和標(biāo)識(shí)1′2經(jīng)傳遞到了P[King_bid]和P[King_id]處.

4.3 結(jié)果分析

在4.2節(jié)中，我們首先使用CPN中的建模工具分別對(duì)Auction合約整體、無(wú)攻擊操作和有攻擊操作進(jìn)行建模，然后使用CPN中的仿真工具對(duì)合約的執(zhí)行過(guò)程進(jìn)行仿真.為方便觀察模型執(zhí)行過(guò)程及結(jié)果，我們繪制了無(wú)攻擊Bid-CPN模型仿真過(guò)程標(biāo)識(shí)傳遞圖和有攻擊Bid-CPN模型仿真過(guò)程標(biāo)識(shí)傳遞圖，如圖6和圖7所示.

圖6 無(wú)攻擊Bid-CPN模型仿真過(guò)程標(biāo)識(shí)傳遞圖Fig.6 No attack Bid-CPN model simulation process identification transfer diagram

此外，通過(guò)觀察模型執(zhí)行前后的結(jié)果，我們分別將無(wú)攻擊Bid模式和有攻擊Bid模式下Competitor、Auction、Oldking三個(gè)位置的標(biāo)識(shí)變化進(jìn)行總結(jié)，如表1和表2所示.

表1 無(wú)攻擊Bid模式下Competitor、Auction、Oldking三者的標(biāo)識(shí)變化Table 1 Changes label of Competitor,Auction and Oldking in non-attack Bid model

由表1可知，在無(wú)攻擊Bid模式下，在模型執(zhí)行前，位置Competitor初始ID為2，初始Ether為5，位置Auction初始ID為1，初始Ether為4，位置Oldking初始標(biāo)記為0，初始Ether為0；模型執(zhí)行后，位置Competitor的ID為0，Ether為0，位置Auction的ID為2，Ether為5，位置Oldking的ID為1，Ether為4.由此可知，該模型是按照Auction合約正常的邏輯流程執(zhí)行的，競(jìng)爭(zhēng)者的投標(biāo)價(jià)格大于原“贏家”，所以競(jìng)爭(zhēng)者的ID和投標(biāo)價(jià)格存入Auction，成為新的“贏家”，原“贏家”則被退回ID和投標(biāo)價(jià)格.

圖7 有攻擊Bid-CPN模型仿真過(guò)程標(biāo)識(shí)傳遞圖Fig.7 Attack Bid-CPN model simulation process identification transfer diagram

表2可知，在有攻擊Bid模式下，在模型執(zhí)行前，位置Competitor、Auction和Oldking初始標(biāo)記與無(wú)攻擊Bid模式下的相同；模型執(zhí)行后，位置Competitor的ID為0，Ether為0，位置Auction的ID為1和2，Ether為4和5，位置Oldking的ID為0，Ether為0.由此可知，Auction合約中存在兩個(gè)“贏家”，而沒有退還Oldking，這不符合Auction合約的第二條規(guī)約：Φ2=(W，T)，在某一時(shí)刻，Auction合約中只能存在一位“贏家”.由此可見該合約存在漏洞.我們對(duì)此結(jié)果進(jìn)行分析，由于標(biāo)識(shí)1′4傳遞到P[Oldking_bid]處后就不可再傳遞，標(biāo)識(shí)1′1傳遞到P[King_id]處就不再傳遞，我們可知原“贏家”拒絕接受退回的投標(biāo)，因此就一直占位Auction.標(biāo)識(shí)1′5和標(biāo)識(shí)1′2經(jīng)傳遞到了P[King_bid]和P[King_id]處，是因?yàn)镃PN Tools是用來(lái)描述并發(fā)系統(tǒng)的工具，因此可以允許兩個(gè)操作同時(shí)進(jìn)行，但是由于Auction合約只允許接受一個(gè)“贏家”，所以Auction合約還是存儲(chǔ)著原“贏家”的投標(biāo).

表2 有攻擊Bid模式下Competitor、Auction、Oldking三者的標(biāo)識(shí)變化Table 2 Changes label of Competitor,Auction and Oldking in attack Bid model

從以上形式化驗(yàn)證可以得出如下兩個(gè)結(jié)論.

結(jié)論 1.Auction的CPN模型發(fā)現(xiàn)和定位了合約的邏輯漏洞.對(duì)比圖4和圖5可發(fā)現(xiàn)，在無(wú)攻擊Bid模式下，模型將投標(biāo)低價(jià)者的ID和ETH退回，并將投標(biāo)高價(jià)者的ID和ETH更新到Auction合約，符合Auction合約的正常執(zhí)行流程；在有攻擊Bid模式下，模型并沒有成功地將投標(biāo)低價(jià)者的ID和ETH退回，可見合約是在投標(biāo)退回過(guò)程中出現(xiàn)了問題，由此可將漏洞定位到Auction合約的退回操作中.

結(jié)論 2.Auction的CPN模型還發(fā)現(xiàn)了合約語(yǔ)言的局限性.通過(guò)圖5，我們將漏洞定位到圖1的第6行require(currentLeader.send(highestBid))，攻擊者利用此漏洞，借助Solidity語(yǔ)言中fallback()函數(shù)的執(zhí)行原則和revert()錯(cuò)誤處理函數(shù)的作用，成功發(fā)動(dòng)拒絕服務(wù)攻擊.這是由于Solidity的局限性造成的.

5 總 結(jié)

自區(qū)塊鏈誕生以來(lái)，由于其去中心化、匿名性等特性，已成為學(xué)術(shù)各界研究的重要課題.習(xí)近平總書記也指出：把區(qū)塊鏈作為核心技術(shù)自主創(chuàng)新的重要突破口.在經(jīng)歷了以比特幣為代表的區(qū)塊鏈1.0時(shí)代，2013年底，以太坊創(chuàng)始人Vitalik Buterin發(fā)布白皮書《以太坊：下一代智能合約和去中心化應(yīng)用平臺(tái)》，使得區(qū)塊鏈的研究方向逐漸往區(qū)塊鏈2.0智能合約時(shí)代發(fā)展，使得區(qū)塊鏈應(yīng)用范圍擴(kuò)展到更多領(lǐng)域.但需要指出的是目前國(guó)內(nèi)外對(duì)智能合約的理論和技術(shù)研究尚處于初始階段，而且智能合約全流程均建立在代碼之上，凡是代碼，就可能存在漏洞，并且一旦部署完成，任何認(rèn)為干預(yù)都將無(wú)法改變合約，這是智能合約的優(yōu)勢(shì)，同時(shí)也成為了智能合約不可逆的主要原因.基于以上原因，智能合約的安全性問題也成為了不可忽視的主要探討課題.

針對(duì)智能合約漏洞方面的問題，本文采用形式化驗(yàn)證的方法對(duì)智能合約進(jìn)行建模，及時(shí)發(fā)現(xiàn)漏洞位置所在.區(qū)塊鏈智能合約的形式化驗(yàn)證是目前檢測(cè)和防范智能合約漏洞最有效的方法，本文選取具有拒絕服務(wù)攻擊漏洞的Auction智能合約，將形式化驗(yàn)證應(yīng)用于驗(yàn)證智能合約的安全性.基于CPN模型，對(duì)智能合約Auction進(jìn)行了形式化建模，并利用CPN模型中的仿真工具執(zhí)行模型.結(jié)果表明，通過(guò)對(duì)智能合約進(jìn)行CPN建模和模型仿真，可以完整呈現(xiàn)合約的執(zhí)行過(guò)程并發(fā)現(xiàn)漏洞.因此，后續(xù)將會(huì)對(duì)智能合約的形式化驗(yàn)證方向做進(jìn)一步研究.