這些智能合約漏洞，可能會影響你的帳戶安全！

摘要：區塊鏈聯盟鏈智能合約形式化驗證揭祕，解釋了咱們爲何要對區塊鏈上的智能合約進行形式化驗證，以及形式化驗證的分類和業界針對每種分類所推出的形式化驗證工具，最後做者描述了一下目前形式化驗證的種種方法所面臨的問題及對於這個領域技術發展的展望。

本文分享自華爲雲社區《這些智能合約漏洞，可能會影響你的帳戶安全！》，做者：麥冬爸 。

什麼是形式化驗證？

維基百科對形式化驗證的解釋是這樣的：在計算機硬件（特別是集成電路）和軟件系統的設計過程當中，形式化驗證的含義是根據某個或某些形式化規範或屬性，使用數學的方法證實其正確性或非正確性。傳統上在硬件設計領域比較經常使用。主要緣由就是硬件設計週期長，成本高，一旦生產出來就很難改動了。例如一個 CPU 設計若是已經出芯片了，那麼出了問題就是大事。形式驗證能夠分爲三大類：抽象解釋（AbstractInterpretation）、形式模型檢查（FormalModel Checking，也被稱做特性檢查）和定理證實（TheoryProver）。

區塊鏈智能合約爲何須要形式化驗證？

在區塊鏈系統中能夠編程且自動運行的程序被稱爲智能合約。智能合約最先在以太坊區塊鏈平臺上應用，如 Solidity 就是一種智能合約編程語言，以使傳統應用程序開發人員可以編寫智能合約。初期會 Solidity 語言的全球只有幾百人，後來隨着以太坊與區塊鏈的火熱，參與 Solidity 智能合約的人才開始逐漸增長，可是跟整個 IT 市場的從業人羣比起來，會編寫智能合約的人仍是太少，大量的 IT 從業者要想開發智能合約只能去學習 Solidity。爲了讓更多的 IT 從業者能夠參與智能合約的編寫與業務規則的實現，智能合約平臺在原有 Solidity 的基礎上擴展了對更多主流語言，甚至高級語言的支持，這樣可讓多普通 It 從業人員也有了能夠進行智能合約編寫的可能性，大量熟悉 Java、Go、Php 等技術編程的開發人員均可以參與智能合約的開發。

然而，因爲區塊鏈交易是不可變的，智能合約代碼中的錯誤會產生毀滅性的後果，破壞了對底層區塊鏈技術的信任。例如，臭名昭著的 TheDAO 漏洞致使價值近 6000 萬美圓的以太損失，奇偶校驗錢包漏洞致使價值 1.69 億美圓的以太永遠被鎖定。解決這些事件的惟一補救辦法是硬分叉區塊鏈，並將其中一個分叉恢復到事件發生前的狀態。然而，這種補救辦法自己是毀滅性的，由於它摧毀了區塊鏈的核心價值，如不可變性和分散信任。可是智能合約的編寫目的是爲了行業應用，一旦應用到實際中必須考慮智能合約的安全性，智能合約要達到機器可信，就必須首先排除掉因人爲因素而形成的智能合約破壞情形。智能合約形式化驗證提供了一種能夠證實的安全檢驗機制，經過形式化語言把合約中的概念、判斷、推理轉化成智能合約模型，能夠消除天然語言的歧義性、不通用性，進而採用形式化工具對智能合約建模、分析和驗證，進行一致性測試，最後自動生成驗證過的合約代碼，造成智能合約生產的可信全生命週期。能夠把市場上已經出現的安全風險進行排查與審計，通過審計後的智能合約代碼天然安全性就獲得加強，同時智能合約形式化驗證也是目前對智能合約進行安全保證最可靠的措施。行業應用區塊鏈與智能合約，就須要進行智能合約 的形式化驗證，消除安全隱患。

智能合約形式化驗證方法分類

業界一般對智能合約進行形式化驗證都有一些通用的方法，大致上分爲下面幾種通用的方法，每種方法都有一些工具和框架進行支撐。

