基于模型檢測(cè)的區(qū)塊鏈智能合約公平性形式化驗(yàn)證

肖美華，周浩洋，朱志亮，羅 敏

（1. 華東交通大學(xué)軟件學(xué)院，江西 南昌 330013；2. 江西省計(jì)算技術(shù)研究所，江西 南昌 330003）

自2009 年中本聰[1]引入比特幣以來，分布式加密貨幣已經(jīng)獲得國(guó)內(nèi)外學(xué)者的關(guān)注。 加密貨幣由用戶在其網(wǎng)絡(luò)中公開管理， 且不依賴于任何可信方，用戶采用共識(shí)協(xié)議來維護(hù)共享的數(shù)據(jù)分類帳（區(qū)塊鏈）。 區(qū)塊鏈[2]技術(shù)因?yàn)槠淙ブ行幕奶匦詾槿藗兯熘瑫r(shí)，基于區(qū)塊鏈技術(shù)更廣泛的應(yīng)用被人們開發(fā)出來[3]，智能合約就是其中之一。

智能合約可以對(duì)其編程語(yǔ)言中表示的任何一組規(guī)則進(jìn)行編碼[4-5]，其與傳統(tǒng)行業(yè)的結(jié)合可以提高該行業(yè)的效率以及安全性。 肖謙等[6]研究中國(guó)分布式電力交易的實(shí)際情況，提出了一種基于區(qū)塊鏈智能合約的分散式電力交易市場(chǎng)框架。 徐美強(qiáng)等[7]基于區(qū)塊鏈技術(shù)設(shè)計(jì)了變電站數(shù)字化配置的自動(dòng)化方案，提高了效率和安全性。 劉維揚(yáng)等[8]基于智能合約技術(shù)提出一種電動(dòng)汽車入網(wǎng)競(jìng)價(jià)機(jī)制，在實(shí)現(xiàn)電網(wǎng)負(fù)荷削峰填谷的同時(shí)，有效保障了用戶、代理商和電力調(diào)度中心的利益。

由于智能合約應(yīng)用便利，大量高價(jià)值數(shù)字資產(chǎn)利用智能合約進(jìn)行存儲(chǔ)和轉(zhuǎn)移，容易受到攻擊者的密集活動(dòng)影響。 隨著智能合約安全受到越來越多的重視，國(guó)內(nèi)外公司和研究機(jī)構(gòu)也在致力于尋找智能合約安全性驗(yàn)證的方法。 Bhargavan 等[9]將Solidity代碼和EVM 字節(jié)碼轉(zhuǎn)換成F*， 然后使用F* 類型檢查來驗(yàn)證智能合約內(nèi)存在的重大漏洞，但是其并不能完整的轉(zhuǎn)換Solidity 代碼。 Nehai 等[10]將智能合約翻譯成NuSMV 輸入語(yǔ)言， 然后使用模型檢測(cè)器對(duì)智能合約進(jìn)行驗(yàn)證，但是其轉(zhuǎn)換規(guī)則并不適合復(fù)雜的智能合約。 Bigi 等[11]將博弈論用在智能合約形式化驗(yàn)證中，使用概率模型檢測(cè)對(duì)智能合約進(jìn)行驗(yàn)證， 但是只能針對(duì)有不確定性人類行為的智能合約。 Luu 等[12]使用Oyente 工具可檢測(cè)部分重要類型的漏洞，但不能涵蓋所有已知類型的漏洞，檢測(cè)出來的結(jié)果需要人工進(jìn)行二次審計(jì)和確認(rèn)。

智能合約作為部署在區(qū)塊鏈系統(tǒng)的合同，其公平性是一個(gè)至關(guān)重要的屬性，只有保證參與合約的各方都能得到自己應(yīng)有的利益，才能使智能合約可信，從而使得智能合約可以被廣泛應(yīng)用。 智能合約的公平性問題大多是由于合約內(nèi)部的邏輯造成的，而每一個(gè)合約的內(nèi)部邏輯都不相同，這使得此類問題的檢測(cè)特別具有挑戰(zhàn)性。

