以太坊智能合約安全形式化驗證方法研究進展

王赫彬，鄭長友，黃 松，孫金磊，丁一先

(1.中國人民解放軍陸軍工程大學 指揮控制工程學院，江蘇 南京 210007；2.中國人民解放軍陸軍工程大學 全軍軍事訓練軟件測評中心，江蘇 南京 2100073.遼寧工程技術大學，遼寧 阜新 123000)

0 引 言

自2009年Satoshi Nakamoto的比特幣發布以來，出現了各種各樣的區塊鏈實現。而自從2013年底Vitalik Buterin發布的以太坊白皮書將智能合約的概念引入到區塊鏈之中，區塊鏈技術的應用變得更加廣泛，并使得比特幣等加密貨幣的可編程能力更進一步。智能合約提供了一個框架，允許以可信任、去中心化的方式執行一個應用程序的業務邏輯。智能合約用戶通常攜帶大量的價值數以億計的貨幣，但是智能合約作為一種計算機代碼可能具有未發現的和未知的漏洞，具有很大的安全隱患。2016年6月17日的The DAO攻擊事件中，一名攻擊者利用去中心化自治組織(decentralized autonomous organization，DAO)部署的智能合約代碼中的多個漏洞，控制了當時價值約為5 000萬美元的以太坊網絡，并從合約中盜走了350多萬以太幣；2018年美鏈BEC上百億項目歸零、BAI(blockchain of artificial intelligence and internet of things)任意賬戶無限轉賬都是因為ERC20代幣標準中出現的一系列漏洞，導致資金惡意發送轉移，正常的礦工節點受到了危害。對于難以避免的智能合約安全性問題來說，在部署鏈上前發現并修復漏洞至關重要。

雖然現有的一些工作通過基于測試的檢測方法來檢測漏洞，但不能完備地發現智能合約源碼和字節碼中所有的漏洞，而且對于智能合約在一些概念和屬性的正確表達缺乏全面的檢查。而現有的一些代碼及合約審計工作則依賴于審計專家的個人經驗和主觀判斷，缺乏嚴謹性和說服力。形式化驗證方法則通過證明序列、邏輯語句檢查數學模型的邏輯，以證明某些規范的正確性并發現運行時錯誤，理論上可以發現更多的漏洞。智能合約對于安全性要求高，代碼量相對較小，這些特點很適用于進行小型的形式化驗證。文中對以太坊智能合約的相關概念進行了系統的介紹，分析了智能合約常見的漏洞類型，總結了常見的形式化驗證方法，進行了實驗結果分析并討論了目前形式化驗證工作存在的問題和挑戰，提出了將來的改進方法及意見建議。

1 背景及相關概念介紹

1.1 以太坊智能合約

以太坊平臺于2015年提出，是使用區塊鏈平臺執行智能合約的最流行的底層系統之一[1]。其市場容量達到了1 000億美元，每天處理超過40萬筆資金交易。以太坊包含以太坊虛擬機、執行環境(賬戶管理、默克樹等)和共識算法三個部件，適用于公有鏈、私有鏈和聯盟鏈三種區塊鏈環境。不同的區塊鏈環境可以通過擴展包的形式，將以太坊智能合約部署到鏈上。以太坊智能合約是部署在其平臺上的一種計算機協議，具有可編程、可維護和安全可信等特點[2]。特別地，智能合約的執行過程是從一個狀態到另一個狀態[3]，可以用有限狀態機將智能合約形式化地表示為一個五元組自動機Q*:

Q*=(Q0,Ω,ζ,t*,G*)

其中，Q0是合約執行自動機的所有狀態的集合，Ω為所有輸入事件的集合，ζ:Q0×Ω→Q0則是轉移函數的集合，t*∈Q0為初始狀態,G*?Q0為終止狀態集合。

1.1.1 以太坊虛擬機

智能合約通常用有別于現有編程語言的高級語言編寫，開發人員在編寫完智能合約代碼后，代碼被編譯成以太坊虛擬(Ethereum virtual machine，EVM)字節碼在計算機上執行。EVM是一種完全基于堆棧的虛擬機架構，支持一個包含134個操作碼的指令集，運行在256比特的基本數據類型之上。與Java虛擬機(Java virtual machine，JVM)相比，EVM相對更加簡單，執行效果更加具有確定性。圖1是一個合約代碼被EVM編譯成字節碼的示例。

