經過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秒。