區(qū)塊鏈智能合約安全的逆向?qū)崟r(shí)模型檢測(cè)方法

李書霞，王國(guó)卿,莊 雷

(鄭州大學(xué) 信息工程學(xué)院，鄭州 450001)

1 引 言

區(qū)塊鏈(Blockchain)是一種特殊的分布式數(shù)據(jù)庫(kù)，由密碼技術(shù)和去中心化機(jī)制共同維護(hù)數(shù)據(jù)的不可篡改.區(qū)塊鏈的三個(gè)發(fā)展階段：區(qū)塊鏈1.0的核心是記錄交易以及確保區(qū)塊鏈數(shù)據(jù)本身的安全唯一性和不可篡改性[1]；區(qū)塊鏈2.0階段是可編程金融[2]，核心為智能合約.區(qū)塊鏈3.0階段代表著區(qū)塊鏈上的各種應(yīng)用.三個(gè)層次都處于分布式環(huán)境中.

智能合約是一經(jīng)部署便自動(dòng)執(zhí)行的計(jì)算機(jī)程序，在物聯(lián)網(wǎng)等領(lǐng)域都有廣闊的應(yīng)用前景[3].狹義來(lái)講，智能合約是由事件驅(qū)動(dòng)的、具備狀態(tài)的、部署于可共享的分布式數(shù)據(jù)庫(kù)上的計(jì)算機(jī)程序[4].

智能合約有不可篡改性、自動(dòng)執(zhí)行性等優(yōu)點(diǎn)，但在實(shí)際生活中智能合約還存有安全性問(wèn)題，即使很小的bug也會(huì)產(chǎn)生巨大的利益損失.2016年5月,TheDAO事件因合約中存有漏洞導(dǎo)致以太幣被盜取[5].2017年7月19日，Parity Wallet的多重簽名錢包“multi-sig”代碼中發(fā)現(xiàn)了一個(gè)漏洞，這導(dǎo)致錢包中的以太幣賬戶被盜取[6].據(jù)英國(guó)和新加坡的研究人員使用Maian(1)https://github.com/MAIAN-tool/MAIAN工具分析統(tǒng)計(jì)，在100萬(wàn)份智能合約中超過(guò)34000個(gè)都有可被利用的安全隱患[7].智能合約的安全性受到嚴(yán)重的威脅.

關(guān)于智能合約安全問(wèn)題，文獻(xiàn)[8]NCC Group總結(jié)出智能合約中高頻出現(xiàn)的安全問(wèn)題，但未對(duì)所出現(xiàn)的安全問(wèn)題給出相應(yīng)的對(duì)策；文獻(xiàn)[9]ContractFuzzer是第一個(gè)基于以太坊平臺(tái)的智能合約安全漏洞模糊測(cè)試框架，但未提出如何避免安全問(wèn)題的發(fā)生.文獻(xiàn)[10]在以太坊環(huán)境中對(duì)智能合約的安全問(wèn)題進(jìn)行了相關(guān)的研究，但并沒(méi)有對(duì)智能合約進(jìn)一步的進(jìn)行驗(yàn)證是否達(dá)到合約功能及性能的需求；Luu[11]等人開(kāi)發(fā)了一種基于符號(hào)執(zhí)行的靜態(tài)分析工具Oyente，可以檢測(cè)出合約中存在的問(wèn)題，但并不能驗(yàn)證所存在問(wèn)題的性質(zhì)如正確性.

智能合約安全問(wèn)題的主要解決方法是形式化驗(yàn)證.智能合約的形式化驗(yàn)證是將數(shù)學(xué)方法和分析工具相結(jié)合在合約的設(shè)計(jì)、開(kāi)發(fā)、測(cè)試過(guò)程中驗(yàn)證智能合約是否滿足公平性、正確性、可達(dá)性等預(yù)期的關(guān)鍵性質(zhì),以規(guī)范合約的生成和執(zhí)行,提高合約的可靠性和執(zhí)行力,支持規(guī)模化智能合約的高效生成[12].形式化驗(yàn)證使用的核心方法是模型檢測(cè).模型檢測(cè)是有窮狀態(tài)系統(tǒng)的自動(dòng)化驗(yàn)證技術(shù).論文引入模型檢測(cè)方法的主要原因是：1)在驗(yàn)證合約時(shí)不僅高度自動(dòng)驗(yàn)證而且驗(yàn)證速度極快，提高了效率；2)當(dāng)智能合約所驗(yàn)證的性質(zhì)沒(méi)有滿足時(shí)，將結(jié)束搜索并給出反例.