圖1 智能合約代碼編譯過程示例

1.1.2 智能合約語言

智能合約通常使用專門的智能合約語言進行編寫[4]。智能合約語言包含高級語言、中間級語言(intermediate representation，IR)和低級語言三種類型。開發人員通常使用高級語言編寫智能合約，因為高級語言能夠提供期望的表達方式。IR語言介于高級語言和低級語言之間，可以用于編寫程序以推導屬性和檢查規范，也可以用于優化代碼的結構。而低級語言則提供了一種在分布式虛擬機上執行的實現方式。基于合約語言不同的安全特性，可以采用不同的方法對合約進行形式化驗證。其中Solidity、Vyper是以太坊平臺常用的智能合約高級語言，EVM是其常用的低級語言，而EthIR和Yul是其常用的中間語言。

1.2 常用的形式化驗證方法

形式化驗證方法[5]是指在形式化建模的基礎上，對具有精確語法和語義的形式化語言的系統建立事務及性質等的關系，從而驗證系統所應具有的功能正確性和其他關鍵性質。

1.2.1 定理證明

定理證明[6]適用于很多系統，方法流程是對其進行形式化規約，并將要證明的命題寫為“待驗證系統滿足形式化規約”，從而將驗證問題轉化為證明一個可滿足性問題，使用預先定義的公理和推理規則作為輸入來完成證明過程。定理證明分為交互式定理證明、自動化定理證明和混合定理證明三種[7]，而不同類型系統的復雜度決定了不同定理證明方式的可行性。復雜度較小的可以使用自動化定理證明，復雜度較大的則可以使用交互式定理證明。

1.2.2 模型檢測

模型檢測[8]是指對于一個協議框架利用邏輯公式進行檢查，觀察該協議描述的需求或系統是否具有某些期望的性質。通常需要驗證的性質包括安全性(safety)、活躍性(liveness)、無阻性(non-blocking)和非嚴格順序性(no strict sequencing)等。該方法適用于可以用有限狀態模型表示的系統。模型檢測器可以自動化完成精準模型和規范的檢測，給出可用的判斷結果。

1.3 常見的漏洞類型

隨著智能合約語言的迭代更新，不斷有新的漏洞被修復，但同時新的版本語言的語法也會帶來新的安全漏洞隱患。截至2020年8月，Solidity語言從0.3.x版本更新到了0.7.0版本。按照漏洞來源依賴，以太坊智能合約漏洞可以分為區塊鏈依賴漏洞、軟件安全依賴漏洞和以太坊及合約語言依賴漏洞[9]。圖2是一些以太坊智能合約的常見漏洞。

2 相關研究進展

本節將介紹智能合約形式化驗證的一些最新技術研究進展。暫時沒有一個固定的標準對于這些形式化驗證方法進行分類，但是已經有很多研究對于智能合約的正確設計和漏洞挖掘產生了效果。借鑒了1.2節傳統的形式化驗證方法，可以采用以下幾種技術手段對智能合約進行形式化驗證。

2.1 類型推斷

基于類型推斷的形式化驗證使用數十行或數百行的核心類型理論來替換智能合約語言的類型或類型子集，能夠用來快速證明數學定理。這種方法使用函數式程序語言，更多地關注類型檢查，而不是運行程序，具有相對簡單的語法。這種方法的一般流程為：首先將智能合約高級語言翻譯成函數式程序語言，指定源語言中的數據在驗證語言中的數據格式和數據類型，并轉換包含這些數據的源語言中的函數；然后提出并證明關于這些函數的定理，可以完成運行時程序正確性的驗證。