1. 定理證實

定理證實是一種利用演繹推理在符號邏輯中提供證實的形式化方法．在這種方法中，證實的每一個步驟都 會引入一個公理或一個前提，並提供一個陳述，使用謂詞邏輯將其進行推導，最終獲得想要驗證的結果．在證實系統知足關鍵指望的過程當中，通常使用定理證實器來作輔助驗證工做，由於這須要將手工證實的過程變成一系列可以在計算機上運行的符號演算，且能夠對正確性進行檢查。

其優點是這個方式是使用數學的方法，經過公理或前提進行推導，保證驗證的嚴謹性。其不足是在作數學驗證前須要將不一樣類型的源代碼轉換爲相關框架的驗證代碼，而目前沒有很好地辦法保證在源代碼與驗證代碼之間的轉換一致性，實現成本高，自動化水平低，正確性也是很難保證的。在區塊鏈智能合約領域通常對於有高隱私性，安全性，功能性，語義一致性等強烈的需求會經過這種法法來保證。

那業界在定理證實仍是實現了不少工具和框架支撐這一能力，基本有下面的一些工具：

Solidity* and EVM*，該框架使用函數式語言 F*分析驗證了 Solidity 智能合約運行時的正確性，F*是一種函數式編程語言，用於形式化驗證程序的正確性。

Corral 是 Boogie 語言的分析工具．默認狀況下，Corral 會進行有界搜索，直到遞歸深度和固定數量到達必定限度爲止，Boogie 是一種中間驗證語言，旨在構建其餘語言的驗證程序的中間層。

Coq 是一個交互式定理證實助手，它提供了一種形式化的語言來編寫數學定義，可執行 算法和定理

Isabelle/HOL 是一個基於高階邏輯的通用交互式定理證實器。

Raziel 是一個編程框架，用於驗證智能合約的多方計算的安全問題，爲智能合約的隱私 性提供保障。

2. 符號執行

符號執行（英語：symbolicexecution）是一種計算機科學領域的程序分析技術，經過採用抽象的符號代替精確值做爲程序輸入變量，得出每一個路徑抽象的輸出結果。 這一技術在硬件、底層程序測試中有必定的應用，可以有效的發現程序中的漏洞。這種方式的優勢是以符號值做爲輸入，藉助相應工具，可獲得具體測試用例，具備很高的代碼覆蓋率。那這種方式本質上屬於測試，不能１００％證實智能合約是沒有問題的，由於基於測試是很難以 100%覆蓋全部的場景，通常在作合約的安全性，功能性驗證會推薦使用這種方式。

基於符號執行的業界的一些比較有名的架構以下：

• SASC，這個工具被用來發現潛在的邏輯風險，它是一種靜態分析的工具，且能夠生成調用關係的拓撲圖。

• MAIAN，這個工具被用來查詢漏洞，被設計成利用符號分析和具體驗證器來跟蹤智能合約中的屬性。

• Securify，這個工具被用來進行安全漏洞分析，它是一個專門針對以太坊智能合約的工具。

• Mythril，這個工具被用來進行代碼安全分析，是一個針對以太坊的智能合約的符號執行的工具。

• Verx 是一個能夠自動驗證以太坊智能合約功能性的驗證器，以太坊相關的問題能夠經過上面三個工具組合使用來提升覆蓋面。

• Oyente，這個工具被用來檢測合約代碼潛在的安全漏洞，是一個基於符號執行技術的測試工具。

3. 模型檢測

模型檢測(modelchecking)，是一種重要的自動驗證和分析技術，由 Clarke 和 Emerson 以及 Quelle 和 Sifakis 提出，主要經過顯式狀態搜索或隱式不動點計算來驗證有窮狀態併發系統的模態/命題性質。其基本思想是檢驗一個結構是否知足一個公式要比證實公式在全部結構下均被知足容易得多，進而面向併發系統創立了在有窮狀態模型上檢驗公式可知足性的驗證新形式，這種方法也被用於驗證智能合約的正確性。