針對(duì)智能合約的現(xiàn)狀模型檢測(cè)有兩種方案：正向方法和逆向方法.正向分析主要從合約提出入手，如圖1所示.

圖1 正向分析過(guò)程圖Fig.1 Forward analysis process diagram

大多數(shù)情況下，在以太坊上無(wú)法獲取智能合約的原始需求及文本規(guī)范,只能獲取智能合約的代碼，因此，需要采用逆向方法對(duì)智能合約代碼進(jìn)行模型檢測(cè).逆向分析方法的思路：首先，通過(guò)靜態(tài)分析法對(duì)合約代碼進(jìn)行分析，從而得到合約的功能模塊圖；其次，檢查代碼是否存有安全漏洞.若代碼存有安全漏洞，則需要對(duì)合約代碼進(jìn)行優(yōu)化；最后，使用模型檢測(cè)工具UPPAAL對(duì)合約進(jìn)行建模，對(duì)優(yōu)化后的代碼進(jìn)行規(guī)約，進(jìn)一步對(duì)代碼所存在的問(wèn)題進(jìn)行性質(zhì)驗(yàn)證，使合約更加安全.逆向方法主要從合約代碼入手進(jìn)行分析，如圖2所示.

2 智能合約安全性的逆向驗(yàn)證方法

2.1 代碼邏輯分析

在以太坊上拿到智能合約代碼后，先對(duì)整個(gè)合約代碼進(jìn)行粗略讀取，大致了解合約所要實(shí)現(xiàn)的功能，并畫出合約的流程圖；其次，對(duì)代碼每個(gè)函數(shù)仔細(xì)研讀，察看是否存在安全問(wèn)題如代碼重入、數(shù)據(jù)溢出等問(wèn)題，若存在以上問(wèn)題則對(duì)合約代碼進(jìn)行針對(duì)性優(yōu)化；最后，將代碼與流程圖相結(jié)合，察看是否存在不符合實(shí)際的問(wèn)題如整數(shù)溢出、是否有截止日期、越權(quán)訪問(wèn)、多次委托等顯性問(wèn)題并將其進(jìn)行修正如防止整數(shù)溢出、設(shè)置截止日期、設(shè)置權(quán)限等.

圖2 逆向分析過(guò)程圖Fig.2 Reverse analysis process diagram

2.2 模型檢測(cè)的驗(yàn)證方法

模型檢測(cè)技術(shù)應(yīng)用到智能合約解決安全問(wèn)題的三個(gè)步驟：合約建模、性質(zhì)刻畫規(guī)約、自動(dòng)驗(yàn)證.

2.2.1 智能合約建模

若對(duì)系統(tǒng)驗(yàn)證是否滿足要求，則需為其設(shè)計(jì)模型來(lái)驗(yàn)證系統(tǒng)的功能行為是否達(dá)到所需期望.首先，建模中存有狀態(tài)及狀態(tài)遷移.狀態(tài)是指系統(tǒng)在某個(gè)時(shí)刻，系統(tǒng)中變量的取值.

定義 1.狀態(tài)遷移

構(gòu)建一個(gè)四元組(S,S0,R,L),其中，S是有限的狀態(tài)集合，S0?S是初始狀態(tài)的集合，R是狀態(tài)發(fā)生變化的事件集合，L?S×R×S是狀態(tài)發(fā)生狀態(tài)遷移的集合.

Si→Sj的狀態(tài)遷移意味著在事件A的觸發(fā)下，狀態(tài)由Si轉(zhuǎn)為Sj，若這樣的轉(zhuǎn)移成立，則說(shuō)明Sj經(jīng)狀態(tài)Si遷移而來(lái)的，那么Si的可達(dá)狀態(tài)為Sj.在合約系統(tǒng)中，由狀態(tài)S0開(kāi)始，i?1…n,j?1…n,經(jīng)過(guò)n次的狀態(tài)遷移后，將構(gòu)成整個(gè)系統(tǒng)的可達(dá)狀態(tài)空間.