微軟研究院和哈佛大學研究團隊的Bhargavan等人[10]提出了一個用于形式化分析的F*框架，試圖通過將合約代碼翻譯成F*語言后，通過類型推斷來驗證智能合約。該框架包括Solidity*和EVM*兩個工具原型，Solidity*支持Solidity的部分語法類型轉換，將智能合約從Solidity語言翻譯成F*語言，EVM*再從EVM字節碼形式反編譯成F*語言。轉換過程中支持遞歸，不支持循環。Solidity*運用類型推導發現運行時函數和變元的錯誤和違反的規范，EVM*則可以分析低層次的屬性，估算gas消耗的上界。驗證了396份合約，其中46份成功地進行了翻譯和類型檢查，發現了一些可重入漏洞和未經檢查的send語句返回調用問題。

Coblenz等人[11]研發的Obsidian是一種面向類型的安全區塊鏈編程語言，該語言以用戶為中心，用戶實驗反饋與語言開發同時進行，類型狀態依賴系統保證了程序員編寫正確的合約。針對可用操作依賴的高級狀態、代碼錯誤導致的資金損失或挪用和不一致狀態導致的重入攻擊等三種嚴重的bug源，類型狀態會將動態信息記錄到類型之中，之后進行靜態的類型推斷，同時，線性類型系統計算貨幣的數量，完成對于交易過程中的財務信息追蹤溯源。

Schrans等人[12]開發了一種專門用于編寫魯棒性智能合約的靜態類型編程語言Flint，引入保護塊(protection blocks)根據類型狀態限制運行代碼的時間和用戶，對于狀態的寫入進行了限制，簡化了合約的推理。具有調用保護、默認不變量、資產類型推理和安全語義等安全特性，實現了安全的內部及外部資金轉移(asset transfer)、事件監控和安全的算術運算等代碼保護功能，通過限制交易過程中的類型狀態，將Solidity語言的安全性進行了提升，避免了智能合約重入漏洞和整數溢出等問題的出現。目前，智能合約交互語言Rholang[13]和Plutus[14]分別使用ρ演算和λ演算等抽象演算方法，完成了一些驗證工作。

2.2 交互式定理證明

智能合約的交互式定理證明是傳統的定理證明方法在智能合約驗證中的應用。智能合約高級語言如Solidity和低級語言如EVM上的字節碼需要被定義成可以為定理證明器編譯的語言，然后再利用交互式定理證明驗證以太坊智能合約的安全性質。定理證明器也可以選擇用一些自動化SMT定理證明器，SMT求解器使用一階邏輯語言來表示命題，然后通過枚舉賦值的方式進行證明。可滿足命題的賦值為程序提供正確的輸入，可以證明在執行路徑中給定的狀態是可達的。

Amani等[15]研發的eth-isabelle是一種作用于EVM字節碼的Isabelle/HOL定理證明器。首先將EVM字節碼序列語義用Lem語言形式化構造成線性代碼塊，將EVM指令劃分為以JUMPDEST為開始的基本塊、JUMP、JUMPI等跳轉指令以及其他指令基本塊三種，然后再翻譯到Isabelle/HOL或Coq中進行定理證明。基于以太坊的gas機制給出了一種out-of-gas異常處理方法，使用分離邏輯(separation logic)驗證以太坊虛擬內存中的字節碼程序，支持使用程序規則、基本塊規則和指令規則自動生成驗證條件和驗證規范，降低了EVM操作碼形式智能合約形式化驗證的時間復雜度。

Lei等[16]提出的Lolisa是Solidity語言的一個大型子集的形式化語法和語義，采用了更魯棒的靜態類型系統，不僅包含了Solidity中映射符、修改器、合約類型和地址類型等語法組件，而且還包含了諸如多個返回值、指針算法以及結構和字段訪問等通用編程語言特性。基于Solidity語言的可擴展性，提出將Lolisa擴展到其他合約編程語言的方案。接著開發了一種支持不同驗證范式的可擴展、可重用的形式化內存框架GREM，模擬了物理內存的硬件結構，并且使用Coq提供了一套防干擾的應用程序編程接口(application programming interfaces，API)，實現了一個獨立可定制的框架。之后開發的執行時驗證同構體(execution verification isomorphism，EVI)將符號執行與定理證明結合，提高了高階邏輯定理證明輔助工具的自動化程度，并且證明了Lolisa可滿足于EVI。

