智能合約自動化審計技術淺析

一、智能合約發展現狀

首先我們來一起看看現在智能合約發展的一個現狀：在過去一個月當中，智能合約的數量每天還在以1317個的平均增長率高速穩定的增長着，這和我們所了解的“區塊鍊現在處于寒冬的時期”不太一樣，其實智能合約的增長率還是比較穩定的。

現在智能合約比較多的應用在一些基礎設施、商業零售、遊戲以及社交媒體和通訊領域中。

二、智能合約安全現狀

從17年9月到18年6月，智能合約的漏洞頻繁爆發，每次漏洞爆發都帶來了大量的資金損失。這使得一些區塊鍊開發者、智能合約的開發者或者一些使用者對智能合約安全性産生高度的質疑，也阻礙了以太坊之後的一些發展。

除了基本的智能合作安全，現在DAPP的安全也是受到了極大的關注。比如說FOMO3D在興起的時候，僅僅在第二天就出現了大量的山寨合約、山寨的遊戲。在這些遊戲中，開發者巧妙地更改了資金配置設定的邏輯，使得玩家在玩FOMO3D遊戲的過程中，投入的資金其實大部分都是流向于這種山寨合約的開發者的，這對DAPP的發展有了極大的阻礙。

現在我們共同面臨着一個問題——如何保證海量的智能合約的安全。

三、智能合約自動化審計方法

我們來回顧一下現在智能合約的情況。截止到昨天中午12點，據統計，現在共有193萬個智能合約，并且一直保持着穩定的日增長率。現在的審計方法有人工的攻防審計以及自動化的審計。

在海量的智能合約中，最好的一種設想就是要降低人工審計的一些複雜度，進而更多的通過自動化審計來進行。

我們把自動化審計分為三個部分：

第一種就是特征代碼的比對，第二類就是基于形态化驗證的自動化審計，最後一類是基于符号執行和符号抽象的自動化審計。

1、特征代碼比對

我們首先看這一項，特定代碼比對。大家從名字上來看應該就能了解到，其實它就是對惡意代碼進行一些提取抽象，像我們之前做的代碼靜态檢測，我們抽樣成一種語義比對，然後再去比對它的靜态源代碼。

這種審計的方法的優點是顯而易見的，比如說速度很快，因為它就是對原碼進行一個字元串的比對。第二是它能夠迅速的響應新的漏洞，因為這種審計方法大部分是以插件形式開發，比如出現了一個新的漏洞，我們就可以快速送出一些新的比對模式。

那麼它的缺點在哪裡呢？我們所了解的現在的區塊鍊都應該是公開透明的，但實際情況并不是這樣，我們大概做了一個統計，目前代碼的開源率僅僅隻占48.62%，

也就是在以太坊上其實有超過一半的智能合約是不開源的，隻暴露它的一個OPCODE。

對于OPCODE的分析對于安全人員來說其實也是面臨着巨大的挑戰，有些人費了十分大的力氣，去逆向OPCODE，這就導緻了它的适用範圍極為有限。

其次就是漏報率高。因為它的一些靜态審計方法其實并不和傳統的靜态代碼審計方法一緻，傳統的靜态審計方法，比如說APP檢測，我會調用庫裡面，确定穩定的一些函數，來對它進行審計，但智能合約裡面它的一些函數、它一些特征等等，還是變化性比較多的，是以說它的漏報率會比較高。

2、基于形式化驗證的自動化審計

第二個方法，我們來探讨一下現在比較火的，基于形式化驗證的自動化審計。

形式化驗證來審計智能合約安全，最早是在16年，由Hirai提供的，當時拿Isabelle高階邏輯互動定理證明器，然後交EVM的一些OPCODE ，通過它的一個lem language轉化成了一個形式化的model，然後通過形式化model的驗證來去判斷它代碼中的邏輯是否存在問題。

而基于這項工作，之後由兩個學家把形式化方法進行了進一步的改正，也就是說他們放棄了lem language這種比較低效的轉換方式，采用了F-framework和K-framework将DVM轉化為一個formal model，而F-framework就是NASA他們經常在航空航天領域當中做一些形式化漏洞驗證的架構，而K-framework就是語意的一些整合架構。

3、基于符号執行、符号抽象的自動化審計

第三點，也是我今天想要着重跟大家交流的，以及現在最常用的方法，就是基于符号執行和符号抽象的一些自動化審計。

我們在分析一個智能合約的時候，我們首先要明确我們的分析對象是什麼。也就像我們剛才在解釋的那個特征比對代碼當中，我們知道其實作在EVM上合約代碼大部分是不公開的。

我們就确認應該是一個EVM OPCODE，通過一些源碼，編譯，可以形成一個OPCODE，然後輸入到我們自動化分析引擎。

在這種基于符号執行和符号抽象化的自動化審計架構裡面，其實它有些共有的特性，就是它在OPCODE或者在輸到這個引擎之後，都會轉化成一個CFG，就是我們的一個Control flow graph，即控制流程圖。

可以簡單了解一下這個CFG是什麼意思。CFG就是說他把合約代碼裡面的邏輯包裝成每個塊，然後有邏輯有分叉的時候，比如說有IF等等這種判斷的時候，就把它分叉。

比如說左邊這個assertion這個合約，我們首先是将input與256進行一個比較，那麼在出現一個If的判斷之後，我們需要對這個CFG進行一個分叉。

