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

（1. 華東交通大學軟件學院，江西 南昌 330013；2. 江西省計算技術研究所，江西 南昌 330003）

自2009 年中本聰[1]引入比特幣以來，分布式加密貨幣已經獲得國內外學者的關注。 加密貨幣由用戶在其網絡中公開管理， 且不依賴于任何可信方，用戶采用共識協(xié)議來維護共享的數(shù)據分類帳（區(qū)塊鏈）。 區(qū)塊鏈[2]技術因為其去中心化的特性為人們所熟知，同時，基于區(qū)塊鏈技術更廣泛的應用被人們開發(fā)出來[3]，智能合約就是其中之一。

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

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

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

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

1 智能合約公平性驗證方法

1.1 方法概述

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

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

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

1） 根據智能合約代碼所建立的形式化模型必須準確的描述合約代碼的內在邏輯。

2） 在刻畫合約公平性時，需要根據合約文本來抽象出滿足合約公平性的條件，不能直接從智能合約代碼中對公平性進行抽象，因為可能存在智能合約代碼本身的邏輯是與文本合約不一致的情況。

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

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

圖1 驗證過程Fig.1 Verification process

1.2 靜態(tài)分析

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

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

1.3 Solidity 語義分析

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

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

在對變量進行轉換時，為Solidity 中的每個全局變量定義一個對應的Promela 變量，對于Solidity中的局部變量，則定義對應的主體名前綴的全局變量來標識。

1.4 合約調用過程抽象

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

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

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

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

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

1.5 交互過程Promela 建模

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

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

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

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

1.6 智能合約公平性刻畫

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

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

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

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

2 Puzzle 合約公平性驗證

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

2.1 Puzzle 合約抽象

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

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

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

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

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

2.2 Puzzle 合約Promela 建模

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

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

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

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

通道ca1 用于提交答案的用戶和智能合約進行交互，通道ca2 用于合約擁有者和智能合約進行交互。 因為定義的通道是一對一的，所以在消息內部不需要再表明消息的發(fā)送者和接收者。

2.2.1 user 建模

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

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

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

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

2.2.2 contract 建模

使用進程proctype contract（）來定義智能合約進程，智能合約主體完成3 個操作。

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

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

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

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

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

2.2.3 owner 建模

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

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

2.3 Puzzle 合約公平性刻畫

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

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

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

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

3） 用戶收到了他應該收到的獎勵。

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

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

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

2.4 驗證結果分析

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

表3 搜索深度為33 時各個變量值Tab.3 The value of each variable at depth 33

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

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

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

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

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

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

3 結論

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

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

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