Yang等人[17]開發的FEther編譯器是一種基于Coq的混合定理證明工具，基于Solidity語言的形式化語法和語義子集Lolisa，結合符號執行和高階邏輯定理證明，提高了執行和驗證合約的自動化程度，同時FEther具有很好的可重用性，可以將驗證過的代碼片段復用檢查其他代碼段的屬性，其運行效率遠遠超過Coq標準教程中的解釋器。是第一個在Coq中對于Solidity語言進行語法和語義定義的證明引擎。Annenkov等人[18]提出了一個基于Coq的框架ConCert，可以對于智能合約進行形式化證明鑒定。

Sergey等[19]研發的中間語言Scilla提供了一個編程組件，為智能合約間的通信提供了一個計算與交互的分離、效率和純計算的分離及調用動作和連續過程的分離等，允許豐富的交互模式，具有規則形式寫成的語義，將Scilla嵌入Coq之中，易于進行形式化驗證。描述了基于自動機[20]的Scilla模型，展示了自動機關于安全和時間等屬性的簡化驗證過程。除了Coq和Isabelle/HOL等工具外，Why3[21]也實現了EVM的語義表示，可以基于EVM字節碼進行一些智能合約的定理證明。

2.3 有界模型檢測

智能合約的模型檢測中常用的方法為有界模型檢測(bounded model check，BMC)，有界模型檢查器系統地、象征性地研究系統的行為，直到某個邊界k，尋找對給定屬性的違反，其中邊界k表示允許從某個初始狀態進行的轉換的數量。使用單個邏輯語句檢查智能合約的性質及規范，若合約狀態轉移符合規范，則證明智能合約滿足所驗證的安全特性；否則構造模型檢測器會構造一個狀態轉移的反例，證明合約違反了該條規范，存在安全性問題。

牛津大學的Antonino等[22]開發了一種基于Solid語言的有界模型檢測工具Solidifier，Solid語言對于Solidity語言和以太坊區塊鏈進行形式化描述，之后將Solid轉換成中間語言Boogie[23]，使用Corral[24]對于Boogie語言形式的合約進行有界模型檢測。提出合約驗證和函數驗證兩種工具，定義main過程和捕獲Solid調用結構的callP過程，探索區塊鏈的行為，尋找合約錯誤。通過特定代碼模式匹配或未預料到的行為方式，查找不符合開發人員意圖的程序錯誤及狀態。

Joel等[26]開發了一種基于符號執行的有界模型檢測工具ETHBMC，設定了Keccak256函數、Memcopy-like指令和Inter-Contract交互等測試斷言，建立了以太坊的攻擊模型、內存模型和數據調用模型等，然后符號執行檢測模塊中的漏洞，對于每個具有易受攻擊的路徑生成交易過程實例。通過對于當前go-ethereum區塊鏈工具套件中活躍的大約220萬個用戶大規模分析，自動生成5 905個觸發漏洞的有效輸入，與之前的分析方法相比較，具有22.8%的更多輸入。

Zhang等[27]開發了一個用4 800多行Python和C++寫成的有界模型檢測工具NPCHECKER，處理Solidity及Vyper語言的不確定性對于合約付款等交易過程的影響。發現由于不可預測的事務調度和外部未知的被調用者行為而讀寫更改的合約全局變量，公開了各種不確定性因素和問題。NPCHECKER的工作流程為：首先將EVM字節碼反編譯，然后利用內聯匯編將匯編指令轉換成LLVM，恢復控制流圖，最后使用SMACK[28]和Boogie等模型檢測工具檢查恢復的IR代碼中是否含有NPⅠ和NPⅡ兩種付款bug。在以太坊主網上收集到3萬多份在線合約并對其進行了評估。NPCHECKER在1 111份合約中檢測到不確定性支付，識別了六種未知的新漏洞類型。目前，NuSMV[29]、SPIN[30]等傳統的模型檢測工具被用于能源交易市場、網上購物等智能合約，完成需求規范開發階段和最終系統驗證集成階段的交互驗證。

2.4 其他驗證方法

