區塊鏈智能合約安全的逆向實時模型檢測方法

李書霞，王國卿,莊 雷

(鄭州大學 信息工程學院，鄭州 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)在上述多層次的分析中，研究合約可能出現的漏洞以及完善方法.