獵豹區塊鏈研究中心楊文玉:智能合約自動化審計存在誤報率高、自動...

編者按：本文來自36氪戰略合作區塊鏈媒體「Odaily星球日報」（公眾號ID：o-daily，APP 下載）。

區塊鏈這三個字近年經歷了幾番跌宕，從前沿的技術概念、風口上的熱詞，到被過度消費的符號。很多人相信，區塊鏈是解決許多行業痛點的工具，有潛力成為下一個世代「超級商業載體」誕生的催化劑。

然而，傳說中的史詩級變革還未來臨，它就已被置於聚光燈之下。有心者從中漁利，趨利者盲目買單。而過早陷入輿論漩渦，對成長期的技術是傷害，也是試煉。  

今天的實際情況是，落地應用寥寥無幾，技術和產業連接尚有距離，投機者的噪音蓋過了真正關注技術與行業的「中堅聲音」。Odaily星球日報聯合頂級新商業媒體36Kr、頂尖技術領袖和學界菁英，共同探討如何擁抱監管，推動行業去粗取精，將流量與話語權交給認真做事的人，用實力讓區塊鏈落地。

9 月 5 日，在由 Odaily星球日報主辦、36Kr 集團戰略協辦的 P.O.D 大會安全論壇上，獵豹區塊鏈研究中心安全專家楊文玉發表題為《智能合約自動化審計技術》的演講。

楊文玉開場介紹了智能合約發展的現狀。大部分人認為區塊鏈現在是一個寒冬時期，但是據獵豹區塊鏈研究中心統計，過去一個月中，智能合約每日新增數量為 1317 個。研究中心收錄的項目中，區塊鏈基礎設施佔 9.38%，遊戲和 VR 4.44%，商業和零售 3.6%，社交媒體與通訊 3.4%。

在數量穩定增長的同時，智能合約還面臨著安全問題。從 2017 年到 2018 年 6 月，智能合約漏洞頻繁爆發，帶來大量資金損失，也使得區塊鏈甚至智能合約的一些開發者或者用戶對智能合約的安全性產生質疑，也阻礙了以太坊之後的發展。

除此之外，Fomo3D 在興起的時候，僅僅在第二天就出現了大量的山寨合約。山寨 Fomo3D 遊戲開發者更改了積極分配的邏輯，導致投入的資金大部分都流向山寨合約開發者，也對 DApp 發展造成阻礙。

在這樣的背景下，如何有效保障海量智能合約的安全？楊文玉認為，最好的方法是降低人工審計複雜度，採用智能合約自動化審計。

具體來講，自動化審計方法主要分為三類：

• 第一種是特徵代碼匹配，就是對惡意代碼進行提取、抽象，形成匹配模塊對待檢測源碼進行檢測。優點是速度快、迅速響應新漏洞，缺點則是使用範圍有限、漏報率高。
  

• 第二種是基於形式化驗證的自動化審計方法。最早是在 2016 年由 Hirai 提供，Grishchenko 和 Hildenbrandt 之後進行了改進，採用 F*framework 和 K framework，將 EVM 轉化為一個 Formal  model。Formal 是航空航天領域常見的形式化驗證框架，而 K framework 則是一個語義的轉化框架。
  

• 最後一種是現在最常用的方法，基於符號執行和符號抽象自動化審計。分析智能合約時，通過編譯源碼，可以形成 EVM OPCODE，然後輸入到自動化分析引擎，轉化成 CFG，再利用這兩種方法進行分析。比較典型的是 Oyente 和 Securify 系統，可以降低誤報率和漏報率，但是分析方法繁瑣並且耗時。
  

不過，楊文玉也指出，現在自動化審計方法處於一個很不成熟的階段，主要面臨三大問題：誤報率高，自動化程度低、依賴人工二次審計，審計時間比較長。

以下為楊文玉演講全文，enjoy：

謝謝大家，今天非常榮幸來參加這個會議，今天我所帶來演講主題就是我們一起來淺析一下當下智能合約自動化安全檢測的技術，今天我的演講可能分兩位個部分，首先第一部分我們會一起來看一下現在以太坊上智能合約發展的現狀，第二部分基於這個現狀了解，再詳細描述一下現在智能合約自動化涉及的一些方法。