它的優勢是可使用市面上現有的模型檢測工具，而且支持自動化驗證，減小人爲參與。可是其沒法保證所使用的模型檢測工具的完備性與正確性，合約複雜度太高會致使狀態空間爆炸，進而致使沒法完成驗證能力。通常狀況下須要保證合約的安全性，功能性會使用這種方式。

業界也有很多這種類型的工具和架構以下：

• NuSMV，這個工具被用於用於工業設計的驗證，具備極高的可靠性，且被設計成模型檢查的開放架構。它是 SMV 工具的從新實現和擴展，而 SMV 是第一個基於 BDD 的模型檢查器。

• BIP， 這個框架包含一整套支持建模、模型轉換、仿真、驗證和代碼生成的工具集，還支持層次化結構, 被設計成爲一個通用的系統級形式化建模框架。

• Prism，這個工具只針對表現出隨機或機率行爲的系統，被設計成一個機率模型檢查器，對機率行爲進行形式化建模和分析。

• SMC，這個工具被設計成模型檢測器，用於檢查在不一樣公平性假設下併發程序的安全性和活性。

4. 形式化建模

能夠經過準確的數學語句和模型組件去定義不一樣組件的關係，消除系統中存在的二義性，這種設計系統的技術就是形式化建模。基於這種方式的系統的仿真結果是能夠復現的，不會存在偶發性事件。這種方法的優勢就是使用精確的數學語句或模型組件來設計系統，從而保證其仿真結果可被複現。可是此方法大多使用市面上已有的建模框架，其框架的完備性與正確性沒法保證。基於智能合約的隱私性，安全性和功能性可使用這種方法來檢驗。Hydra，就是基於形式化建模的一個框架，該框架鼓勵開發者和用戶誠實地披露智能合約中的錯誤和漏洞，它的設計是基於漏洞賞金的模式和 NNVP 編程。

5. 有限狀態機

有限狀態機是一種用來進行對象行爲建模的工具，其做用主要是描述對象在它的生命週期內所經歷的狀態序列，以及如何響應來自外界的各類事件。智能合約的執行也能夠看做從一個狀態到下一個狀態的變遷。

這個方法的優勢是思惟導向簡單，將智能合約抽象轉換爲狀態機的形式，易於操做，且具備圖形界面。可是狀態定義的好壞，對智能合約的驗證難易程度有很強相關性，合約複雜度太高也會致使狀態空間爆炸。對智能合約的安全性，語義一致性校驗通常會使用這種方式。

業界通常的工具介紹以下：

• Contract Larva, 這個工具能夠驗證智能合約運行時的安全情況，它目前只支持以太坊的 Solidity。

• VeriSol，這個工具支持對智能合約語義的一致性進行形式化檢測，具體原理是使用訪問控制策略檢查狀態機工做流。

• FSolidM，這個工具能夠自動生成以太坊智能合約代碼，而且帶有圖形畫界面，界面上支持將智能合約設計爲有限狀態機的形式並進行驗證。

• SPIN，這個工具能夠檢測一個有限狀態系統是否知足 PLTL 公式以及其餘一些性質，包括是否有循環或可達性，它是一種顯式模型檢測工具。

6. 着色 Petri 網

Petri 網是 ２０世紀 ６０年代由 Carl Adam Petri 發 明的，適合於描述異步的、併發的系統模型。所謂的着色 Petri 網就是在原有 Petri 網的基礎上加入了顏色集和模型聲明等元素，藉此能夠表達更復雜的類型信息。這種方式的優勢是基於已有的 Petri 網模型，進行形式化驗證，具備良好的語義描述且具備圖形界面。可是當智能合約邏輯較爲複雜時，可能會致使可達圖生成難度增長，狀態空間爆炸等一系列問題。對於智能合約的安全性，功能性驗證能夠選擇此種方式。

