朱 雪 陽

(1.中國科學院 軟件研究所 計算機科學國家重點實驗室，北京100190；2.中國科學院大學，北京100049)

0 引言

化名為“中本聰”(Satoshi Nakamoto)的學者于2008年提出了比特幣概念并于2009 年初發(fā)行了最初的50 個比特幣[1]。隨后，人們發(fā)現(xiàn)比特幣底層所用的區(qū)塊鏈技術(shù)并不僅僅限于加密數(shù)字貨幣的應(yīng)用[2]；特別是提供智能合約[3]編程的開放區(qū)塊鏈平臺以太坊(Ethereum)[4]的創(chuàng)立，使區(qū)塊鏈技術(shù)的發(fā)展更加生機勃勃。

區(qū)塊鏈是一種將數(shù)據(jù)區(qū)塊按照時間順序組織起來的加密鏈式結(jié)構(gòu)，是一種不可篡改和不可偽造的去中心化共享賬本。加入智能合約后，區(qū)塊鏈技術(shù)可看作是一種新型的去中心化基礎(chǔ)架構(gòu)與分布式計算范式[5]。有了智能合約，開發(fā)人員能夠在區(qū)塊鏈上建立和發(fā)布各種分布式應(yīng)用，為區(qū)塊鏈技術(shù)的應(yīng)用提供了無限的可能。

智能合約最初由SZABO N 提出[6](1997 年正式發(fā)表[7])，是以數(shù)字形式定義的一組承諾，以及合約參與方執(zhí)行這些承諾所需的協(xié)議。智能合約的本質(zhì)是運行于區(qū)塊鏈這一去中心化基礎(chǔ)架構(gòu)上的分布式程序，是運行在共享區(qū)塊鏈數(shù)據(jù)賬本上的商業(yè)邏輯，在被觸發(fā)時自動執(zhí)行。

正如軟件在網(wǎng)絡(luò)安全的研究與實踐中扮演著至關(guān)重要的角色，幾乎所有的網(wǎng)絡(luò)攻擊都是利用系統(tǒng)軟件或應(yīng)用軟件中存在的安全缺陷實施的[8]。在區(qū)塊鏈系統(tǒng)安全中，智能合約也扮演著重要的角色。如著名的The DAO 事件[9]，由于智能合約中存在安全漏洞，黑客得以竊取在當時價值超過五千萬美元的360 萬個以太幣。智能合約的安全(security)問題得到廣泛關(guān)注[10]；許多用于合約漏洞檢查的原型工具應(yīng)運而生，如采用符號化執(zhí)行[11]方法的工具Oyente[12]、Mythril[13]、Manticore[14]和Securify[15]等，以及在線檢查合約漏洞的工具如文獻[16]和文獻[17]等。

在The DAO 事件中，造成重大損失的根源在于合約中存在一種被稱為重入(Reentrancy)漏洞的錯誤。本文通過形式化分析來更清晰地展示該漏洞特點及攻擊行為，并以此為例介紹基于模型檢測技術(shù)的智能合約形式化驗證方法。

1 DAO 合約及重入漏洞

本質(zhì)上，一個智能合約文本描述了一個類，部署上鏈后，相當于生成一個該類的實例對象；鏈上的合約對象之間、外部地址與合約之間通過消息傳遞通信。因此，智能合約的設(shè)計及行為方式本質(zhì)上遵從面向?qū)ο蠓妒健橥怀鏊治龅膯栴}，參照文獻[16]的方法，將The DAO 合約中與重入漏洞相關(guān)的代碼提取表示為如圖1 所示的DAO 對象。

圖1 表示合約DAO 的一個對象[16]

為便于闡述問題，將合約的余額balance 顯式地定義在DAO 對象中。每個合約的參與對象o 有一個賬號余額credit[o]。參與對象可通過調(diào)用方法deposit()存入一定數(shù)額的以太幣，其余額相應(yīng)增加；也可通過調(diào)用方法withdrawAll()將其存入的以太幣全部取出，其余額清零。顯然，在這個合約中，余額一致性要得到滿足：對合約DAO 的任何操作都要保證DAO 的余額(balance) 是所有參與對象余額(credit[o])的總和。即合約應(yīng)滿足不變式(Invariant)：(sum o: credit[o])=balance。