時(shí)間自動(dòng)機(jī)添加了時(shí)鐘因素，滿足實(shí)時(shí)系統(tǒng)驗(yàn)證的需求，并能準(zhǔn)確的描述狀態(tài)遷移.

定義 2.時(shí)鐘約束

若設(shè)φ為時(shí)鐘約束即：

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

其中，φ∈(C),時(shí)鐘集合C={n1,n2,n3,…，nn}，(C)表示C上的時(shí)鐘約束集合.

定義 3.時(shí)鐘自動(dòng)機(jī)[13]

定義為一個(gè)六元組(C,L,l0,R,I,E).其中：C為時(shí)鐘變量集；L為有限狀態(tài)集合；l0∈L為初始狀態(tài)位置；R是狀態(tài)發(fā)生變化的事件集合；I為映射，I使每個(gè)狀態(tài)都有一個(gè)時(shí)鐘約束；狀態(tài)轉(zhuǎn)換集為E?L×R×(C)×2C×L，表示在合約系統(tǒng)中，若狀態(tài)l0的時(shí)鐘滿足時(shí)鐘約束φ，則在觸發(fā)事件A下?tīng)顟B(tài)由l0→l并重置時(shí)鐘.

合約建模，首先，為每個(gè)模塊設(shè)置不同的名字，在作用域內(nèi)進(jìn)行參數(shù)、變量聲明；其次，將每個(gè)模塊抽象成所處的各種狀態(tài)即系統(tǒng)在某個(gè)時(shí)間段內(nèi)，變量的值；進(jìn)而，根據(jù)合約代碼的作用，為每一條邊設(shè)置不同的遷移規(guī)則，如條件約束、時(shí)鐘約束等；最后，將每個(gè)模塊結(jié)合起來(lái)，考慮整體的智能合約系統(tǒng)的狀態(tài)遷移集合.模板可以通過(guò)系統(tǒng)定義進(jìn)行實(shí)例化得到具有相同特征和不同實(shí)參的狀態(tài)機(jī).根據(jù)以上的步驟就可以為每個(gè)系統(tǒng)的每個(gè)模塊建立時(shí)間自動(dòng)機(jī)的模型.

定義 4.層次自動(dòng)機(jī)[14]

層次自動(dòng)機(jī)定義為一個(gè)八元組(V,C,Ch,L,L0,ε,I,E).其中：V、C、Ch分別為變量、時(shí)鐘、通道的集合；L為有限的狀態(tài)集合；L0∈L為初始狀態(tài)集合；I:L→Invariant，使每一個(gè)狀態(tài)位置都有一個(gè)時(shí)鐘約束；E?L×(Guard×Ch×Reset×{true,false}×L)是狀態(tài)遷移關(guān)系，其中g(shù)uard為衛(wèi)式集合，reset為時(shí)鐘重置集合.

2.2.2 合約規(guī)約性質(zhì)刻畫

在建模后，需要聲明智能合約必須滿足的安全性質(zhì).代碼邏輯分析時(shí)，合約代碼中可能會(huì)存有顯性的漏洞如越權(quán)問(wèn)題、截止日期問(wèn)題.不僅要對(duì)其進(jìn)行代碼修改，還要對(duì)其進(jìn)行性質(zhì)驗(yàn)證.根據(jù)所出現(xiàn)的問(wèn)題，將改過(guò)后的代碼進(jìn)行性質(zhì)刻畫.在模型檢測(cè)中經(jīng)常使用時(shí)序邏輯規(guī)約系統(tǒng)的性質(zhì)，時(shí)序邏輯規(guī)約能時(shí)刻表現(xiàn)出系統(tǒng)隨時(shí)間的變化而變化.結(jié)合智能合約簡(jiǎn)單介紹一下計(jì)算樹(shù)邏輯樹(shù)(computation tree logic，CTL)的性質(zhì).

CTL公式由路徑量詞和時(shí)序運(yùn)算符構(gòu)成.CTL有5個(gè)基本運(yùn)算符分別是：X表示下一狀態(tài)性質(zhì)的滿足；F表示路徑中將來(lái)某個(gè)狀態(tài)性質(zhì)滿足；G表示路徑上的所有狀態(tài)性質(zhì)都滿足；U表示兩個(gè)性質(zhì)的關(guān)系，其中第二個(gè)性質(zhì)滿足的條件是第一個(gè)性質(zhì)滿足；R表示U運(yùn)算的邏輯非.路徑量詞有E和A，其中E為存在一條路徑，A為所有的計(jì)算路徑.

