基于CPN模型Auction智能合約的形式化驗證

董春燕，譚 良,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建模和模型仿真，可以完整呈現合約的執行過程并發現漏洞.因此，后續將會對智能合約的形式化驗證方向做進一步研究.