首先我們一起看一下現在智能合約發展的一個現狀，根據我們平臺，可以知道在過去一個月當中，智能合約的數量每天還在以 1317 個的平均增長率高度穩定地增長著，可能和我們所理解的區塊鏈現在是一個寒冬時期，所不太一樣這種增長率還比較穩定的。其次我們通過一些 NLT 方法，把智能合約領域劃分出來，除了一些敏感領域，現在智能合約比較多的應用在一些基礎設施，商業零售，遊戲以及社交媒體和通訊。這是一個智能合約大的現狀，智能合約現在面臨一個安全現狀是什麼樣的，可能剛才兩位嘉賓已經都進行了非常詳細的描述，從 2017 到 2018 年 6 月，這種智能合約漏洞頻繁爆發，每次都帶來大量資金損失，也使得區塊鏈甚至智能合約的一些開發者或者一些用戶對智能合約這種安全性產生一些高度的質疑，也阻礙了以太坊之後的發展。

除此之外，我們還可以看到像剛才嘉賓講到 Fomo3D 這件事情，除了基本智能合約安全，現在安全受到極大的關注，之前 Fomo3D 在興起的時候，僅僅在第二天就出現了大量的山寨合約，山寨的 Fomo3D，在這種遊戲當中，其實開發者更改了積極分配的邏輯，使得其實玩那個蜂窩遊戲過程當中，投入的資金大部分都是流向山寨合約開發者，也對 DApp 發展造成阻礙。

現在面臨一個問題是如何有效保障海量智能合約的安全，也是我們今天要討論的問題，也是第二部分想跟大家分享一個現在智能合約自動化審計技術的發展。

再回顧一下，現在智能合約截止到昨天中午 12 點，以太坊總共有 193 萬個合約，日增長率穩定增長，現在審計方法有人工審計，以及自動化審計。在海量智能合約當中，我們最好的方法就是降低人工審計複雜度，從而讓更多通過自動化審計進行。我們把自動化審計分為三個部分。首先第一種是特徵代碼匹配，第二類是基於形勢化驗證的子都化審計方法，最後一種是基於符號執行和符號抽象自動化審計。

首先看特徵代碼匹配，從名字可以很清晰理解到，就是對惡意代碼進行提取抽象，我們是一種語義匹配，匹配靜態原代碼，審計的方法優點是很顯而易見的，比如說速度很快，因為對源碼進行一個字符串匹配，第二個可以迅速進行新的漏洞，他審計出現一個新的漏洞，我們就可以快速提交一些新的匹配模式。他缺點在哪裡，再來看一下，我們所理解的現在區塊鏈都上應該是公開透明的，但實際情況並不是這樣，我們大概做了一個統計，目前代碼的開原率僅僅只佔 48.62%，就是說在以太坊上，其實有超過一半合約是不開源的，只暴露 code，剛剛那個嘉賓也說，他們也費了十分大的力氣去立項這個 code 這種限制就導致這種方法使用範圍有限，傳統的靜態審計方法比如說 App 檢測，會調用一個庫裡面確定唯一一些函數，對他進行審計，智能合約裡面一些函數一些特徵變化性比較多的，所以說漏洞率比較高。

第二個方法，我們就來探討一下現在比較火的，基於形式化驗證的自動化審計，形式化驗證審計智能合約安全，最早是在 2016 年由 Hirai 提供的，他提出了一點，他當時拿出邏輯交互證明器，通過 Isabelde  lem-Language->Formal-model，通過形式化 model 驗證，來判斷代碼邏輯是否存在問題，這項工作最後的兩個把形式化方面進行進一步改造，他們放棄 Lem-language 也是比較低效的轉化方式，他們採用了 F*framework 和 K framework，將 EVM 轉化為一個 Formal  model，而 Formal 可能就是經常在航空航天領域當中做一些形式化驗證的框架，而 K framework 則是一個語義的轉化框架，這兩個比較有代表性的技術研究，如果想更加深入了解可以參考下列的一些論文。

第三點就是今天想要著重跟大家交流，以及現在最常用的一些方法，就是基於符號執行和符號抽象的自動化審計，這種自動化審計現在看一下，我們在分析一個智能合約的時候，首先要明確分析對象是什麼，像我們剛才在解釋特徵匹配代碼當中，我們知道現在 EVM 上智能合約代碼大部分是不公開的，我們現在分析對象就確認應該是 EVM  OPCODE，在通過一些源碼，我們通過編譯，可以形成 EVM OPCODE，輸入到自動化分析引擎。在這種基於符號執行和符號抽象化自動化審計框架裡面，有些共有的特性，OPCODE 在輸入這個引擎當中，都會轉化成一個 CFG，就是一個一個控制流程圖，通過這個 CFG，可以簡單了解一下這個 CFG 是什麼意思，CFG 就是把合約代碼裡面邏輯包裝成哪個快，在裡面邏輯分叉的時候，左邊那個合約形成一個十分龐大完善的 CFD，讓程式設計師更好了解能夠執行一些邏輯。