僅從DAO 合約看，這一要求似乎一定能得到滿足：方法deposit()在第6 行增加完credit[o]后接著在第7 行相應(yīng)增加balance；方法withdrawAll()在第3行從balance 中扣減對象o 的余額并在第5 行將credit[o]清零。當withdrawAll()執(zhí)行時，會調(diào)用對象o的方法pay()。如果參與對象是圖2 左列所示Good-Client，上述不變式確實能夠得到滿足。但是，由于DAO 合約部署在區(qū)塊鏈上，任何外部對象都有可能對它進行操作，結(jié)果可能出乎合約設(shè)計者的預(yù)料。例如，如果參與對象是圖2 右列所示的Attacker，那么它的方法pay() 將回調(diào)Dao.withdrawAll()，引起DAO 的狀態(tài)變化，并破壞上述不變式。

圖2 合約DAO 的可能調(diào)用對象[16]

所以，DAO 合約存在的使重入攻擊有可能實現(xiàn)的漏洞，一般稱為重入漏洞。The DAO 事件中，攻擊者正是利用這一漏洞竊取了大量以太幣。

重入漏洞的產(chǎn)生主要是對使用模式的不確定性估計不足，只考慮到合規(guī)的使用而沒預(yù)料到可能的攻擊模式。工具如Oyente 等只要檢測到有回調(diào)情況就匯報該漏洞，存在誤報的情況。因為回調(diào)并不是產(chǎn)生重入漏洞的必然原因。例如，將DAO 合約中第5 句移到第2.5 句，則無論GoodClient 還是Attacker都不會破壞余額一致性，任何參與對象都不可能取出超過其余額的以太幣。

2 基于模型檢測的漏洞分析方法

模型檢測[18]是基于狀態(tài)搜索的一種形式化驗證方法，是模擬和測試方法的自然延伸。它是迄今為止最為成功的形式化方法，在計算機硬件、軟件、網(wǎng)絡(luò)與通信協(xié)議、控制系統(tǒng)、認證協(xié)議等領(lǐng)域都得到應(yīng)用。在智能合約驗證方面也有一些嘗試[19-21]。

模型檢測工具應(yīng)用算法自動驗證并發(fā)系統(tǒng)抽象模型是否滿足給定性質(zhì)，對不滿足性質(zhì)的模型能生成反例。比較著名的模型檢測工具有SPIN[22]、NuSMV[23]和UPPAAL[24]等?；谀Ｐ蜋z測的漏洞分析如圖3 所示。

圖3 基于模型檢測的分析框架示意圖

本文工作基于UPPAAL 介紹利用模型檢測技術(shù)檢測重入漏洞的方法。以下幾節(jié)分別介紹如何構(gòu)建DAO 合約的形式模型、余額一致性的邏輯公式表示以及如何從UPPAAL 所返回的結(jié)果中分析重入攻擊行為。

3 重入漏洞的形式模型

本文用UPPAAL 的形式模型——時間自動機來描述合約語義。由于本例未涉及時間相關(guān)特性，因此以下簡稱自動機。用UPPAAL 的性質(zhì)描述語言——分支時序邏輯(CTL)來表示余額一致性性質(zhì)。

自動機由節(jié)點和邊組成，每條邊包含三類屬性：條件(Guard)、狀態(tài)更新操作(Update)和同步操作(Sync)。僅當邊上條件被滿足并且所需接收的信號到達時，邊所表示的由一個節(jié)點到另一個節(jié)點的轉(zhuǎn)換才可能發(fā)生。合約內(nèi)或合約之間的函數(shù)調(diào)用行為可看作是多個自動機的并發(fā)。更詳細的語義細節(jié)將結(jié)合DAO 合約的形式模型來介紹。

為考察DAO.withdrawAll()的行為，需構(gòu)建三個自動機：

(1)自動機DAO_w。模擬DAO.withdrawAll()的執(zhí)行過程，如圖4(a)所示。DAO_w 初始處于idle 狀態(tài)，當收到調(diào)用信號（callW[Cid]?）時啟動，如果DAO.withdrawAll()中第二行的條件不滿足，則經(jīng)由邊e2轉(zhuǎn)到結(jié)束狀態(tài)，再發(fā)出執(zhí)行結(jié)束信號（endW[Cid]! ）完成函數(shù)的一次執(zhí)行;否則經(jīng)由e3 執(zhí)行相應(yīng)操作，并在e4 發(fā)出調(diào)用Client.pay()的信號(callP[Cid]！ )，然后等待其執(zhí)行結(jié)束并返回(endP[Cid]?)，收到返回信號后，將變量credit[0]賦值為0。接著結(jié)束并發(fā)出執(zhí)行結(jié)束信號(endW[Cid]?)，完成DAO.withdrawAll()的一次執(zhí)行。

