智慧合約自動化審計技術淺析
前言
經過THE DAO事件、幣安被盜事件，智慧合約的安全性越來越受到業內關注。本文根據獵豹區塊鏈安全專家楊文玉9月5日在星球日報P.O.D大會上的分享錄音整理而成，淺析當前智慧合約的發展現狀，以及智慧合約自動化檢測的一些方法。
一、智慧合約發展現狀
首先我們來一起看看現在智慧合約發展的一個現狀：在過去一個月當中，智慧合約的數量每天還在以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秒。
*本文作者：獵豹區塊鏈安全實驗室，轉載請註明來自FreeBuf.COM