在有 CFG 生成之後，現在就出現兩種分析方法，第一類就是基於符號執行的驗證，這類比較有代表性，大家都比較熟知像 Mythril、Oyente、Maian，還有一種就是上個月剛剛公開的一個符號抽象分析的方法，就是 Securify，今天主要跟大家講一下 Oyente 跟 Securify 這兩種系統具體的架構以及實現方法，首先我們來看 Oyente，Oyente 的邏輯我們可以從左邊看到，在 CFG 申請之後，首先是一個 explorer，會把代碼當中每一個流程驗證一邊，進行一個形式化驗證，就像這個我們驗證是我們是否有一個 X，使得 X 不僅滿足 C1、C2、C3 條件，這時候可以判斷狀態是 no 還是 yes，以此驗證整個邏輯的流程。第二個 core analysis 這一部分其實是 Oyente 最為核心的一個部分，將剛剛輸出的 explorer 這種路徑，把它轉化，只進行一些漏洞驗證，目前只提供包括 TOD 和 Timestamp  dependence 和 Mishandled exceptions，這三種驗證，最後這個系統又能保證誤報率和漏報率，他採用微軟的開源的驗證器，進行整體的架構封裝，在剛剛我們講述過程中，大家也應該了解到，在 CFG 轉 explorer 驗證的時候，我們是需要對他的循環，每次都是一個驗證，所以這種分析方法特別耗時，並且不一定成功。這就是 Oyente 目前存在一個巨大問題。

在這個問題基礎上，像 Securify，他們就提供了另外一種方法，他們認為現在合約的代碼其實是特別容易解耦合的，不像傳統代碼，耦合性特別高，像合約代碼這個一些比較固定形式化的解耦合模塊，我們並不是需要對整個合約邏輯進行一個交驗，我們對合約解耦各個模塊進行分析，以此提高自動化程度，左邊這個圖是整個驗證流程，把 contract bytecode 通過定義域語言之後有一個驗證模塊，特別像之前說的模式匹配，把一些漏洞轉化成驗證語言模式匹配框架，驗證這個語義是否磨合這個。最後也給出一個 report，通過這個自動化審計方法，最終可以輸出錢包的管理者是可以被修改的。

再具體一點是怎麼做語義分析，其實分析這種 explorer 代碼是從兩個維度，第一個是邏輯，第二個是數據，邏輯方式定義兩種邏輯，第一個叫做 MayFollow，第二個叫做 MustFollow，MayFollow 的意思就是說，L2 必須是有一條路徑跟在 L1 後面，而 MustFollow 是說 L2 每一條路徑都跟在 L1 後面，這兩種區別定義了整個邏輯的框架。

第二個是數據，怎麼定義合約裡面數據變化用了三種，第一個 MayDepOn，就是兩個因素，一個叫做 Y，一個叫 T，T 變 ，Y 可能變也可能不變。第二個是 Eq，就是 Y 是由 T 決定的。第三個是 DetBy，Y 和 T 是一一對應的，只要 T 變 Y 肯定要變了，這裡面用更加形象的方法來想像一下，其實 Maydepon 就像我們的 T 變量是 time，在一段時間中，Y 可能是一個值，T 變， Y 可能不變，第三個就是說一對一關係，就像我們算哈希，只要你 T 變，Y 肯定要變，通過邏輯和數據這兩個維度，他們進行一些驗證，最終驗證模塊現在提供了大概六、七個智能合約漏洞驗證性的語言，這種語言都是以插件化來寫的，其他的安全開發者可以在不斷豐富漏洞的驗證語言。

最終我們在對自動審計進行評估的時候，是從要自動化程度、漏報率、誤報率提供這件事情，我們現在知道數據就可以綁定出來，檢測出來數據還是需要人工進行二次確認，這個工作是十分繁瑣的，經過這種方法可以是誤報率會降低，這兩種符號執行和符號抽象的自動化審計方法。

最後回顧一下，現在自動化審計方法分為三種，特徵代碼匹配，形式化驗證以及符號執行、符號抽象。回顧整個淺析過程，我們可以清楚知道，現在自動化審計方法是在一個很不成熟的階段，主要面臨三大問題，第一個是誤報率高，並不能做到完全自動化，還需要人工參與。第二個是自動化程度比較低，還需要不斷去審計它，第三個審計時間比較長。

最後就是回顧一下我們整個分析，首先我們明晰一下智能合約發展現狀，又檢測自動化審計方法，左右各有我們技術交流群，有感興趣小朋友歡迎加入，可以一起更加深入的討論，這就是我今天所分享的內容，謝謝。