securify：智能合約的實證安全分析

10.1引用：

Tsankov P , Dan A , Cohen D D , et al. Securify: Practical Security Analysis of Smart Contracts[J]. 2018.

10.2摘要：

無許可區塊鏈允許執行任意程序(稱為智能合約)，允許相互不可信的實體在不依賴可信第三方的情況下進行交互。儘管存在這樣的潛力，但不斷出現的安全擔憂已經動搖了人們對通過智能合同處理數十億美元資產的信心。

為了解決這個問題，我們提出了SECURIFY，這是一個為以太坊智能合約提供的安全分析程序，它是可伸縮的、完全自動化的，並且能夠證明對於給定的屬性，合約行為是安全的/不安全的。SECURIFY的分析包括兩個步驟。首先，它象徵性地分析合約的依賴關係圖，以從代碼中提取精確的語義信息。然後，它檢查遵從性和違反模式，這些模式捕獲了足夠的條件來證明屬性是否具有。為了支持可擴展性，所有模式都是用指定的領域特定語言指定的

區塊鏈平臺，如中本聰的比特幣，使相互不信任的各方能夠進行加密貨幣的交易。為了消除對信任的需求，他設計了一個對等網絡，使其同行能夠就交易達成一致。之後，由於分散計算在交易之外的適用性， Ethereum區塊鏈被設計出來，它支持用圖靈完備語言編寫的程序(稱為智能合約)的執行。

越來越多地採用智能合同需要強有力的安全保障。不幸的是，創建沒有安全漏洞的智能合約非常具有挑戰性。因此，智能契約中的關鍵漏洞每隔幾個月就會被發現和利用。

為智能合約創建一個有效的安全分析器的主要挑戰是編程語言的圖靈完整性，它使得對任意屬性的自動驗證不可判定。為了解決這個問題，目前的自動化解決方案往往依賴於相當通用的測試和符號執行方法。這些方法有幾個缺點:(i)他們可以錯過關鍵違規(ii),也可以產生假陽性和(iii)他們能不能達到足夠的代碼覆蓋現實合約。總的來說，這些缺陷給用戶帶來了很大的負擔，他們必須檢查所有報告是否有錯誤警報，並擔心未報告的漏洞。實際上，智能契約的許多安全屬性本來就很難直接推理。解決這些挑戰的可行途徑是構建一個針對重要領域特定屬性的自動驗證器。

對這項工作的一個關鍵觀察是，通常可以設計出在合約的數據流圖上表示的精確模式，其中模式的匹配意味著違反或滿足原始安全屬性。例如，在Ethereum智能合約中的所有調用中，有90.9%可以通過匹配一個模式來證明沒有臭名昭著的DAO bug，該模式聲明調用之後沒有寫入存儲。之所以能夠建立這樣的對應關係，是因為在實際契約中，對原始屬性的違反往往會違反一個簡單得多的屬性。實際上，就驗證而言，使用模式而不是使用它們相應的屬性的一個關鍵好處是，模式實際上更適合自動推理。

基於以上認識，我們開發了SECURIFY，一個輕量級的、可伸縮的以太坊智能合約安全驗證器。關鍵的技術思想是定義兩種模式來反映給定的安全屬性:(i)遵從模式，這意味著屬性的滿足;(ii)違反模式，這意味著屬性的否定。

與現有的智能合同符號分析儀相比，SECURIFY減少了兩種方式檢查報告所需的努力。首先，現有的分析程序沒有報告明確的違規，因此要求用戶手動將所有報告的漏洞分類為真陽性或假陽性。相比之下，SECURIFY會自動對被擔保為違規的行為進行分類。因此，用戶只需要手動將警告分類為真或假陽。

10.2.2SECURIFY系統介紹

SECURIFY的輸入是合約的EVM字節碼和一組安全模式，在我們指定的領域特定語言中指定。SECURIFY也可以作為以可靠形式編寫的輸入契約，這些契約在進行分析之前被編譯為EVM字節碼。有兩種安全模式:遵從性模式和違反模式，它們捕獲足夠的條件來確保合約滿足給定的安全屬性，並分別違反給定的安全屬性。

要發現合約中不受限制的條款，SECURIFY主要有以下三個步驟

第一步:反編譯EVM字節碼。SECURIFY首先將作為輸入提供的EVM字節碼轉換為靜態單分配表單中的無堆棧表示形式。

第二步:推斷語義事實。反編譯之後，SECURIFY分析契約，以推斷語義事實，包括數據和控制流依賴關係，它們控制契約的所有行為。

語義事實的SECURIFY派生在分層數據中聲明性地指定，並使用現有的可伸縮引擎實現完全自動化。聲明式方法的主要優點是:(i)推理規則簡明地捕獲關於不同組件的抽象推理;(ii)可以輕鬆添加更多的事實和推理規則;(iii)推理規則以模塊化的方式指定。