(2)自動機Client_p。模擬Client.pay()的行為，如圖4(b)所示。由于自動機可以表示不確定轉(zhuǎn)換，無論圖2 所示的參與對象GoodClient 還是Attacker 中的pay()的行為，都可在同一自動機中描述。Client_p初始處于idle 狀態(tài)，接收到調(diào)用信號(callP[Cid]？)時啟動。接著，如果pay()中沒有回調(diào)行為(如Good-Client.pay())，執(zhí)行轉(zhuǎn)換e2，然后發(fā)送執(zhí)行結(jié)束信號(endP[Cid]! )；如果包含回調(diào)行為(如Attacker.pay())，執(zhí)行轉(zhuǎn)換e3，并發(fā)送對DAO.withdrawAll()的調(diào)用信號(callW[Cid+1]！ )(此時，上一次，即第Cid 次的調(diào)用還未結(jié)束，故為第Cid+1 次)。等待這次調(diào)用結(jié)束(接收到執(zhí)行結(jié)束信號endW[Cid+1]?)后，發(fā)送自身進程結(jié)束信號(endP[Cid]! )。

(3)自動機initCaller。模擬對DAO.withdrawAll()進行初始調(diào)用動作，如圖4(c)所示。initCaller 通過發(fā)送對DAO.withdrawAll()的調(diào)用信號(callW[0]! )啟動一次交易；當它接收到對應(yīng)的DAO.withdrawAll()執(zhí)行結(jié)束信號(endW[0]?)時，結(jié)束整個執(zhí)行，即結(jié)束一次交易。為方便隨后的性質(zhì)驗證與分析，這里還用到一個布爾變量closed，初始值設(shè)為false，在交易結(jié)束時設(shè)為true(邊e2)。

圖4 合約DAO 及其調(diào)用模型

本例中設(shè)callNum=2，表明各函數(shù)至多被嵌套調(diào)用兩次。標號Cid 從0 開始，表示對對應(yīng)函數(shù)的第Cid+1 次嵌套調(diào)用。DAO.withdrawAll()最初只能由外部觸發(fā)，故它的第一次調(diào)用為自動機initCaller發(fā)送調(diào)用信號callW[0]發(fā)起。

不失一般性地，假設(shè)有兩個對象參與合約調(diào)用，他們已各自存入100 以太幣，當前他們在合約DAO 中的賬戶余額都是100；合約的余額是200，即balance=200。假設(shè)由0 號參與對象啟動DAO.withdrawAll()操作，對credit[0]和balance 的值進行修改。

在這個模型上，很直觀地，上述關(guān)于“保證balance 的值為所有對象的余額總和”這一不變式可用CTL 公式描述為：

其中q=(balance==sum(i:int[0,oNum-1]) credit[i])，是一命題邏輯公式。

直觀地說，模型所表示的程序的所有可能執(zhí)行路徑形成一棵樹。CTL 公式A＜＞q 表示這棵樹的每一條路徑上，都存在至少一個節(jié)點滿足命題邏輯公式q。公式(1)即是余額一致性的時序邏輯公式描述。其含義是： 無論參與對象的行為如何，q在每個狀態(tài)下滿足。至此，完成了圖1 所示的DAO 合約以及性質(zhì)“余額一致性”的建模。

4 重入漏洞的形式分析

如果DAO 合約在兩次嵌套調(diào)用(一次回調(diào))時不滿足余額一致性性質(zhì)，那么就可以判斷其存在重入漏洞[16]。因此，將模型中Cid 的取值范圍設(shè)為{0，1}，即DAO.withdrawAll()只被回調(diào)一次。

在UPPAAL 中，在模型上驗證某一性質(zhì)，將得到“滿足該性質(zhì)”或“不滿足該性質(zhì)”的結(jié)果。對于不滿足的性質(zhì)，工具還可生成反例。

可從驗證結(jié)果得到這樣一些信息：

如果性質(zhì)滿足，只要參與對象模型涵蓋了所有可能的使用行為，可以得出該合約不存在可重入漏洞的結(jié)論。

反之，如果模型不滿足該性質(zhì)，說明至少存在一條路徑，其上有狀態(tài)不滿足余額一致性。這樣就存在攻擊路徑，攻擊者可利用它來實現(xiàn)重入攻擊。UPPAAL 可以返回一條攻擊路徑來幫助開發(fā)者查錯。為了得到一條完整的路徑，本文用公式(2)來驗證。

