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

什么是形式化驗(yàn)證？

維基百科對形式化驗(yàn)證的解釋是這樣的： 在計(jì)算機(jī)硬件（特別是集成電路）和軟件系統(tǒng)的設(shè)計(jì)過程中，形式化驗(yàn)證的含義是根據(jù)某個(gè)或某些形式化規(guī)范或?qū)傩?，使用?shù)學(xué)的方法證明其正確性或非正確性。傳統(tǒng)上在硬件設(shè)計(jì)領(lǐng)域比較常用。主要原因就是硬件設(shè)計(jì)周期長，成本高，一旦生產(chǎn)出來就很難改動了。例如一個(gè) CPU 設(shè)計(jì)如果已經(jīng)出芯片了，那么出了問題就是大事。形式驗(yàn)證可以分為三大類：抽象解釋（Abstract Interpretation）、形式模型檢查（Formal Model Checking，也被稱作特性檢查）和定理證明（Theory Prover）。

區(qū)塊鏈智能合約為什么需要形式化驗(yàn)證？

在區(qū)塊鏈系統(tǒng)中可以編程且自動運(yùn)行的程序被稱為智能合約。智能合約最早在以太坊區(qū)塊鏈平臺上應(yīng)用，如Solidity就是一種智能合約編程語言，以使傳統(tǒng)應(yīng)用程序開發(fā)人員能夠編寫智能合約。初期會Solidity語言的全球只有幾百人，后來隨著以太坊與區(qū)塊鏈的火熱，參與Solidity智能合約的人才開始逐漸增加，但是跟整個(gè)IT市場的從業(yè)人群比起來，會編寫智能合約的人還是太少，大量的IT從業(yè)者要想開發(fā)智能合約只能去學(xué)習(xí)Solidity。為了讓更多的IT從業(yè)者可以參與智能合約的編寫與業(yè)務(wù)規(guī)則的實(shí)現(xiàn)，智能合約平臺在原有Solidity的基礎(chǔ)上擴(kuò)展了對更多主流語言，甚至高級語言的支持，這樣可以讓多普通It從業(yè)人員也有了可以進(jìn)行智能合約編寫的可能性，大量熟悉Java、Go、Php等技術(shù)編程的開發(fā)人員都可以參與智能合約的開發(fā)。

?

然而，由于區(qū)塊鏈交易是不可變的，智能合約代碼中的錯(cuò)誤會產(chǎn)生毀滅性的后果，破壞了對底層區(qū)塊鏈技術(shù)的信任。例如，臭名昭著的TheDAO漏洞導(dǎo)致價(jià)值近6000萬美元的以太損失，奇偶校驗(yàn)錢包漏洞導(dǎo)致價(jià)值1.69億美元的以太永遠(yuǎn)被鎖定。解決這些事件的唯一補(bǔ)救辦法是硬分叉區(qū)塊鏈，并將其中一個(gè)分叉恢復(fù)到事件發(fā)生前的狀態(tài)。然而，這種補(bǔ)救辦法本身是毀滅性的，因?yàn)樗輾Я藚^(qū)塊鏈的核心價(jià)值，如不可變性和分散信任。但是智能合約的編寫目的是為了行業(yè)應(yīng)用，一旦應(yīng)用到實(shí)際中必須考慮智能合約的安全性，智能合約要達(dá)到機(jī)器可信，就必須首先排除掉因人為因素而造成的智能合約破壞情形。智能合約形式化驗(yàn)證提供了一種可以證明的安全檢驗(yàn)機(jī)制，通過形式化語言把合約中的概念、判斷、推理轉(zhuǎn)化成智能合約模型，可以消除自然語言的歧義性、不通用性，進(jìn)而采用形式化工具對智能合約建模、分析和驗(yàn)證，進(jìn)行一致性測試，最后自動生成驗(yàn)證過的合約代碼，形成智能合約生產(chǎn)的可信全生命周期?？梢园咽袌錾弦呀?jīng)出現(xiàn)的安全風(fēng)險(xiǎn)進(jìn)行排查與審計(jì)，經(jīng)過審計(jì)后的智能合約代碼自然安全性就得到增強(qiáng)，同時(shí)智能合約形式化驗(yàn)證也是目前對智能合約進(jìn)行安全保證最可靠的措施。行業(yè)應(yīng)用區(qū)塊鏈與智能合約，就需要進(jìn)行智能合約 的形式化驗(yàn)證，消除安全隱患。