2.2.3 自動(dòng)利用UPPAAL進(jìn)行驗(yàn)證

模型檢測(cè)的驗(yàn)證是由工具自動(dòng)完成，無(wú)須人參與.時(shí)間自動(dòng)機(jī)添加了時(shí)鐘元素，適合實(shí)時(shí)系統(tǒng)，結(jié)合CTL，確定工具采用UPPAAL.

UPPAAL[15]是一種適用于實(shí)時(shí)系統(tǒng)的驗(yàn)證工具，具有高效性和實(shí)用性等優(yōu)點(diǎn)[16].UPPAAL的編輯器是根據(jù)系統(tǒng)進(jìn)行建模；UPPAAL的模擬器是模擬所有可能出現(xiàn)的狀態(tài).UPPAAL的驗(yàn)證器用于驗(yàn)證系統(tǒng)是否符合用戶輸入的表達(dá)式所體現(xiàn)的性質(zhì).

UPPAAL驗(yàn)證器中使用BNF語(yǔ)言對(duì)合約模型的功能進(jìn)行驗(yàn)證.在對(duì)合約進(jìn)行驗(yàn)證時(shí)，主要針對(duì)代碼分析時(shí)所出現(xiàn)的問(wèn)題進(jìn)行針對(duì)性驗(yàn)證，輸入語(yǔ)法后出現(xiàn)“滿足該性質(zhì)”，則表明此時(shí)驗(yàn)證性質(zhì)滿足該要求；若出現(xiàn)“不滿足該性質(zhì)”，則表明該性質(zhì)與要求不符合，需要對(duì)該合約模型進(jìn)一步修改優(yōu)化，直到滿足性質(zhì)通過(guò)驗(yàn)證為止.BNF的路徑公式如表1所示.

表1 路徑公式Table 1 Path formula table

如果在UPPAAL驗(yàn)證器中，合約系統(tǒng)模型滿足性質(zhì)，則說(shuō)明系統(tǒng)達(dá)到了功能與性能的要求及時(shí)間約束的活性合理；若沒(méi)有滿足性質(zhì)，則將給出一個(gè)反例，可以找出錯(cuò)誤發(fā)生的位置對(duì)其進(jìn)行改正，從而確保了合約的安全性與可靠性.接下來(lái)以一個(gè)投票合約實(shí)例具體介紹逆向方法.

2.3 合約改進(jìn)

合約代碼中一般存在兩種問(wèn)題即顯性問(wèn)題和隱性問(wèn)題.顯性問(wèn)題可由代碼邏輯分析得出，并進(jìn)行改進(jìn).隱性問(wèn)題需要利用模型檢測(cè)工具UPPAAL得出.在驗(yàn)證合約性質(zhì)時(shí)，若工具給出一個(gè)錯(cuò)誤的軌跡即檢測(cè)性質(zhì)的反例，則證明合約中存有隱性問(wèn)題.分析錯(cuò)誤軌跡并對(duì)合約進(jìn)行改進(jìn)，改進(jìn)后的合約仍需要重新進(jìn)行模型檢測(cè)，重新驗(yàn)證，直到驗(yàn)證通過(guò).

3 投票智能合約代碼的形式化分析

3.1 合約代碼功能分析

投票合約源代碼來(lái)自Solidity語(yǔ)言文檔中的案例(2)https://solidity.readthedocs.io/en/latest/solidity-by-example.html..通過(guò)對(duì)投票合約代碼分析得知：投票合約中含有不同的投票活動(dòng)，每個(gè)投票活動(dòng)由不同的提案構(gòu)成.合約中的主席即合約的創(chuàng)建者，通過(guò)地址為用戶授權(quán).經(jīng)授權(quán)的用戶有兩種投票方式即親自投票，或委托他人投票.若用戶親自投票，則在選中的提案票數(shù)加上自己的票權(quán)；若用戶委托他人投票將分兩種情況：

圖3 投票合約系統(tǒng)流程圖Fig.3 Voting contract system diagram

