經(jīng)過THE DAO事件、幣安被盜事件，智能合約的安全性越來越受到業(yè)內(nèi)關(guān)注。本文根據(jù)獵豹區(qū)塊鏈安全專家楊文玉9月5日在星球日報(bào)P.O.D大會上的分享錄音整理而成，淺析當(dāng)前智能合約的發(fā)展現(xiàn)狀，以及智能合約自動化檢測的一些方法。
一、智能合約發(fā)展現(xiàn)狀
首先我們來一起看看現(xiàn)在智能合約發(fā)展的一個現(xiàn)狀：在過去一個月當(dāng)中，智能合約的數(shù)量每天還在以1317個的平均增長率高速穩(wěn)定的增長著，這和我們所理解的“區(qū)塊鏈現(xiàn)在處于寒冬的時期”不太一樣，其實(shí)智能合約的增長率還是比較穩(wěn)定的。
現(xiàn)在智能合約比較多的應(yīng)用在一些基礎(chǔ)設(shè)施、商業(yè)零售、游戲以及社交媒體和通訊領(lǐng)域中。
二、智能合約安全現(xiàn)狀
從17年9月到18年6月，智能合約的漏洞頻繁爆發(fā)，每次漏洞爆發(fā)都帶來了大量的資金損失。這使得一些區(qū)塊鏈開發(fā)者、智能合約的開發(fā)者或者一些用戶對智能合約安全性產(chǎn)生高度的質(zhì)疑，也阻礙了以太坊之后的一些發(fā)展。
除了基本的智能合作安全，現(xiàn)在DAPP的安全也是受到了極大的關(guān)注。比如說FOMO3D在興起的時候，僅僅在第二天就出現(xiàn)了大量的山寨合約、山寨的游戲。在這些游戲中，開發(fā)者巧妙地更改了資金分配的邏輯，使得玩家在玩FOMO3D游戲的過程中，投入的資金其實(shí)大部分都是流向于這種山寨合約的開發(fā)者的，這對DAPP的發(fā)展有了極大的阻礙。
現(xiàn)在我們共同面臨著一個問題——如何保證海量的智能合約的安全。
三、智能合約自動化審計(jì)方法
我們來回顧一下現(xiàn)在智能合約的情況。截止到昨天中午12點(diǎn)，據(jù)統(tǒng)計(jì)，現(xiàn)在共有193萬個智能合約，并且一直保持著穩(wěn)定的日增長率。現(xiàn)在的審計(jì)方法有人工的攻防審計(jì)以及自動化的審計(jì)。
在海量的智能合約中，最好的一種設(shè)想就是要降低人工審計(jì)的一些復(fù)雜度，從而更多的通過自動化審計(jì)來進(jìn)行。
我們把自動化審計(jì)分為三個部分：
第一種就是特征代碼的匹配，第二類就是基于形態(tài)化驗(yàn)證的自動化審計(jì)，最后一類是基于符號執(zhí)行和符號抽象的自動化審計(jì)。
1、特征代碼匹配
我們首先看這一項(xiàng)，特定代碼匹配。大家從名字上來看應(yīng)該就能理解到，其實(shí)它就是對惡意代碼進(jìn)行一些提取抽象，像我們之前做的代碼靜態(tài)檢測，我們抽樣成一種語義匹配，然后再去匹配它的靜態(tài)源代碼。
這種審計(jì)的方法的優(yōu)點(diǎn)是顯而易見的，比如說速度很快，因?yàn)樗褪菍υa進(jìn)行一個字符串的匹配。第二是它能夠迅速的響應(yīng)新的漏洞，因?yàn)檫@種審計(jì)方法大部分是以插件形式開發(fā)，比如出現(xiàn)了一個新的漏洞，我們就可以快速提交一些新的匹配模式。
那么它的缺點(diǎn)在哪里呢？我們所理解的現(xiàn)在的區(qū)塊鏈都應(yīng)該是公開透明的，但實(shí)際情況并不是這樣，我們大概做了一個統(tǒng)計(jì)，目前代碼的開源率僅僅只占48.62%，
也就是在以太坊上其實(shí)有超過一半的智能合約是不開源的，只暴露它的一個OPCODE。
對于OPCODE的分析對于安全人員來說其實(shí)也是面臨著巨大的挑戰(zhàn)，有些人費(fèi)了十分大的力氣，去逆向OPCODE，這就導(dǎo)致了它的適用范圍極為有限。
其次就是漏報(bào)率高。因?yàn)樗囊恍╈o態(tài)審計(jì)方法其實(shí)并不和傳統(tǒng)的靜態(tài)代碼審計(jì)方法一致，傳統(tǒng)的靜態(tài)審計(jì)方法，比如說APP檢測，我會調(diào)用庫里面，確定穩(wěn)定的一些函數(shù)，來對它進(jìn)行審計(jì)，但智能合約里面它的一些函數(shù)、它一些特征等等，還是變化性比較多的，所以說它的漏報(bào)率會比較高。
2、基于形式化驗(yàn)證的自動化審計(jì)
第二個方法，我們來探討一下現(xiàn)在比較火的，基于形式化驗(yàn)證的自動化審計(jì)。
形式化驗(yàn)證來審計(jì)智能合約安全，最早是在16年，由Hirai提供的，當(dāng)時拿Isabelle高階邏輯交互定理證明器，然后交EVM的一些OPCODE ，通過它的一個lem language轉(zhuǎn)化成了一個形式化的model，然后通過形式化model的驗(yàn)證來去判斷它代碼中的邏輯是否存在問題。
而基于這項(xiàng)工作，之后由兩個學(xué)家把形式化方法進(jìn)行了進(jìn)一步的改正，也就是說他們放棄了lem language這種比較低效的轉(zhuǎn)換方式，采用了F-framework和K-framework將DVM轉(zhuǎn)化為一個formal model，而F-framework就是NASA他們經(jīng)常在航空航天領(lǐng)域當(dāng)中做一些形式化漏洞驗(yàn)證的框架，而K-framework就是語意的一些整合框架。
3、基于符號執(zhí)行、符號抽象的自動化審計(jì)
第三點(diǎn)，也是我今天想要著重跟大家交流的，以及現(xiàn)在最常用的方法，就是基于符號執(zhí)行和符號抽象的一些自動化審計(jì)。
我們在分析一個智能合約的時候，我們首先要明確我們的分析對象是什么。也就像我們剛才在解釋的那個特征匹配代碼當(dāng)中，我們知道其實(shí)現(xiàn)在EVM上合約代碼大部分是不公開的。
我們就確認(rèn)應(yīng)該是一個EVM OPCODE，通過一些源碼，編譯，可以形成一個OPCODE，然后輸入到我們自動化分析引擎。
在這種基于符號執(zhí)行和符號抽象化的自動化審計(jì)框架里面，其實(shí)它有些共有的特性，就是它在OPCODE或者在輸?shù)竭@個引擎之后，都會轉(zhuǎn)化成一個CFG，就是我們的一個Control flow graph，即控制流程圖。
可以簡單了解一下這個CFG是什么意思。CFG就是說他把合約代碼里面的邏輯包裝成每個塊，然后有邏輯有分叉的時候，比如說有IF等等這種判斷的時候，就把它分叉。
比如說左邊這個assertion這個合約，我們首先是將input與256進(jìn)行一個比較，那么在出現(xiàn)一個If的判斷之后，我們需要對這個CFG進(jìn)行一個分叉。
CFG Builder主要是對OPCODE這種智能合約代碼，把它形成一個十分龐大完善的一個CFG，然后讓程序員更好的去了解它里面執(zhí)行的一些邏輯。再有CFG生成了之后，就是這樣兩種分析方法。
第一類就是基于符號執(zhí)行的驗(yàn)證，這邊比較有代表性的，可能大家都比較熟知的像Mythril、Oyente、Maian。還有一種就是，上個月他們剛剛公開的一個符號抽象分析的方法，也就是Securify。
下面主要分析一下Oyente以及Securify這兩種系統(tǒng)的一個具體的架構(gòu)以及實(shí)現(xiàn)方法。
Oyente符號執(zhí)行驗(yàn)證
Oyente的邏輯是在CFGbuild形成之后，首先是一個EXPLORER，EXPLORER的意思就是說我會把代碼當(dāng)中的每一個流程都去驗(yàn)證一遍，進(jìn)行一個之外的驗(yàn)證。
我們的驗(yàn)證就是是否有一個X，使得X不僅滿足C1、C2、C3三個條件，并且Z=X+2，那么這時候我們可以判斷他的狀態(tài)是no還是yes，然后以此來驗(yàn)證整個邏輯的一個流程。
到了第二個code analysis，這一部分其實(shí)是這個Oyente最為核心的一個部分，就是它將剛剛輸出的EXPLORSE這種路徑把它轉(zhuǎn)化，至始至終只包含Ether的一些路徑，進(jìn)行一些漏洞驗(yàn)證，而他目前只提供包括TOD、Timestamp dependence、Mishandled exceptions這三種驗(yàn)證，最后系統(tǒng)為了保證誤報(bào)率和漏報(bào)率，采用了微軟的Z3Bit-Vector Solver 開源的驗(yàn)證器，然后來進(jìn)行整體架構(gòu)的一個封裝。
在剛剛我們講述的過程當(dāng)中，其實(shí)大家也應(yīng)該了解到，在CFG轉(zhuǎn)EXPLORER驗(yàn)證的時候，我們需要對它的循環(huán)的每次都進(jìn)行一個驗(yàn)證，所以說這種分析方法特別耗時，并且也不一定成功。
比如說像parity的那個錢包代碼，它的Oyente覆蓋率僅僅達(dá)到20%，剩下80%的代碼，是沒有辦法去跟蹤的，所以這就是Oyente目前存在一個巨大的問題。
Securify符號抽象分析
在這個問題的基礎(chǔ)上，像Securify他們就提供了另外一種方法，它們認(rèn)為現(xiàn)在合約代碼其實(shí)是特別容易解耦合的，不像我們傳統(tǒng)的代碼一樣，它的耦合性特別高，但像合約代碼里面，就有transfer等等一些比較固定解耦合的一些結(jié)構(gòu)和模塊，我們并不是需要對整個合約的邏輯進(jìn)行的校驗(yàn)，可能我們就是對合約解耦合的各個模塊進(jìn)行校驗(yàn)分析，因此可以提高它的自動化程度。
這張圖也就是他們整個在驗(yàn)證的一個流程：
它們把contract bytecode轉(zhuǎn)化成一種他們自定義的一種語義語言，然后通過自定義的語義語言，它們之后有一個驗(yàn)證模塊，這個驗(yàn)證模塊就特別像我們之前說的那種模式匹配，就是把一些漏洞轉(zhuǎn)化成一種它驗(yàn)證語言的模式匹配的框架，然后去驗(yàn)證它這個語意在此是否滿足他這個比較，最終會生成一個安全報(bào)告。
這里也給出了一個parity的例子，通過自動化審計(jì)的方法，最終可以輸出錢包的owner其實(shí)是可以被修改的。
再具體一點(diǎn)，它是怎么做語義分析的呢？Securify分析這種合約代碼，是從兩個維度，第一個是邏輯，第二個是數(shù)據(jù)。
在邏輯方向的話，它定義了兩種邏輯，第一個叫MayFollow，第二叫MustFollow。MayFollow的意思是說L2是有一條路徑是跟在L1后面的，而MustFollow是說L2每一條路徑都跟在L1后面。這兩種區(qū)別定了它整個邏輯的一個框架。
第一個就是它的一個數(shù)據(jù)，它怎么定義合約里面的數(shù)據(jù)變化？分了三種，第一種是MayDepOn，就是兩個因素，一個叫Y、一個叫T，T變Y可能變也可能不變。
第二個就是Eq，就是說Y是由T來決定的
第三個就是大家把DetBy和Y和T是一一對應(yīng)的，只要T變Y就肯定要變了。
這里面就用更加形象的方法，我們想象一下，MayDepOn就是，變量是T，在一段時間當(dāng)中Y可能是一個值，然后有的說T變Y可能不變，第三個DetBy就是說一對一的關(guān)系，就比如說我們知道哈希，哈希如果T變，Y就肯定要變。
通過邏輯和數(shù)據(jù)這兩個維度進(jìn)行了一些驗(yàn)證，最終驗(yàn)證模塊的話，現(xiàn)在提供了大概六七個智能合約漏洞的驗(yàn)證性的語言，而且這種語言都是以插件化的形式來寫的，其他的安全開發(fā)者可以不斷去豐富這個漏洞的驗(yàn)證語言，最終我們在對自動化審計(jì)進(jìn)行一個評估的時候，我們其實(shí)是要從它的自動化程度，漏報(bào)率、誤報(bào)率來評估這件事情的。
像我們現(xiàn)在知道的一些數(shù)據(jù)就可以表明出來，其實(shí)像Mythril跟Oyente，它里面存在大量的誤報(bào)，比如說它檢測出來的數(shù)據(jù)還是需要人工進(jìn)行二次確認(rèn)，這個工作其實(shí)是非常繁瑣，而Securify這種方法可能誤報(bào)率會降低。
這也是兩種比較現(xiàn)在比較流行的符號執(zhí)行和抽象的自動化審計(jì)方法。
四、總結(jié)回顧
最后我們回顧一下，現(xiàn)在做的智能合約審計(jì)的話可能分為三種，：特征代碼匹配、形式化驗(yàn)證以及符號抽象。
回顧整個解釋的過程當(dāng)中，我們可以清楚地知道，現(xiàn)在自動化審計(jì)的方法其實(shí)是出于一個很不成熟的階段。
它們主要面臨三大問題：
第一個就是誤報(bào)率高，其實(shí)它并不能做到完全自動化，它還需要人工的一些參與。
第二個就是它的自動化其實(shí)程度比較低，還需要不斷有feedback去去審計(jì)。
第三就是審計(jì)時間比較長，比如說像Mythril，平均在60秒，Oyente大概在30秒，而Securify大概在20秒。
| 