?

智能合約形式化驗(yàn)證方法分類

業(yè)界通常對智能合約進(jìn)行形式化驗(yàn)證都有一些通用的方法，大體上分為下面幾種通用的方法，每種方法都有一些工具和框架進(jìn)行支撐。

1. 定理證明

定理證明是一種利用演繹推理在符號邏輯中提供證明的形式化方法．在這種方法中，證明的每個(gè)步驟都 會引入一個(gè)公理或一個(gè)前提，并提供一個(gè)陳述，使用謂詞邏輯將其進(jìn)行推導(dǎo)，最終得到想要驗(yàn)證的結(jié)果．在證明系統(tǒng)滿足關(guān)鍵期望的過程中，一般使用定理證明器來做輔助驗(yàn)證工作，因?yàn)檫@需要將手工證明的過程變成一系列能夠在計(jì)算機(jī)上運(yùn)行的符號演算，且可以對正確性進(jìn)行檢查。

其優(yōu)勢是這個(gè)方式是使用數(shù)學(xué)的方法，通過公理或前提進(jìn)行推導(dǎo)，保證驗(yàn)證的嚴(yán)謹(jǐn)性。其不足是在做數(shù)學(xué)驗(yàn)證前需要將不同類型的源代碼轉(zhuǎn)換為相關(guān)框架的驗(yàn)證代碼，而目前沒有很好地辦法保證在源代碼與驗(yàn)證代碼之間的轉(zhuǎn)換一致性，實(shí)現(xiàn)成本高，自動化水平低，正確性也是很難保證的。在區(qū)塊鏈智能合約領(lǐng)域一般對于有高隱私性，安全性，功能性，語義一致性等強(qiáng)烈的需求會通過這種法法來保證。

那業(yè)界在定理證明還是實(shí)現(xiàn)了很多工具和框架支撐這一能力，基本有下面的一些工具：

Solidity* and EVM*，該框架使用函數(shù)式語言F*分析驗(yàn)證了Solidity智能合約運(yùn)行時(shí)的正確性，F(xiàn)*是一種函數(shù)式編程語言，用于形式化驗(yàn)證程序的正確性。

Corral是Boogie語言的分析工具．默認(rèn)情況下，Corral會進(jìn)行有界搜索，直到遞歸深度和固定數(shù)量到達(dá)一定限度為止，Boogie是一種中間驗(yàn)證語言，旨在構(gòu)建其他語言的驗(yàn)證程序的中間層。

Coq是一個(gè)交互式定理證明助手，它提供了一種形式化的語言來編寫數(shù)學(xué)定義，可執(zhí)行 算法和定理

Isabelle/HOL是一個(gè)基于高階邏輯的通用交互式定理證明器.

Raziel是一個(gè)編程框架，用于驗(yàn)證智能合約的多方計(jì)算的安全問題，為智能合約的隱私 性提供保障.

2. 符號執(zhí)行

符號執(zhí)行（英語：symbolic execution）是一種計(jì)算機(jī)科學(xué)領(lǐng)域的程序分析技術(shù)，通過采用抽象的符號代替精確值作為程序輸入變量，得出每個(gè)路徑抽象的輸出結(jié)果。 這一技術(shù)在硬件、底層程序測試中有一定的應(yīng)用，能夠有效的發(fā)現(xiàn)程序中的漏洞。這種方式的優(yōu)點(diǎn)是以符號值作為輸入，借助相應(yīng)工具，可得到具體測試用例，具有很高的代碼覆蓋率。那這種方式本質(zhì)上屬于測試，不能１００％證明智能合約是沒有問題的，因?yàn)榛跍y試是很難以100%覆蓋所有的場景，一般在做合約的安全性，功能性驗(yàn)證會推薦使用這種方式。

