The DAO 事件的形式化分析

朱 雪 陽

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

0 引言

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

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

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

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

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

1 DAO 合約及重入漏洞

本質上，一個智能合約文本描述了一個類，部署上鏈后，相當于生成一個該類的實例對象；鏈上的合約對象之間、外部地址與合約之間通過消息傳遞通信。因此，智能合約的設計及行為方式本質上遵從面向對象范式。為突出所要分析的問題，參照文獻[16]的方法，將The DAO 合約中與重入漏洞相關的代碼提取表示為如圖1 所示的DAO 對象。

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

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

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

圖2 合約DAO 的可能調用對象[16]

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

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

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

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

模型檢測工具應用算法自動驗證并發系統抽象模型是否滿足給定性質，對不滿足性質的模型能生成反例。比較著名的模型檢測工具有SPIN[22]、NuSMV[23]和UPPAAL[24]等。基于模型檢測的漏洞分析如圖3 所示。

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

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

3 重入漏洞的形式模型

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

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

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

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

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

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

圖4 合約DAO 及其調用模型

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

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

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

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

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

4 重入漏洞的形式分析

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

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

可從驗證結果得到這樣一些信息：

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

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

圖5 參與對象回調DAO 時的消息序列圖及狀態變化

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

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

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

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

圖6 參與對象無回調時的消息序列圖及狀態變化

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

圖7 參與對象回調DAOfixed 時的消息序列圖及狀態變化

5 結論

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

圖8 嵌套調用次數設為4 時，參與對象回調DAOfixed 時的消息序列圖