圖5 參與對象回調(diào)DAO 時的消息序列圖及狀態(tài)變化

公式(2)表示，在所有執(zhí)行路徑上，當整個執(zhí)行結(jié)束時，q 滿足。當整個執(zhí)行回到initCaller 的e2 邊時，closed 被置為真。顯然，若公式(2)不成立，公式(1)也不成立。

在UPPAAL 中，在上述DAO 模型及其調(diào)用模型上驗證公式(2)，將被告知“不滿足該性質(zhì)”，并生成反例。反例的消息序列圖及狀態(tài)變化如圖5 所示(沒有變化的狀態(tài)省略)。這個序列圖很好地展示了當參與對象包含回調(diào)時模型的行為。通過狀態(tài)變化，可以看到余額一致性性質(zhì)是如何被破壞的。圖中的5 條線程分別對應(yīng)交易發(fā)起者(initCaller)，對DAO.withdrawAll()的兩次嵌套調(diào)用(DAO_w(0)和DAO_w(1))，對pay()的兩次嵌套調(diào)用(Client_p(0)和Client_p(1))；最右列是幾個變量值的變化情況，無變化的情況省略。可以看到，在初始狀態(tài)S0，余額是一致的；在狀態(tài)S1，合約的余額已被扣減，但用戶余額不變(credit[0]=100)；由于該用戶尚有余額(credit[0]＞0)，在pay()回調(diào)的DAO.withdrawAll()(第二次調(diào)用，對應(yīng)于DAO_w(1))執(zhí)行時，合約余額再次被扣減(S3)；直到對pay() 的第二調(diào)用(Client_p(1))執(zhí)行返回后，credit[0]才被清零(狀態(tài)S3)。這個狀態(tài)一直保持到結(jié)束(S4)?？梢灾庇^地看出，在這執(zhí)行過程中除了初始狀態(tài)，其他狀態(tài)都不滿足q，因而驗證模型不滿足公式(2)從而不滿足公式(1)。因此，可以斷言，當參與對象的pay()有回調(diào)行為時，DAO 合約是可重入的，它的狀態(tài)會被意外修改。

在這一模型中只允許設(shè)置兩層嵌套(即回調(diào)一次DAO.withdrawAll())，在實際的DAO 攻擊事件中，回調(diào)次數(shù)(即balance 被扣減，而credit[0]不變)取決于什么時候balance 被取完或攻擊者的gas 耗盡。

合約DAO 的重入漏洞的隱密性在于，如果函數(shù)pay()中不回調(diào)DAO.withdrawAll()，在執(zhí)行結(jié)束時，余額一致性是能夠保持的。圖6 所示的消息序列圖對應(yīng)的即是圖2 中的goodClient 的行為。當closed 為真時q 為真(S7)，故而整個行為滿足公式(2)。但公式(2)成立并不能推出公式(1)成立。

圖6 參與對象無回調(diào)時的消息序列圖及狀態(tài)變化

重入漏洞看似由回調(diào)引起，但實際上回調(diào)并不是根本原因。例如，修改一下DAO 合約，將圖1 中DAO.withdrawAll()的第5 行代碼放至第2.5 行處，這時相應(yīng)的模型也要修改：將圖4(a) 所示自動機DAO_w 的邊e5 上的更新操作credit[0]移至e3,緊接著對balance 的更新，形成新的模型DAOfixed。這時，無論Client_p 走哪條路徑，公式(1)都成立。圖7展示的是修改后的模型在pay()中包含回調(diào)的情況下的執(zhí)行序列?？梢钥吹剑珼AO.withdrawAll()的第二次執(zhí)行(DAOfixed(1)) 過程中并不再次調(diào)用pay()(Client_p(1))。實際上，在這個模型中，無論將嵌套調(diào)用次數(shù)(callNum)設(shè)為多大，pay()只為被執(zhí)行一次，DAO.withdrawAll()只會被執(zhí)行兩次。例如，圖8所示的是當callNum=4 的情況。

圖7 參與對象回調(diào)DAOfixed 時的消息序列圖及狀態(tài)變化

5 結(jié)論

在The DAO 事件中，造成重大損失的根源在于合約中存在重入漏洞。本文通過形式化分析來更清晰地展示該漏洞特點及攻擊行為，并以此為例介紹基于模型檢測技術(shù)的智能合約形式化驗證方法。

圖8 嵌套調(diào)用次數(shù)設(shè)為4 時，參與對象回調(diào)DAOfixed 時的消息序列圖