基于符號執(zhí)行的業(yè)界的一些比較有名的架構(gòu)如下：

·???????? SASC，這個(gè)工具被用來發(fā)現(xiàn)潛在的邏輯風(fēng)險(xiǎn)，它是一種靜態(tài)分析的工具，且可以生成調(diào)用關(guān)系的拓?fù)鋱D。

·???????? MAIAN，這個(gè)工具被用來查詢漏洞，被設(shè)計(jì)成利用符號分析和具體驗(yàn)證器來跟蹤智能合約中的屬性。

·???????? Securify，這個(gè)工具被用來進(jìn)行安全漏洞分析，它是一個(gè)專門針對以太坊智能合約的工具。

·???????? Mythril，這個(gè)工具被用來進(jìn)行代碼安全分析，是一個(gè)針對以太坊的智能合約的符號執(zhí)行的工具。

·???????? Verx是一個(gè)可以自動驗(yàn)證以太坊智能合約功能性的驗(yàn)證器，以太坊相關(guān)的問題可以通過上面三個(gè)工具組合使用來提高覆蓋面。

·???????? Oyente，這個(gè)工具被用來檢測合約代碼潛在的安全漏洞，是一個(gè)基于符號執(zhí)行技術(shù)的測試工具。

3. 模型檢測

模型檢測(model checking)，是一種重要的自動驗(yàn)證和分析技術(shù)，由Clarke和Emerson以及Quelle和Sifakis提出，主要通過顯式狀態(tài)搜索或隱式不動點(diǎn)計(jì)算來驗(yàn)證有窮狀態(tài)并發(fā)系統(tǒng)的模態(tài)/命題性質(zhì)。其基本思想是檢驗(yàn)一個(gè)結(jié)構(gòu)是否滿足一個(gè)公式要比證明公式在所有結(jié)構(gòu)下均被滿足容易得多，進(jìn)而面向并發(fā)系統(tǒng)創(chuàng)立了在有窮狀態(tài)模型上檢驗(yàn)公式可滿足性的驗(yàn)證新形式，這種方法也被用于驗(yàn)證智能合約的正確性。

它的優(yōu)點(diǎn)是可以使用市面上現(xiàn)有的模型檢測工具，并且支持自動化驗(yàn)證，減少人為參與。但是其無法保證所使用的模型檢測工具的完備性與正確性，合約復(fù)雜度過高會導(dǎo)致狀態(tài)空間爆炸，進(jìn)而導(dǎo)致無法完成驗(yàn)證能力。一般情況下需要保證合約的安全性，功能性會使用這種方式。

業(yè)界也有不少這種類型的工具和架構(gòu)如下：

·???????? NuSMV，這個(gè)工具被用于用于工業(yè)設(shè)計(jì)的驗(yàn)證，具有極高的可靠性，且被設(shè)計(jì)成模型檢查的開放架構(gòu)。它是SMV工具的重新實(shí)現(xiàn)和擴(kuò)展，而SMV是第一個(gè)基于BDD的模型檢查器。

·???????? BIP， 這個(gè)框架包含一整套支持建模、模型轉(zhuǎn)換、仿真、驗(yàn)證和代碼生成的工具集，還支持層次化結(jié)構(gòu),被設(shè)計(jì)成為一個(gè)通用的系統(tǒng)級形式化建?？蚣?。

·???????? Prism，這個(gè)工具只針對表現(xiàn)出隨機(jī)或概率行為的系統(tǒng)，被設(shè)計(jì)成一個(gè)概率模型檢查器，對概率行為進(jìn)行形式化建模和分析。