第三步:檢查安全模式。在獲得語義事實之後，SECURIFY檢查作為輸入的遵從性和違反安全性模式集。這些模式是用特定於領域的專用語言(DSL)編寫的，這使安全專家能夠使用定製的模式擴展我們的內置模式集。我們的DSL是通過SECURIFY推斷出的語義事實的邏輯公式片段。

我們注意到，在進行安全審計時，安全專家有時會添加特定於合約的模式。例如,它經常需要檢查沒有不良的依賴關係,如:只有主人可以修改某些值的存儲,或確保特定算術表達式的結果不依賴於部門指令。

對於任何違反模式的匹配，SECURIFY輸出導致該模式匹配的指令。它突出顯示了指令sstore(c, b)。此外，對於違反或合規模式都不匹配的任何財產，證券化都會輸出警告，表明它未能證明或反駁該財產。

我們簡要總結了SECURIFY的幾個侷限性。首先，當前版本的SECURIFY無法對溢出等數值屬性進行推理。為了解決這一侷限性，我們計劃將SECURIFY擴展到數值分析，這不僅可以提高SECURIFY的精度，而且可以檢查數值屬性。

其次，SECURIFY不考慮可達性，而是假設合同中的所有指令都是可達的。這一假設對於在SECURIFY所支持的證券屬性與用來證明和反駁它們的模式之間建立正式的對應關係是必要的。

最後，我們認為捕獲違規的屬性常常會被攻擊者利用，但並不總是如此。例如，契約中的某些字段必須是所有用戶都可以通用編寫的。為了解決這個問題，安全專家可以在SECURIFY的DSL中編寫特定於契約的模式。

10.3語義事實

在本節中，我們將介紹SECURIFY所使用的控制和數據流依賴關係的自動推理。在此過程中推斷的事實稱為語義事實，稍後將用於檢查安全性屬性。我們從理解這個分析所必需的背景開始:EVM指令集和分層數據。然後，我們將介紹SECURIFY派生的語義事實，以及分層數據中指定的用於派生這些事實的聲明推理規則。

10.3.1背景

Ethereum虛擬機(EVM)。智能合約是在區塊鏈上執行的。當用戶提交指定合約、要運行的方法和方法參數的事務時，將執行合約。當事務被處理時，它被添加到區塊鏈的新塊中。合約可以訪問易失性內存和非易失性存儲。EVM指令集支持幾十個操作碼。SECURIFY處理所有EVM操作碼。

分層數據日誌。分層數據日誌是一種聲明性邏輯語言，它支持編寫事實和規則來推斷事實。接下來，我們將簡要概述它的語法和語義。

語法。我們在圖10-1中給出了Datalog s語法。Datalog程序由一個或多個規則組成，用r表示。規則r由頭部A和體l組成，體l由文字組成，中間用逗號分隔。頭部，也稱為原子，是零個或多個術語上的謂詞，表示為t，逗號分隔。字面量l是一個謂詞或它的否定。按照慣例，我們用大寫字母寫Datalog變量，用小寫字母寫常量。

圖10-1

語義。設

(其中t是由逗號分隔的術語列表)表示所有ground原子;我們把這些稱為事實。解釋是一組事實。完全格

對的解釋集部分排序。

給定一個替換變量映射到常數,一個原子,我們寫σ(a)獲得的事實根據σ替換的變量。例如,σ(p (X))返回的p(σ(X))。給定一個程序P，其結果運算符定義為

10.3.2事實與推理規則

SECURIFY首先提取一組適用於每條指令的基本事實。這些基本事實構成一個Datalog輸入，該輸入被輸入到Datalog程序中，以推斷關於合同的其他事實。我們使用術語語義事實來引用Datalog程序派生的事實。出現在契約中的所有程序元素，包括指令標籤、變量、字段、字符串和整數常量，都表示為Datalog程序中的常量。

基本事實。我們推理機的基本事實描述了合同控制流程圖(CFG)中的指令。基本事實以，其中instr是指令名，L是指令s標籤，Y是存儲指令結果的變量(如果有的話)，是作為參數給指令的變量。

連續指令的基本事實由在稱為Follow的標籤上定義的謂詞表示。對於每兩個標籤，L1和L2，它們的指令在CFG中是連續的(要麼在相同的基本塊中，要麼在鏈接的基本塊中)，我們都有基本事實Follow(L1, L2)。

Flow-Dependency謂詞。我們考慮的流謂詞是MayFollow和MustFollow，它們都是在一對標籤上定義的，並從合約CFG中推斷。