除了以上研究深入廣泛的以太坊智能合約形式化驗證方法外，根據以太坊智能合約框架的性質用途和工作流程，還有很多結合緊密的驗證方法產生更加具有領域自適應性的應用。本節介紹幾種在主流的智能合約形式化驗證之上有所改進的方法。

2.4.1 用戶和區塊鏈行為建模

傳統的模型檢測方法可以對智能合約及其用戶進行建模，但是不能對底層的區塊鏈進行建模。Abdellatif等[31]提出了一種對于區塊鏈及其用戶進行建模的方法，按照行為交互優先級(behavior interaction priorities，BIP)使用統計型模型檢測器(statistical model checking，SMC)進行驗證。對于給定的系統B和性質δ，SMC模型檢測器使用概率有界線性時序邏輯(probabilistic bounded linear time logic，PB-LTL)來判斷B是否滿足δ。令B滿足δ記為B|=δ，首先判斷公式：

P({B|=δ})>θ

是否成立，其中P(.)為某個事件發生的概率，θ為某個選定的閾值；然后估算P({B|=δ})的值p，使得估計值p0滿足：

P(|p-p0|≤α)≥1-β

其中，α為估計精度，β為攻擊風險水平。運用該方法能夠發現傳統模型檢測方法難以發現的易受攻擊用戶行為和交易路徑。

2.4.2 博弈論

Giancarlo等[32]提出了一種利用博弈論(game theory)來對涉及物理行為的智能合約進行驗證的方法。首先通過博弈論分析交易過程中顧客和商家的行為，觀察兩方行為的相互影響，然后使用概率模型檢測器PRISM通過分析顧客和商家不確定的選擇行為對于選擇事件對應的概率的影響，將行為建模成離散時間馬爾可夫決策過程(discrete time Markov decision process，DTMDP)，來解決不確定性問題。根據顧客的誠實度和商家的信譽使用了六種存款與出售價格比率，對于一組誠實的顧客與不誠實的商家，商家損失30%的可能性不大于2%，顧客損失30%的可能性卻可以達到50%。

2.4.3 著色Petri網

Wang等[33]改進了字節碼的程序邏輯規則，應用霍爾條件(Hoare condition)建立了著色Petri網(colored Petri Nets，CPN)模型。首先，對于Solidity源代碼形式的智能合約，利用ANTLR語法分析器建立抽象語法樹(abstract syntax tree，AST)模型并解析抽象語法樹中的元素，生成等價的CPN模型；然后，對于EVM字節碼形式的智能合約，對于字節碼序列對應的操作語義進行靜態分析，劃分出具有不同特征的基本塊，構建控制流圖(control flow graph，CFG)，生成等價的CPN模型。最后，將之前建立的CPN模型放入CPN工具中完成動態仿真和模型檢測。該方法設計了一種自動化的建模方法，引入了一個自定義調用庫和一種基于回溯的路徑推導算法，提高了傳統模型檢測方法的針對性和有效性。

2.4.4 K框架

K框架[34]是一種可執行的程序框架語義集，可以用于形式化智能合約，對事務進行狀態和網絡演化進行建模，并使用轉換規則來詳細闡述狀態的修改和網絡的演化。K框架在邏輯上可以分成三個模塊:data.k,language.k和ethereum.k，目的是與以太坊的依賴結構保持一致。Hildenbrandt等[35]在K框架中定義了一個EVM的語義—KEVM，將EVM表示成K框架范式中的ENBF樣式提供的語言語法、狀態配置描述和驅動程序執行的轉換規則三個主要組件，深入解釋了KEVM的結構定義描述，然后給出了幾種語義擴展，根據ERC20標準驗證了標準代幣的兩種不同語言實現，使用K框架的可達性邏輯證明器，表現了KEVM語義框架的可用性。此外，該框架還可用于gas消耗分析和解析以太坊白皮書中EVM的語言規范等。KVyper[36]由Vyper到LLL、LLL到EVM兩個翻譯器組成，可用于發現Vyper編譯器中存在的錯誤。KSolidity[37]是K框架中Solidity語義的定義，可用于Solidity語言合約測試。

除此之外，ZEUS[38]和Oyente[39]也使用形式化驗證的方法分別在源碼級和操作碼級進行了自動化的漏洞檢測，并發現了一些以太坊智能合約存在的安全漏洞。