如果被委托人已投票，則在已投票的提案上直接加上委托人的票權(quán)；若被委托人沒(méi)有投票，則將兩人的票權(quán)加一起進(jìn)行投票.用戶只有一次投票或委托的權(quán)力，一旦投票，該用戶不再享有投票或委托權(quán)力.投票活動(dòng)結(jié)束時(shí)，將返回最高票數(shù)的提案.整個(gè)計(jì)票的過(guò)程都是系統(tǒng)自動(dòng)執(zhí)行并且公開(kāi)透明.合約投票系統(tǒng)的流程圖如圖3所示.

3.2 合約代碼漏洞分析

3.2.1 整數(shù)溢出

在投票合約中，提案的票數(shù)等于該提案投票的總數(shù).投票合約經(jīng)靜態(tài)分析發(fā)現(xiàn)，當(dāng)投票的總數(shù)大于2254時(shí)，數(shù)據(jù)發(fā)生溢出將導(dǎo)致合約的票數(shù)從零開(kāi)始計(jì)數(shù).

3.2.2 無(wú)截止日期

投票合約未設(shè)置投票的截止日期，將無(wú)法判斷用戶是否已經(jīng)全部結(jié)束投票.若合約中的用戶沒(méi)有投票，合約將一直處于執(zhí)行狀態(tài).

3.2.3 越權(quán)訪問(wèn)

合約委托函數(shù)中，未對(duì)被委托對(duì)象進(jìn)行限定.若合法用戶授權(quán)于一個(gè)非法用戶，則非法用戶(被委托人)將成為合法用戶.破壞者可以通過(guò)此操作將合法用戶的權(quán)限授予非法用戶，讓這些非法用戶，影響了整個(gè)投票議程.

3.2.4 多次委托

投票合約中未對(duì)委托人和被委托人的委托次數(shù)進(jìn)行限制，將發(fā)生兩種缺陷.

1)U2已授權(quán)于U1，U3委托U2,…，Un委托Un-1，依次類推將形成一條委托鏈向前并且最終委托于U1.U3委托U2意味U3僅信任U2.

2)U1已授權(quán)于U2，U2委托U3,…，Un-1委托Un，依次類推將形成一條委托鏈向后并且最終委托于Un.整個(gè)過(guò)程中U1委托對(duì)象一直處于修改狀態(tài)直至最后委托成功.

3.3 合約代碼優(yōu)化

3.3.1 整數(shù)溢出

合約代碼中加入safemath函數(shù)對(duì)加法運(yùn)算進(jìn)行防溢出判斷.當(dāng)加法的結(jié)果值溢出時(shí)候，將產(chǎn)生回滾且不消耗gas.

3.3.2 時(shí)效性

根據(jù)2.1.2小節(jié)情況，合約中設(shè)置全局變量--timeLimit，創(chuàng)建合約時(shí)由主席設(shè)置投票活動(dòng)的截止日期，將由函數(shù)修改器對(duì)合約有效期進(jìn)行判定如Require(now<=deadline).

3.3.3 用戶權(quán)限判定

合約中通過(guò)語(yǔ)句require(voters[_address].weight!=0)來(lái)判斷用戶權(quán)限，若票權(quán)大于0,則為合法用戶.反之，則為非法用戶.

3.3.4 拒絕多次委托

為投票用戶設(shè)置布爾變量delegated，用于確認(rèn)用戶是否處于委托或被委托.當(dāng)且僅當(dāng)用戶狀態(tài)為false時(shí)，方可進(jìn)行委托和被委托；反之，不能進(jìn)行委托和被委托的操作.

4 投票智能合約的逆向形式化驗(yàn)證

4.1 形式化表示

根據(jù)3.2小節(jié)對(duì)合約進(jìn)行改進(jìn)，并對(duì)其進(jìn)行建模，投票合約系統(tǒng)可以表示為：

BallotSystem≡Voter‖Chairperson‖Sys‖Proposal

其中，Voter表示投票用戶，Chairperson表示投票主席，Sys表示系統(tǒng)，Proposal表示提案.模型的狀態(tài)、同步通道和變量的名稱及其含義分別如表2-表4所示.

根據(jù)層次時(shí)間自動(dòng)機(jī)[15]語(yǔ)義，將voter模塊形式化模型為Voter=(L1，L11，δ1，V1，C1，CH1，I1，E1),其中：

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