CFG Builder主要是對OPCODE這種智能合約代碼，把它形成一個十分龐大完善的一個CFG，然後讓程式員更好的去了解它裡面執行的一些邏輯。再有CFG生成了之後，就是這樣兩種分析方法。

第一類就是基于符号執行的驗證，這邊比較有代表性的，可能大家都比較熟知的像Mythril、Oyente、Maian。還有一種就是，上個月他們剛剛公開的一個符号抽象分析的方法，也就是Securify。

下面主要分析一下Oyente以及Securify這兩種系統的一個具體的架構以及實作方法。

Oyente符号執行驗證

Oyente的邏輯是在CFGbuild形成之後，首先是一個EXPLORER，EXPLORER的意思就是說我會把代碼當中的每一個流程都去驗證一遍，進行一個之外的驗證。

我們的驗證就是是否有一個X，使得X不僅滿足C1、C2、C3三個條件，并且Z=X+2，那麼這時候我們可以判斷他的狀态是no還是yes，然後以此來驗證整個邏輯的一個流程。

到了第二個code analysis，這一部分其實是這個Oyente最為核心的一個部分，就是它将剛剛輸出的EXPLORSE這種路徑把它轉化，至始至終隻包含Ether的一些路徑，進行一些漏洞驗證，而他目前隻提供包括TOD、Timestamp dependence、Mishandled exceptions這三種驗證，最後系統為了保證誤報率和漏報率，采用了微軟的Z3Bit-Vector Solver 開源的驗證器，然後來進行整體架構的一個封裝。

在剛剛我們講述的過程當中，其實大家也應該了解到，在CFG轉EXPLORER驗證的時候，我們需要對它的循環的每次都進行一個驗證，是以說這種分析方法特别耗時，并且也不一定成功。

比如說像parity的那個錢包代碼，它的Oyente覆寫率僅僅達到20%，剩下80%的代碼，是沒有辦法去跟蹤的，是以這就是Oyente目前存在一個巨大的問題。

Securify符号抽象分析

在這個問題的基礎上，像Securify他們就提供了另外一種方法，它們認為現在合約代碼其實是特别容易解耦合的，不像我們傳統的代碼一樣，它的耦合性特别高，但像合約代碼裡面，就有transfer等等一些比較固定解耦合的一些結構和子產品，我們并不是需要對整個合約的邏輯進行的校驗，可能我們就是對合約解耦合的各個子產品進行校驗分析，是以可以提高它的自動化程度。

這張圖也就是他們整個在驗證的一個流程：

它們把contract bytecode轉化成一種他們自定義的一種語義語言，然後通過自定義的語義語言，它們之後有一個驗證子產品，這個驗證子產品就特别像我們之前說的那種模式比對，就是把一些漏洞轉化成一種它驗證語言的模式比對的架構，然後去驗證它這個語意在此是否滿足他這個比較，最終會生成一個安全報告。

這裡也給出了一個parity的例子，通過自動化審計的方法，最終可以輸出錢包的owner其實是可以被修改的。

再具體一點，它是怎麼做語義分析的呢？Securify分析這種合約代碼，是從兩個次元，第一個是邏輯，第二個是資料。

在邏輯方向的話，它定義了兩種邏輯，第一個叫MayFollow，第二叫MustFollow。MayFollow的意思是說L2是有一條路徑是跟在L1後面的，而MustFollow是說L2每一條路徑都跟在L1後面。這兩種差別定了它整個邏輯的一個架構。

第一個就是它的一個資料，它怎麼定義合約裡面的資料變化？分了三種，第一種是MayDepOn，就是兩個因素，一個叫Y、一個叫T，T變Y可能變也可能不變。

第二個就是Eq，就是說Y是由T來決定的

第三個就是大家把DetBy和Y和T是一一對應的，隻要T變Y就肯定要變了。

這裡面就用更加形象的方法，我們想象一下，MayDepOn就是，變量是T，在一段時間當中Y可能是一個值，然後有的說T變Y可能不變，第三個DetBy就是說一對一的關系，就比如說我們知道哈希，哈希如果T變，Y就肯定要變。

通過邏輯和資料這兩個次元進行了一些驗證，最終驗證子產品的話，現在提供了大概六七個智能合約漏洞的驗證性的語言，而且這種語言都是以插件化的形式來寫的，其他的安全開發者可以不斷去豐富這個漏洞的驗證語言，最終我們在對自動化審計進行一個評估的時候，我們其實是要從它的自動化程度，漏報率、誤報率來評估這件事情的。

像我們現在知道的一些資料就可以表明出來，其實像Mythril跟Oyente，它裡面存在大量的誤報，比如說它檢測出來的資料還是需要人工進行二次确認，這個工作其實是非常繁瑣，而Securify這種方法可能誤報率會降低。

這也是兩種比較現在比較流行的符号執行和抽象的自動化審計方法。

四、總結回顧

最後我們回顧一下，現在做的智能合約審計的話可能分為三種，：特征代碼比對、形式化驗證以及符号抽象。

回顧整個解釋的過程當中，我們可以清楚地知道，現在自動化審計的方法其實是出于一個很不成熟的階段。

它們主要面臨三大問題：

第一個就是誤報率高，其實它并不能做到完全自動化，它還需要人工的一些參與。

第二個就是它的自動化其實程度比較低，還需要不斷有feedback去去審計。

第三就是審計時間比較長，比如說像Mythril，平均在60秒，Oyente大概在30秒，而Securify大概在20秒。

http://www.xyqkl.cn/