當前技術應用的問題與展望

智能合約的形式化驗證雖然已經有了一些成果和進展，可是這個領域還只是剛剛開始，離發展完備還有很大的距離，在商用過程當中可能還存有下列問題：

• 易用性問題，形式化驗證一般須要具有專業知識的人員參與調試，一般參與編寫智能合約的人沒法掌握這種技術來檢驗合約的正確性，須要花費大量金錢找專業人士花很長時間來完成檢測。自動化的對智能合約進行形式化驗證也存在相關侷限性，通常狀況下自動化程度越高的方法和框架，驗證智能合約的性質越侷限。那將自動化形式化驗證方法擴大其普世性，而且支持非專業人士使用是急需解決的一個問題，從而才能立於形式化智能合約方法的普遍應用。

• 執行驗證的計算機的時間和內存的問題，形式化驗證經過探索儘量多的執行狀態來發現錯誤和安全問題的可能性。在這種狀況下，計算機運行時內存的上限和執行時間成爲複雜程序和協議的基本限制。商用場景中對於用戶沒法實施檢測出結果，須要長時間的等待和分析也會影響相關體驗。

• 正確性問題，當咱們使用形式化驗證工具時，咱們將代碼、安全目標和操做環境經過工具在不一樣模型之間轉換，將高級語言轉換爲形式化驗證工具支持的語言。工具的執行結果決定了形式化的準確性。可是，咱們沒有一個好的工具檢查語言轉換或者模型轉換的準確性，缺少對源代碼和目標語言的語義一致性須要進行嚴格的證實。對於任意的形式化系統，咱們須要經過查看人類的形式化代碼來檢查正確性，所以這就限制了形式化驗證的通常適用性。

• 信任性問題，當前形式化驗證智能合約的方法不斷增長，如何評判這種方式的準確度，其驗證的必要性，驗證合約的效率，都要靠開發人員憑藉其經驗，這種方式是否是和不用形式化驗證的測試沒有區別。並且當解決問題的成本超過問題自己時，咱們也會質疑解決該問題是否有意義。

咱們相信，隨着智能合約應用的法律化、區塊鏈技術的發展，形式化驗證方法在智能合約的全生命週期過程當中，將會起到愈來愈重要的做用，獲得更廣泛的應用。華爲區塊鏈服務基於上面的問題以及現有方式出發也打造了本身的形式化驗證工具，給出了其證實內容的正確性和必要性，而且提升其驗證效率，也是爲業界使用自動化形式化驗證方式給出一條探索和思考的路徑。

1. Luu, L.; Chu, D.H.; Olickel, H.; Saxena, P.; Hobor, A. Makingsmart contracts smarter. In Proceedings of the ACM SIGSAC Conf. Comput. Commun.Securit, New York, NY, USA, 24–28 October 2016; pp. 254–269.

2. Atzei, N.; Bartoletti, M.; Cimoli, T. A Survey of Attacks onEthereum Smart Contracts (SoK). In Proceedings of the Int. Conf. Princ. Secur.Trust, Uppsala, Sweden, 22–29 April 2017; pp. 164–186. 3. The DAO Attacked:Code Issue Leads to $60 Million Ether Theft. Available online:www.coindesk. com/dao-attacked-code-issue-leads-60-million-ether-theft/(accessed on 17 June 2017).

3. Liu, J.; Liu, Z.T. A Survey on Security Verification of BlockchainSmart Contracts. IEEE Access 2019, 7, 77894–77904. [CrossRef]

4. 王璞巍，楊航天，孟佶，等．面向合同的智能合約的形式化定義及參考實現［Ｊ］．軟件學報，２０１９，３０（９）：２６０８－２６１９．

5. 胡凱，白曉敏，等．智能合約的形式化驗證方法［Ｊ］．信息安全研究，２０１６，２（１２）：１０８０－１０８９．

點擊關注，第一時間瞭解華爲雲新鮮技術~