L11={Idle}

表2 模型中狀態(tài)位置的含義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是映射函數(shù)，如圖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狀態(tài)模型、Sys狀態(tài)模型、Proposal狀態(tài)模型給合圖容易得出，篇幅有限不再詳述.

圖4 Voter狀態(tài)模型Fig.4 Voter state model

4.2 合約建模

投票合約主要有4個(gè)狀態(tài)機(jī)分別是：Voter，Chairperson，Sys，Proposal,如圖5～圖7所示.因4個(gè)狀態(tài)機(jī)是同步狀態(tài)，不單獨(dú)介紹.

圖5 Chairperson狀態(tài)模型Fig.5 Chairperson model model

圖6 Sys狀態(tài)模型Fig.6 Sys state model

圖7 Proposal狀態(tài)模型Fig.7 Proposal state model

投票合約中設(shè)置了4個(gè)用戶，并對(duì)其進(jìn)行實(shí)例化為voter1，voter2，voter3和voter4，4個(gè)用戶設(shè)置了不同的票權(quán)(_weight)分別為1，2，3，和4.實(shí)例化4個(gè)提案，分別為proposal1，proposal2，proposal3，proposal4.初始票數(shù)voteCount=0.

在chairperson狀態(tài)模型中，由ChairPerson發(fā)出changState!命令，并將初始狀態(tài)的標(biāo)志變量flag=0和resetFlag=0改為flag=1及resetFlag=1.投票合約Sys狀態(tài)機(jī)中，初始狀態(tài)的Idle接受changeState?命令后，由Idle狀態(tài)轉(zhuǎn)為Work工作狀態(tài).當(dāng)ChairPerson發(fā)送right！命令，此時(shí)合約中Voter的初始化狀態(tài)為Idle，當(dāng)系統(tǒng)接收到right？命令，開(kāi)始執(zhí)行命令，對(duì)票權(quán)進(jìn)行更新并將Idle狀態(tài)轉(zhuǎn)為Initial狀態(tài).處于Initial狀態(tài)的用戶，若用戶發(fā)送delegate！命令，并且voted=true，則狀態(tài)由Initial轉(zhuǎn)為L(zhǎng)_delegating；若用戶接收delegate？命令，此時(shí)需要將票權(quán)和被委托人的票權(quán)相加，并由Initial狀態(tài)轉(zhuǎn)為L(zhǎng)_delegated狀態(tài).當(dāng)flag==1和voted=true,同時(shí)發(fā)送vote!命令，Initial和L_delegated狀態(tài)的用戶能進(jìn)行投票，并轉(zhuǎn)為L(zhǎng)_voted狀態(tài).在ProposalAdd狀態(tài)機(jī)中，接收vote？命令，并對(duì)voteCount進(jìn)行更新.若授權(quán)、投票和委托狀態(tài)，接受reset？命令且伴隨flag==1時(shí)，若出現(xiàn)異常，則由Chairperson停止投票操作但不影響已投的票數(shù).當(dāng)異常情況被處理后，Chairperson將恢復(fù)投票功能.Chairperson發(fā)送changeState！命令，將把flag=0改為flag=1.同時(shí)，處于Sys狀態(tài)機(jī)中的Stop狀態(tài)接收changeState？命令，將由Stop狀態(tài)轉(zhuǎn)為Work狀態(tài).在投票活動(dòng)結(jié)束時(shí)，主席發(fā)送reset！命令 ，flag=0，此時(shí)，另三個(gè)狀態(tài)機(jī)狀態(tài)也會(huì)隨之回到初始狀態(tài).

投票合約全局時(shí)鐘從ChairPerson發(fā)出changState!命令開(kāi)始計(jì)時(shí)，伴隨ChairPerson的每個(gè)操作時(shí)鐘都會(huì)隨之增加一個(gè)時(shí)間單位.若time>LIMITTIME，狀態(tài)機(jī)Sys現(xiàn)有的狀態(tài)轉(zhuǎn)為End.4.3 性質(zhì)刻畫

根據(jù)2.2.2小節(jié)介紹的CTL，結(jié)合投票合約案例，列出以下5條規(guī)約性質(zhì).

P1:G┑(vote∧delegate)

用戶的vote和delegate僅使用其中一項(xiàng).