·???????? SMC，這個(gè)工具被設(shè)計(jì)成模型檢測器，用于檢查在不同公平性假設(shè)下并發(fā)程序的安全性和活性。

4. 形式化建模

可以通過準(zhǔn)確的數(shù)學(xué)語句和模型組件去定義不同組件的關(guān)系，消除系統(tǒng)中存在的二義性，這種設(shè)計(jì)系統(tǒng)的技術(shù)就是形式化建模?；谶@種方式的系統(tǒng)的仿真結(jié)果是可以復(fù)現(xiàn)的，不會存在偶發(fā)性事件。這種方法的優(yōu)點(diǎn)就是使用精確的數(shù)學(xué)語句或模型組件來設(shè)計(jì)系統(tǒng)，從而保證其仿真結(jié)果可被復(fù)現(xiàn)。但是此方法大多使用市面上已有的建?？蚣?，其框架的完備性與正確性無法保證?；谥悄芎霞s的隱私性，安全性和功能性可以使用這種方法來檢驗(yàn)。Hydra，就是基于形式化建模的一個(gè)框架，該框架鼓勵(lì)開發(fā)者和用戶誠實(shí)地披露智能合約中的錯(cuò)誤和漏洞，它的設(shè)計(jì)是基于漏洞賞金的模式和NNVP編程。

5. 有限狀態(tài)機(jī)

有限狀態(tài)機(jī)是一種用來進(jìn)行對象行為建模的工具，其作用主要是描述對象在它的生命周期內(nèi)所經(jīng)歷的狀態(tài)序列，以及如何響應(yīng)來自外界的各種事件。智能合約的執(zhí)行也可以看作從一個(gè)狀態(tài)到下一個(gè)狀態(tài)的變遷。

這個(gè)方法的優(yōu)點(diǎn)是思維導(dǎo)向簡單，將智能合約抽象轉(zhuǎn)換為狀態(tài)機(jī)的形式，易于操作，且具有圖形界面。但是狀態(tài)定義的好壞，對智能合約的驗(yàn)證難易程度有很強(qiáng)相關(guān)性，合約復(fù)雜度過高也會導(dǎo)致狀態(tài)空間爆炸。對智能合約的安全性，語義一致性校驗(yàn)一般會使用這種方式。

業(yè)界一般的工具介紹如下：

·???????? Contract Larva, 這個(gè)工具可以驗(yàn)證智能合約運(yùn)行時(shí)的安全狀況，它目前只支持以太坊的Solidity。

·???????? VeriSol，這個(gè)工具支持對智能合約語義的一致性進(jìn)行形式化檢測，具體原理是使用訪問控制策略檢查狀態(tài)機(jī)工作流。

·???????? FSolidM，這個(gè)工具可以自動生成以太坊智能合約代碼，并且?guī)в袌D形畫界面，界面上支持將智能合約設(shè)計(jì)為有限狀態(tài)機(jī)的形式并進(jìn)行驗(yàn)證。

·???????? SPIN，這個(gè)工具可以檢測一個(gè)有限狀態(tài)系統(tǒng)是否滿足PLTL公式以及其他一些性質(zhì)，包括是否有循環(huán)或可達(dá)性，它是一種顯式模型檢測工具。

6.著色Petri網(wǎng)

Petri網(wǎng)是 ２０世紀(jì) ６０年代由Carl Adam Petri發(fā) 明的，適合于描述異步的、并發(fā)的系統(tǒng)模型。所謂的著色Petri網(wǎng)就是在原有Petri網(wǎng)的基礎(chǔ)上加入了顏色集和模型聲明等元素，借此可以表達(dá)更復(fù)雜的類型信息。這種方式的優(yōu)點(diǎn)是基于已有的Petri網(wǎng)模型，進(jìn)行形式化驗(yàn)證，具有良好的語義描述且具有圖形界面。但是當(dāng)智能合約邏輯較為復(fù)雜時(shí)，可能會導(dǎo)致可達(dá)圖生成難度增加，狀態(tài)空間爆炸等一系列問題。對于智能合約的安全性，功能性驗(yàn)證可以選擇此種方式。