本文將智能合約間互相調(diào)用的過程抽象為主體間互相發(fā)送消息的協(xié)議，用進(jìn)程表示主體，利用進(jìn)程間通信模擬智能合約的互相調(diào)用過程。 通過進(jìn)程的并發(fā)執(zhí)行來實(shí)現(xiàn)區(qū)塊鏈環(huán)境中智能合約的并發(fā)調(diào)用過程，然后使用模型檢測(cè)[13]方法對(duì)進(jìn)程執(zhí)行過程中的狀態(tài)進(jìn)行檢測(cè)。 從而發(fā)現(xiàn)智能合約調(diào)用過程中存在違反公平性約束的狀態(tài)， 進(jìn)而根據(jù)模型檢測(cè)器產(chǎn)生的反例來推出智能合約中存在的漏洞。

1 智能合約公平性驗(yàn)證方法

1.1 方法概述

智能合約是根據(jù)文本合同編寫的可以部署的區(qū)塊鏈上的可執(zhí)行代碼。 智能合約從生成到被調(diào)用一共包括以下幾個(gè)階段。

合約雙方或多方達(dá)成共識(shí)->文本合同->智能合約代碼->智能合約字節(jié)碼->調(diào)用執(zhí)行結(jié)果。

需要解決的是，由于智能合約代碼和文本合同之間的不一致導(dǎo)致其執(zhí)行結(jié)果與合同參與方預(yù)期不一致，從而使其中的某一方或多方利益受損的問題。 對(duì)智能合約進(jìn)行形式化驗(yàn)證時(shí)，需要滿足3 個(gè)條件。

1） 根據(jù)智能合約代碼所建立的形式化模型必須準(zhǔn)確的描述合約代碼的內(nèi)在邏輯。

2） 在刻畫合約公平性時(shí)，需要根據(jù)合約文本來抽象出滿足合約公平性的條件，不能直接從智能合約代碼中對(duì)公平性進(jìn)行抽象，因?yàn)榭赡艽嬖谥悄芎霞s代碼本身的邏輯是與文本合約不一致的情況。

3） 在對(duì)形式化模型進(jìn)行驗(yàn)證時(shí)，需要考慮真實(shí)合約執(zhí)行過程中所有可能出現(xiàn)的情況，例如變量值可能極大，極小，或者出現(xiàn)負(fù)值，合約的調(diào)用可能會(huì)并發(fā)執(zhí)行等等。

針對(duì)上述問題，提出基于模型檢測(cè)的智能合約公平性驗(yàn)證方法，將智能合約間的互相調(diào)用抽象成為主體互相傳遞消息的協(xié)議，將合約內(nèi)在邏輯抽象成為一個(gè)狀態(tài)遷移函數(shù)，同時(shí)對(duì)智能合約應(yīng)該滿足的公平性用線性時(shí)態(tài)邏輯[14]（linear temporal logic，LTL）公式進(jìn)行形式化描述，通過對(duì)協(xié)議執(zhí)行過程中各個(gè)主體的狀態(tài)進(jìn)行檢測(cè)，發(fā)現(xiàn)違反智能合約公平性約束的狀態(tài)以及對(duì)應(yīng)的漏洞。 具體驗(yàn)證過程如圖1 所示。

圖1 驗(yàn)證過程Fig.1 Verification process

1.2 靜態(tài)分析

在對(duì)智能合約進(jìn)行建模之前，首先對(duì)智能合約代碼進(jìn)行靜態(tài)分析，以排除直觀的錯(cuò)誤。 可以對(duì)照如表1 所示的目前已知的智能合約中常見的漏洞，如時(shí)間戳依賴、錯(cuò)誤的異常處理、整數(shù)溢出等。 這些都可以通過對(duì)代碼靜態(tài)分析發(fā)現(xiàn)。

表1 智能合約常見漏洞Tab.1 Common vulnerabilities of smart contract

1.3 Solidity 語(yǔ)義分析