3 總結與展望

3.1 現有研究存在的不足

如第二節所述，智能合約形式化驗證工具發展迅速，但是仍有一些缺陷，主要問題如下：

(1)合約語言不完整。不同的形式化驗證方法通常能夠驗證合約語言的一個子集，而不能完整地驗證所有智能合約可能出現的問題。總結一些常用形式化驗證方法對于智能合約的處理，如表1所示。

表1 智能合約形式化驗證框架/工具對比分析

可以看出，很多語言只能處理合約語言的一個語義語法子集，如FEther基于Solidity語言的Lolisa子集進行證明，不能對整個Solidity語言進行驗證，查找漏洞的手段較少，發現漏洞的類型不足。有些待驗證的規范可能包含類型特性子集之外的語義語法元素，導致難以驗證智能合約滿足的性質及規范。擴展可驗證的合約語言子集，建立更多的驗證范式，發現更多的漏洞類型是一個需要解決的技術問題。

(2)應用范圍受限。由于智能合約仍是一個較新的領域，因此形式化驗證缺乏一個統計評價標準和最佳實踐，方法應用沒有突破高昂成本、合約規模等技術局限。文中選取了106個Solidity源碼合約樣本結合偷以太幣(Steal Ether)、黑杰克(Hijack)和自毀(Suicidal)三種攻擊行為，對Solidifier和ETHBMC兩種有界模型檢測工具檢查效果進行對比，其編譯通過率和漏報率結果如表2所示。三種工具都存在較多的問題漏報的情況。此外，形式化驗證還只適用于簡化的合約模型，采用的啟發式方法難以擴展到復雜的合約中去。自動化程度不高，且缺乏對于高階業務邏輯范式的證明。

(3)驗證語言安全性未知。在驗證的過程中，通常需要將源代碼形式或字節碼形式的合約翻譯成另一種語言，例如F*方法，但是驗證語言的安全性沒有得到保證，具有很大的安全隱患。翻譯過程的正確性也是未知的，很有可能出現轉換前后的類型有很大差別。因此證明或提高驗證語言的安全性及翻譯過程的正確性是形式化驗證面臨的一些重難點工作。

3.2 未來研究方向和改進思路

針對現有工具存在的問題，提出如下未來改進思路：

(1)擴展形式化驗證方法的應用范圍。由于缺乏測試判定準則(test oracles)，驗證好壞通常難以衡量。所以需要建立標準的測試判定用例集，對于驗證方法的有效性進行定性定量評估。通過建立綜合評價指標體系，找出實踐性好的驗證方法及工具，有助于在此基礎上對智能合約的形式化驗證進行改進和提高。通過與符號執行、污點分析等方法的結合，提高形式化驗證方法的自動化程度，創建可重用的驗證模式庫，減少驗證所需時間，增強合約驗證方法的可用性。

(2)提高形式化驗證方法的驗證效果。針對智能合約形式化驗證過程不直觀的問題，可以通過類型標記、著色Petri網等增強合約驗證的可視化效果，利用逆向工程重新構造合約執行的控制流圖。根據以太坊智能合約具有的一些性質和用途，建立具有嚴謹可靠數學基礎的區塊鏈模型和智能合約機制模型，提高以太坊平臺合約驗證的效果。

4 結束語

以太坊為代表的智能合約平臺的出現擴展了區塊鏈的資金轉移能力，促進了區塊鏈2.0時代的到來。文中梳理了以太坊智能合約常用的語言和常見的漏洞類型，討論了基于類型推斷的形式化驗證、智能合約的交互式定理證明和智能合約的有界模型檢測等主流的智能合約形式化驗證方法，通過對幾種現有形式化驗證工具的實驗結果分析研究發現，并針對現有方法的不足之處，提出了未來研究的改進思路。下一步工作的重點和難點在于根據以太坊智能合約的實現機制、環境狀態和網絡演化等內部性質用途，提出具有自適應性的理論著力提高驗證的準確性，減少時間和空間成本，擴展驗證的適用范圍，進一步提高以太坊智能合約的安全開發部署能力。