?

當(dāng)前技術(shù)應(yīng)用的問題與展望

智能合約的形式化驗(yàn)證雖然已經(jīng)有了一些成果和進(jìn)展，但是這個(gè)領(lǐng)域還只是剛剛開始，離發(fā)展完備還有很大的距離，在商用過程中可能還存有下列問題：

·???????? 易用性問題，形式化驗(yàn)證通常需要具備專業(yè)知識的人員參與調(diào)試，通常參與編寫智能合約的人無法掌握這種技術(shù)來檢驗(yàn)合約的正確性，需要花費(fèi)大量金錢找專業(yè)人士花很長時(shí)間來完成檢測。自動化的對智能合約進(jìn)行形式化驗(yàn)證也存在相關(guān)局限性，一般情況下自動化程度越高的方法和框架，驗(yàn)證智能合約的性質(zhì)越局限。那將自動化形式化驗(yàn)證方法擴(kuò)大其普世性，并且支持非專業(yè)人士使用是急需解決的一個(gè)問題，從而才能立于形式化智能合約方法的廣泛應(yīng)用。

·???????? 執(zhí)行驗(yàn)證的計(jì)算機(jī)的時(shí)間和內(nèi)存的問題，形式化驗(yàn)證通過探索盡可能多的執(zhí)行狀態(tài)來發(fā)現(xiàn)錯(cuò)誤和安全問題的可能性。在這種情況下，計(jì)算機(jī)運(yùn)行時(shí)內(nèi)存的上限和執(zhí)行時(shí)間成為復(fù)雜程序和協(xié)議的基本限制。商用場景中對于用戶無法實(shí)施檢測出結(jié)果，需要長時(shí)間的等待和分析也會影響相關(guān)體驗(yàn)。

·???????? 正確性問題，當(dāng)我們使用形式化驗(yàn)證工具時(shí)，我們將代碼、安全目標(biāo)和操作環(huán)境通過工具在不同模型之間轉(zhuǎn)換，將高級語言轉(zhuǎn)換為形式化驗(yàn)證工具支持的語言。工具的執(zhí)行結(jié)果決定了形式化的準(zhǔn)確性。但是，我們沒有一個(gè)好的工具檢查語言轉(zhuǎn)換或者模型轉(zhuǎn)換的準(zhǔn)確性，缺乏對源代碼和目標(biāo)語言的語義一致性需要進(jìn)行嚴(yán)格的證明。對于任意的形式化系統(tǒng)，我們需要通過查看人類的形式化代碼來檢查正確性，因此這就限制了形式化驗(yàn)證的一般適用性。

·???????? 信任性問題，當(dāng)前形式化驗(yàn)證智能合約的方法不斷增加，如何評判這種方式的準(zhǔn)確度，其驗(yàn)證的必要性，驗(yàn)證合約的效率，都要靠開發(fā)人員憑借其經(jīng)驗(yàn)，這種方式是不是和不用形式化驗(yàn)證的測試沒有區(qū)別。而且當(dāng)解決問題的成本超過問題本身時(shí)，我們也會質(zhì)疑解決該問題是否有意義。

?

我們相信，隨著智能合約應(yīng)用的法律化、區(qū)塊鏈技術(shù)的發(fā)展，形式化驗(yàn)證方法在智能合約的全生命周期過程中，將會起到越來越重要的作用，得到更普遍的應(yīng)用。華為區(qū)塊鏈服務(wù)基于上面的問題以及現(xiàn)有方式出發(fā)也打造了自己的形式化驗(yàn)證工具，給出了其證明內(nèi)容的正確性和必要性，并且提高其驗(yàn)證效率，也是為業(yè)界使用自動化形式化驗(yàn)證方式給出一條探索和思考的路徑。

?