為確保所建模型準(zhǔn)確的描述智能合約代碼的內(nèi)在邏輯， 需要對(duì)Solidity 編程語(yǔ)言的語(yǔ)義進(jìn)行分析[15]。 由于通過靜態(tài)分析已經(jīng)剔除了那些如整數(shù)溢出、錯(cuò)誤的異常處理等漏洞，所以建模時(shí)主要對(duì)合約的控制語(yǔ)句進(jìn)行抽象，對(duì)Solidity 語(yǔ)言的控制語(yǔ)句進(jìn)行形式化定義，定義如下

對(duì)于if 語(yǔ)句，B 表示語(yǔ)句的判斷條件，σB，σM則分別表示存儲(chǔ)在區(qū)塊鏈上的全局變量和存儲(chǔ)在智能合約內(nèi)部的局部變量，如果判斷條件為真則執(zhí)行操作O，↓表示判斷條件為假時(shí)，不做任何操作。 對(duì)于while 語(yǔ)句，若判斷條件為真，則執(zhí)行循環(huán)體內(nèi)部的操作語(yǔ)句然后再進(jìn)行判斷，若條件為假，則不做任何操作。 在使用Promela 進(jìn)行建模時(shí)， 需要將Solidity 中的控制語(yǔ)句轉(zhuǎn)換為Promela 語(yǔ)句。 定義轉(zhuǎn)換規(guī)則如下

在對(duì)變量進(jìn)行轉(zhuǎn)換時(shí)，為Solidity 中的每個(gè)全局變量定義一個(gè)對(duì)應(yīng)的Promela 變量，對(duì)于Solidity中的局部變量，則定義對(duì)應(yīng)的主體名前綴的全局變量來標(biāo)識(shí)。

1.4 合約調(diào)用過程抽象

由于公平性都是相對(duì)而言，所以在對(duì)智能合約調(diào)用過程進(jìn)行抽象時(shí)，需要描述參與合約執(zhí)行的全部主體。 用主體間發(fā)送消息來模擬智能合約間互相發(fā)送交易的調(diào)用過程，消息內(nèi)容包含交易信息以及交易所攜帶的金額。 抽象后的主體間交互過程如圖2 所示。

圖2 主體間交互抽象Fig.2 Interaction abstract between agents

以太坊中的智能合約可以看作是一個(gè)隨著執(zhí)行交易狀態(tài)不斷變換的有限狀態(tài)機(jī)。 所以在對(duì)智能合約的公平性進(jìn)行驗(yàn)證時(shí)，把參與合約執(zhí)行的主體看作一個(gè)整體。 即智能合約的執(zhí)行過程中是這個(gè)整體從一個(gè)狀態(tài)到下一個(gè)狀態(tài)的遷移過程。 本文借鑒Bai[16]中對(duì)智能合約的形式化定義并對(duì)其簡(jiǎn)化，將智能合約執(zhí)行過程定義如式（7）所示的4 元組

式中：S 為整體的當(dāng)前狀態(tài)，包括參與合約執(zhí)行的全部主體狀態(tài)，S＝（SA，SB，…）；T 為智能合約發(fā)送和接收的所有消息集合，T＝（T1，T2，…）；A 為智能合約主體所做的動(dòng)作集合，包括Send（Ti）和Receive（Ti），A＝（a1，a2， …）；F 為參與合約執(zhí)行的主體內(nèi)部函數(shù)的集合，F(xiàn)＝（FA，F(xiàn)B，…）。將主體的內(nèi)部邏輯抽象為一個(gè)函數(shù)， 函數(shù)的輸入為當(dāng)前狀態(tài)和所做的動(dòng)作，輸出為下一個(gè)狀態(tài)，即SAi+1=FA（SAi，ai）。

雖然區(qū)塊鏈上的所有計(jì)算都是確定性的，但是由于交易本身之間的競(jìng)爭(zhēng)（即由礦工為給定的區(qū)塊選擇哪些交易），仍然會(huì)發(fā)生一定數(shù)量的不確定性。這里使用Promela 語(yǔ)言中進(jìn)程的并發(fā)執(zhí)行來達(dá)到這個(gè)目的，使動(dòng)作的執(zhí)行順序在一定的規(guī)則下存在隨機(jī)性，以模擬智能合約真實(shí)的執(zhí)行環(huán)境。

1.5 交互過程Promela 建模