為了推斷MayFollow和MustFollow謂詞，我們使用Follow(L1, L2)輸入事實，如果CFG中L2緊跟L1，則該事實成立。也就是說，謂詞MayFollow是由以下兩個Datalog規則定義的：

第一條規則解釋為:如果Follow(L1, L2)成立(即:，它包含在Datalog輸入中)，然後導出謂詞MayFollow(L1, L2)(即，它被添加到定點)。第二個規則被解釋為:如果MayFollow(L1, L3)和Follow(L3, L2)都成立，那麼就派生出MayFollow(L1, L2)。注意，如果在定點計算中(定點計算結束時)沒有派生出MayFollow(L1, L2)，那麼在執行任何合約時，標記L2處的指令不會出現在標記L1處的指令之後。

10.4安全模式

在本節中，我們將展示如何在語義事實之上表達安全模式。我們首先定義表示安全模式的SECURIFY語言。然後，為了形式化地定義安全屬性，我們提供了EVM契約執行語義的背景知識，並形式化地定義了屬性。我們繼續展示一組相關的安全屬性，對於每一個屬性，我們都顯示遵從性和違反模式，它們分別表示屬性及其否定性。這種構造使我們能夠確定合同是否符合或違反給定的安全屬性。最後，我們將展示SECURIFY如何利用一些模式來進行錯誤定位。

10.4.1語言安全

我們首先定義用於編寫模式的語言的語法，然後定義如何根據給定契約派生的語義事實解釋模式。

語法。SECURIFY語言的語法由以下BNF給出：

語義。模式是通過檢查推斷的語義事實來解釋的：

量詞和連接器按通常的方法被解釋。流和數據依賴謂詞的解釋當且僅當它包含在Datalog定點中時，語義事實才成立。

10.4.2EVM背景和屬性

EVM語義。契約是EVM指令序列。契約的語義是初始狀態的所有跟蹤的集合。跟蹤合同的C是一系列state-instruction 。從一個初始狀態σ0,這樣的關係是根據EVM有效的執行語義。

屬性。屬性是一組跟蹤上的關係。合同滿足安全屬性我們說C違反房地產ρ。我們使用一階邏輯公式定義關係。公式通過由用戶標識符、偏移量和EVM指令的其他參數或返回值組成的跟蹤和位串來解釋。我們用t1 t2…引用跟蹤的變量。我們用i1 i2…引用跟蹤中一對的索引的變量。我們對位串變量使用其他字母。

10.4.3安全屬性和模式

Ether動性(LQ)。我們定義此安全性屬性通過要求(i)所有跟蹤t不改變契約的餘額，或者(ii)存在一個減少契約餘額的跟蹤t。

調用後無寫操作（NW）。首先，調用指令在執行時使調用的接收者能夠在返回到契約之前執行自己的代碼。其次，此調用傳輸的數量取決於存儲值，存儲值在此調用之後更新。這個值非常重要，因為它記錄了調用方在合同中擁有的ether的數量，因此可以請求接收ether。

受限制的寫操作（RW）。攻擊者利用了契約對庫的依賴，庫可以無條件地將所有者字段設置為任何地址。這使得攻擊者能夠獲得契約的所有權並竊取它的ether。

受限制的發送(RT)。我們定義了一個屬性，它保證ether傳輸(通過調用)不能被任何用戶a調用

異常處理（HE）。我們的遵從性模式檢查調用指令之後是否遵循goto指令，該指令的條件由調用的返回代碼決定

交易順序依賴（TOD）。我們的遵從性模式要求調用指令發送的ether量獨立於存儲狀態和契約餘額。

參數驗證（VA）。我們的遵從性模式檢查在持久性內存中存儲一個可能依賴於方法參數的變量之前，是否存在對參數值的檢查。

10.5主要貢獻

我們提出了SECUIFY，一個新的輕量級和可伸縮的驗證Ethereum智能合同。SECUIFY利用了特定於領域的洞見，即對智能合約的許多實際屬性的違反，也違反了更簡單的屬性，而這些更簡單的屬性以一種完全自動化的方式檢查起來要容易得多。基於這一認識，我們設計了遵從性和違反模式，這些模式可以有效地證明現實世界中的合同是否與相關屬性相關是安全的/不安全的。總的來說，證券化有幾個重要的好處:

(一) 分析所有合同行為，避免不必要的虛假否定;

(二) 確保某些行為是實際錯誤，從而減少用戶將警告分為真報警和假報警的工作量;它支持一種新的特定於領域的語言，使用戶能夠在出現新的漏洞模式時加以表示;最後，它的分析管道——從字節碼反編譯、優化到模式檢查——是完全自動化的，使用可伸縮的現成Datalog解決方案。

本文由南京大學軟件學院2016級本科生徐介輝轉述。