P2：G ┑(right∧vote)

用戶的right和vote只能使用其中一個(gè).

P3：G ┑(right∧delegate)

用戶的權(quán)限只能使用其中一個(gè).

P4：G Intervention→F (time>LIMLTTIME)

當(dāng)發(fā)生超時(shí)，投票合約將結(jié)束操作.

P5：G ┑deadlock

驗(yàn)證合約是否存在死鎖.

4.4 自動(dòng)驗(yàn)證

通過(guò)UPPAAL驗(yàn)證器，驗(yàn)證系統(tǒng)狀態(tài)變化是否滿足預(yù)期的性質(zhì).針對(duì)投票合約的特點(diǎn)，投票智能合約必須滿足穩(wěn)健性、唯一性和時(shí)效性的特點(diǎn).使用需求規(guī)范語(yǔ)言的BNF語(yǔ)法對(duì)上述性質(zhì)用表達(dá)式描述，再利用驗(yàn)證器進(jìn)行驗(yàn)證，分析結(jié)果是否滿足預(yù)期.

1)無(wú)死鎖

A[] not deadlock;

結(jié)果：滿足該性質(zhì)，表明系統(tǒng)中不存在死鎖.

2)唯一性

投票合約的唯一性是指用戶僅有一次投票或委托投票的機(jī)會(huì).

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

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

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

結(jié)果：滿足該性質(zhì)，表明用戶投票或是委托都滿足唯一性.

3)時(shí)效性

合約的時(shí)效性指用戶投票或是委托需要在規(guī)定范圍內(nèi)進(jìn)行.

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

結(jié)果：均滿足性質(zhì).表明用戶在規(guī)定時(shí)間內(nèi)行使自己的權(quán)限.

UPPAAL驗(yàn)證器對(duì)以上3個(gè)性質(zhì)的語(yǔ)句進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如表5所示，原驗(yàn)證結(jié)果如表6所示.

表5 模型檢測(cè)結(jié)果Table 5 Model test resultstable

表6 模型檢測(cè)結(jié)果Table 6 Model test resultstable

由模型檢測(cè)結(jié)果表5與未修的原代碼實(shí)驗(yàn)結(jié)果表6相比，修改后3個(gè)性質(zhì)都通過(guò)驗(yàn)證，所改進(jìn)后的投票合約系統(tǒng)滿足無(wú)死鎖、唯一性、有效性.因?yàn)轵?yàn)證已通過(guò)，故不需要進(jìn)一步改進(jìn).

5 結(jié)束語(yǔ)

為了保障區(qū)塊鏈智能合約的安全性，根據(jù)以太坊只提供智能合約的實(shí)際，提出一種基于時(shí)間自動(dòng)機(jī)的智能合約安全的逆向形式化驗(yàn)證方法.通過(guò)靜態(tài)分析方法得到智能合約的邏輯流程并簡(jiǎn)單分析其安全隱患，對(duì)于顯而易見(jiàn)的問(wèn)題進(jìn)行改進(jìn)優(yōu)化；采用模型檢測(cè)的方法，根據(jù)智能合約的邏輯流程對(duì)智能合約進(jìn)行建模、刻畫及驗(yàn)證；若驗(yàn)證通過(guò)則說(shuō)明智能合約滿足安全性，否則需要根據(jù)驗(yàn)證工具給出的反例進(jìn)一步改進(jìn)合約，保障其安全.結(jié)合投票智能合約實(shí)例，對(duì)所提方法的具體步驟進(jìn)行了闡述和說(shuō)明，選擇模型檢測(cè)工具UPPAAL對(duì)合約系統(tǒng)的功能性和安全性進(jìn)行了驗(yàn)證，結(jié)果表明改進(jìn)后的合約系統(tǒng)滿足無(wú)死鎖、唯一性、有效性等安全性質(zhì)，體現(xiàn)了區(qū)塊鏈不可篡改性等優(yōu)勢(shì).

下一步研究工作主要有兩個(gè)方面：

1)分析智能合約的傳輸層和數(shù)據(jù)層，綜合考慮一個(gè)合約從產(chǎn)生到用戶實(shí)際使用各個(gè)區(qū)塊的變化.

2)在上述多層次的分析中，研究合約可能出現(xiàn)的漏洞以及完善方法.