Promela 是一種描述并發(fā)系統(tǒng)的建模語(yǔ)言，用于有限狀態(tài)機(jī)系統(tǒng)建模，是模型檢測(cè)器SPIN 的輸入語(yǔ)言， 使用Promela 進(jìn)程間通信的方式對(duì)智能合約間互相調(diào)用的交互過程進(jìn)行建模。 在Promela 中，主體間傳遞消息并不是直接發(fā)送消息給對(duì)方， 而是發(fā)送方將消息發(fā)送到消息通道內(nèi)， 接收方從消息通道內(nèi)取出消息。 建立消息通道格式如式（8）所示

式中：ca 為通道名稱；[0] 為通道內(nèi)可以存放的消息數(shù)量。如果是同步消息傳遞，則通道內(nèi)可以存放的消息數(shù)量為0， 異步傳遞則可以設(shè)置通道內(nèi)存放的消息數(shù)量。{ }為消息內(nèi)容，包括消息數(shù)據(jù)類型的定義以及數(shù)據(jù)項(xiàng)的數(shù)目。 通道內(nèi)發(fā)送消息和接收消息如下

式（9）表示向通道ca 內(nèi)發(fā)送一條消息，消息的內(nèi)容包括x1，x2 兩條數(shù)據(jù)。式（10）表示從通道cb 內(nèi)接收兩條消息， 并將其分別賦值給變量x1，x2。Promela 消息通道中還有一種用于判斷的操作，如式（11）所示

式（11）表示從通道cb 內(nèi)接收一條消息，如果第一項(xiàng)數(shù)據(jù)等于x1，則把第二項(xiàng)數(shù)據(jù)賦值給變量x2，否則丟棄這條消息。

1.6 智能合約公平性刻畫

對(duì)于智能合約公平性的定義，不同的合約會(huì)有不同的描述。 例如，一個(gè)簡(jiǎn)單的買賣合約，如果買方先付款，賣方后發(fā)貨，就需要有對(duì)賣方不發(fā)貨這種情況的懲罰性條款，否則對(duì)于買方是不公平的。 在一個(gè)拍賣合約中，如果存在幾個(gè)投標(biāo)人私下串通然后再出價(jià)的情況，則會(huì)對(duì)其他投標(biāo)人不公平。 總的來說， 智能合約的公平性是指在合約執(zhí)行過程中，可能出現(xiàn)的所有情況內(nèi)，每一位合約參與者都能獲得自己應(yīng)有的利益。

在對(duì)具體合約安全性進(jìn)行描述時(shí)， 需要結(jié)合文本合約以及所建的形式化模型來抽象出與公平性相關(guān)的變量。使用各個(gè)變量間的關(guān)系來表示公平性。在對(duì)公平性進(jìn)行描述時(shí)， 要首先對(duì)智能合約執(zhí)行流程進(jìn)行分析，規(guī)定在一些特定的狀態(tài)時(shí)，與公平性有關(guān)的單個(gè)或多個(gè)變量應(yīng)該滿足怎樣的關(guān)系。 然后使用LTL 公式描述滿足公平時(shí)變量之間的關(guān)系。

例如對(duì)于一個(gè)簡(jiǎn)單的轉(zhuǎn)賬操作中的變量之間的關(guān)系，公平性可以描述為轉(zhuǎn)賬前后，轉(zhuǎn)出方和接收方兩人的余額之和是恒定的。 使用LTL 描述如式（12）所示

[]（balance［sender］+balance［receiver］） （12）

2 Puzzle 合約公平性驗(yàn)證

Puzzle 是一個(gè)在區(qū)塊鏈上很常見的獎(jiǎng)勵(lì)合約。合約的主要功能是對(duì)向智能合約提交問題正確答案的用戶發(fā)放獎(jiǎng)勵(lì)。 這個(gè)合約的邏輯是首先智能合約向區(qū)塊鏈網(wǎng)絡(luò)中廣播尋求問題解決答案的交易信息，交易內(nèi)包含問題描述以及賞金的金額。 然后用戶節(jié)點(diǎn)向智能合約發(fā)送提交答案的交易。 智能合約在收到答案后， 會(huì)對(duì)答案的正確性進(jìn)行驗(yàn)證，若正確則向用戶發(fā)放獎(jiǎng)勵(lì)，否則終止交易。 同時(shí)智能合約的擁有者可以向智能合約發(fā)送修改獎(jiǎng)勵(lì)金額的交易，智能合約收到交易后會(huì)驗(yàn)證交易的發(fā)送方地址，如果是合約擁有者，則會(huì)將之前存放在智能合約的獎(jiǎng)勵(lì)金額返還給合約擁有者，并將擁有者發(fā)來的交易中攜帶的金額設(shè)置為新的獎(jiǎng)勵(lì)金額。 經(jīng)過靜態(tài)分析修改后的Puzzle 合約的核心代碼如下：

2.1 Puzzle 合約抽象

參與Puzzle 合約交互的主體有3 個(gè)，分別是智能合約（contract）、合約擁有者（owner）和提交答案的用戶（user）。在區(qū)塊鏈網(wǎng)絡(luò)中交易信息是公開的，所以可以簡(jiǎn)化加解密以及身份地址認(rèn)證等操作，直接使用點(diǎn)對(duì)點(diǎn)通信的方式來表示交易信息的發(fā)送和接收，這樣能夠簡(jiǎn)化模型，避免模型檢測(cè)過程中狀態(tài)空間爆炸的問題。 Puzzle 合約主體間交互過程如圖3 所示。

圖3 主體間交互過程圖Fig.3 Interaction process diagram between agents

智能合約執(zhí)行過程中的狀態(tài)定義如式（13）所示

關(guān)于狀態(tài)定義中每個(gè)變量的意義如表2 所示。關(guān)于消息、函數(shù)及動(dòng)作集合的定義將在下一節(jié)中使用Promela 進(jìn)程來說明。

表2 變量名稱及意義Tab.2 Name and meaning of each variable

2.2 Puzzle 合約Promela 建模

在對(duì)Puzzle 合約交互過程抽象以后，可以發(fā)現(xiàn)有兩對(duì)主體互相發(fā)送交易，分別是合約和用戶以及合約和合約擁有者，通過定義兩條一對(duì)一通信的消息通道來對(duì)進(jìn)程間通信建模。 為了便于解釋下邊的消息通道定義， 需要先說明有限名稱集的定義，如式（14）所示。

mtype question，answer，update；pay，payback；contract_reward；user_data；owner_balance; （14）

前5 個(gè)名稱對(duì)應(yīng)主體間發(fā)送消息的類型，分別是發(fā)送問題，提交答案，修改獎(jiǎng)勵(lì)金額，支付賞金以及退回獎(jiǎng)勵(lì)金額，后3 個(gè)則對(duì)應(yīng)消息中的變量。 消息通道定義如式（15）所示。

chan ca1=［0］ of ｛mtype，mtype｝；chan ca2=［0］ of｛mtype，mtype｝ （15）

通道ca1 用于提交答案的用戶和智能合約進(jìn)行交互，通道ca2 用于合約擁有者和智能合約進(jìn)行交互。 因?yàn)槎x的通道是一對(duì)一的，所以在消息內(nèi)部不需要再表明消息的發(fā)送者和接收者。

2.2.1 user 建模

使用進(jìn)程proctype user（）來定義向智能合約提交答案的用戶進(jìn)程，在proctype user（）中主要對(duì)user_balance，user_reward，user_data0，user_data1 這4 個(gè)變量進(jìn)行操作。 user 進(jìn)程主要做出的動(dòng)作如式（16）所示。

user 進(jìn)程的內(nèi)部邏輯則通過Promela 語(yǔ)言中的控制語(yǔ)句以及消息通道內(nèi)的判斷操作來實(shí)現(xiàn)。 這里將user 進(jìn)程內(nèi)部的邏輯抽象為一個(gè)狀態(tài)轉(zhuǎn)移函數(shù)，函數(shù)的輸入是user 的當(dāng)前狀態(tài)以及所做的動(dòng)作，輸出為下一個(gè)狀態(tài)。 例如user 的初始狀態(tài)Suser0如式（17）所示。

Suser0（user_balance，user_reward，user_data0，user_data1）＝（0，0，1，2） （17）

則經(jīng)過執(zhí)行動(dòng)作a1 后得狀態(tài)Suser0為：Suser1＝Fuser（Suser0，a1）=（0，5，1，2），鑒于篇幅原因，這里不再列出user 進(jìn)程的Promela 代碼。

2.2.2 contract 建模

使用進(jìn)程proctype contract（）來定義智能合約進(jìn)程，智能合約主體完成3 個(gè)操作。

1） 向區(qū)塊鏈網(wǎng)絡(luò)廣播消息，來請(qǐng)求問題答案。

2） 接收來自答案提交用戶的交易信息，對(duì)答案驗(yàn)證后，按照最新的獎(jiǎng)勵(lì)金額向用戶發(fā)放獎(jiǎng)勵(lì)。 為了簡(jiǎn)化模型，省略了對(duì)答案驗(yàn)證的過程。

3） 接收來自合約擁有者的修改獎(jiǎng)勵(lì)金額的交易信息，將之前的獎(jiǎng)勵(lì)金返回給合約擁有者，然后將合約擁有者發(fā)來的交易中攜帶的金額設(shè)置為新的獎(jiǎng)勵(lì)金額。

使用兩條發(fā)送語(yǔ)句模擬向網(wǎng)絡(luò)中廣播交易。 智能合約主體的動(dòng)作定義如式（18）所示。

智能合約主體內(nèi)部函數(shù)的定義則使用Promela進(jìn)程中關(guān)于通道內(nèi)接收消息的判斷操作以及控制語(yǔ)句來實(shí)現(xiàn)。 智能合約主體內(nèi)部邏輯核心代碼如下所示。

2.2.3 owner 建模

使用進(jìn)程proctype owner（）來定義向智能合約提交答案的用戶進(jìn)程，在proctype owner（）中主要對(duì)owner_balance，owner_reward 這2 個(gè)變量進(jìn)行操作。owner 進(jìn)程主要做出的動(dòng)作如式（19）所示。

在這里假設(shè)合約擁有者在收到請(qǐng)求信息后，直接向合約發(fā)送修改價(jià)格的交易信息。 owner 進(jìn)程內(nèi)部邏輯為，在收到請(qǐng)求信息后，將其中攜帶的獎(jiǎng)勵(lì)金額的數(shù)量減少1，作為新的獎(jiǎng)勵(lì)金額發(fā)送給合約。

2.3 Puzzle 合約公平性刻畫

在對(duì)智能合約的公平性進(jìn)行刻畫時(shí)， 需要考慮智能合約是否完美的實(shí)現(xiàn)了它的功能且沒有出現(xiàn)任何不允許出現(xiàn)的狀態(tài)。 在Puzzle 合約中，要達(dá)到的目的就是提交答案的用戶和合約擁有者能夠公平的完成交易。 因?yàn)槭÷粤舜鸢蛤?yàn)證以及地址驗(yàn)證等操作，所以要公平的完成交易，就需要滿足以下3 點(diǎn)。

屬性1 提交答案的用戶在提交正確答案后， 最終能夠收到他接收問題時(shí)所觀察到的獎(jiǎng)勵(lì)金額。 即總是存在以下3 種狀態(tài)中的一種：

1） 用戶還沒有發(fā)送答案。

2） 用戶發(fā)送了答案但是還沒有收到錢。

3） 用戶收到了他應(yīng)該收到的獎(jiǎng)勵(lì)。

使用LTL 公式描述如式（20）所示。

屬性2 合約擁有者在發(fā)送了新的獎(jiǎng)勵(lì)金額給智能合約后， 安全的收到智能合約返還的獎(jiǎng)勵(lì)金額，且與他所觀察到的修改前的獎(jiǎng)勵(lì)金額相等。 使用LTL公式描述如式（21）所示。

屬性3 合約在向用戶發(fā)送完獎(jiǎng)勵(lì)以后， 合約內(nèi)一定存有正確的答案。這里使用user_balance!=0 來表示合約向用戶付款成功。 即contract_data 一定在user_balance!=0 變?yōu)檎嬷盀檎妗Ｊ褂肔TL 公式描述如式（22）所示。

2.4 驗(yàn)證結(jié)果分析

將上述模型在SPIN6.4.9，Ispin 1.1.4 中運(yùn)行，驗(yàn)證結(jié)果表明在搜索深度為33 時(shí)， 公平性約束被違反，查看深度33 時(shí)各個(gè)變量的值如表3 所示。

表3 搜索深度為33 時(shí)各個(gè)變量值Tab.3 The value of each variable at depth 33

在深度33 時(shí)owner_balance 與owner_reward相等,即擁有者的公平得到了保證，但是當(dāng)user_data0=0，即用戶提交了答案以后，用戶最后得到的獎(jiǎng)勵(lì)與他接收問題時(shí)所觀察到的不同，user_balance 不等于user_reward，即用戶的公平性沒有得到保證。 查看違反公平性時(shí)的消息序列如圖4 所示。 當(dāng)公平性被違反時(shí)，主體間交互過程如圖5 所示。

圖4 公平性違反時(shí)消息序列Fig.4 Message sequence graph for fairness violation

圖5 主體間交互過程Fig.5 Interaction process between agents

為了更加細(xì)致的分析造成公平性被違反的原因，需要根據(jù)主體間的交互過程來刻畫智能合約的狀態(tài)遷移序列。 Puzzle 合約狀態(tài)遷移如圖6 所示（*標(biāo)記值發(fā)生變化的變量）， 這里僅列出與公平性有關(guān)的變量。

圖6 Puzzle 合約公平性違反時(shí)狀態(tài)遷移圖Fig.6 State transition graph for fairness violation of Puzzle contract

由此可知Puzzle 合約不滿足公平性是因?yàn)橛脩艉秃霞s擁有者兩個(gè)主體同時(shí)發(fā)送交易調(diào)用了智能合約， 由于同一區(qū)塊內(nèi)交易執(zhí)行順序的隨機(jī)性，導(dǎo)致用戶接收的獎(jiǎng)勵(lì)是被合約擁有者修改以后的獎(jiǎng)勵(lì)金額。 即用戶沒有收到他接收問題時(shí)所看到的獎(jiǎng)勵(lì)金額。 結(jié)合文獻(xiàn)[12]中對(duì)交易順序依賴漏洞的分析，Puzzle 合約中存在交易順序依賴漏洞，對(duì)提交答案的用戶是不公平的。 通過上述實(shí)驗(yàn)證明，發(fā)現(xiàn)Puzzle 合約中存在公平性漏洞， 證明了本文中提出方法的可行性。

3 結(jié)論

本文提出一種基于模型檢測(cè)的智能合約公平性驗(yàn)證方法，將智能合約執(zhí)行過程抽象為主體間交互的協(xié)議，模擬智能合約間并發(fā)調(diào)用的過程，使用LTL 公式對(duì)智能合約需要滿足的公平屬性進(jìn)行刻畫， 使用模型檢測(cè)器SPIN 對(duì)智能合約公平性進(jìn)行驗(yàn)證。

1） 解決了使用模型檢測(cè)方法對(duì)智能合約進(jìn)行驗(yàn)證時(shí)，所建立的模型只能針對(duì)一種類型合約的問題，為發(fā)現(xiàn)智能合約并發(fā)調(diào)用時(shí)產(chǎn)生的漏洞提供了新的方法。 使用該方法對(duì)Puzzle 合約公平性進(jìn)行驗(yàn)證，發(fā)現(xiàn)該合約存在交易順序依賴漏洞。

2） 本方法目前僅適用于使用Solidity 編寫的智能合約， 未來工作將致力于擴(kuò)展語(yǔ)言轉(zhuǎn)換規(guī)則，以及屬性刻畫方法。 使其可以對(duì)其他語(yǔ)言編寫的智能合約的更多屬性進(jìn)行驗(yàn)證以致于可以發(fā)現(xiàn)更多類型的漏洞，同時(shí)也將致力于實(shí)現(xiàn)對(duì)智能合約主體間交互過程建模的自動(dòng)化。