智能合約安全漏洞挖掘技術研究

付夢琳 吳禮發 洪 征 馮文博

摘 要：近年來，以智能合約為代表的第二代區塊鏈平臺及應用出現了爆發性的增長，但頻發的智能合約漏洞事件嚴重威脅著區塊鏈生態安全。針對當前主要依靠基于專家經驗的代碼審計效率低下的問題，提出開發通用的自動化工具來挖掘智能合約漏洞的重要性。首先，調研并分析了智能合約面臨的安全威脅問題，總結了代碼重入、訪問控制、整數溢出等10種出現頻率最高的智能合約漏洞類型和攻擊方式;其次，討論了主流的智能合約漏洞的檢測手段，并梳理了智能合約漏洞檢測的研究現狀;然后，通過實驗驗證了3種現有符號執行工具的檢測效果。對于單一漏洞類型，漏報率最高達0.48，誤報率最高達0.38。實驗結果表明，現有研究涵蓋的漏洞類型不完整，誤報及漏報多，并且依賴人工復核;最后，針對這些不足展望了未來研究方向，并提出一種符號執行輔助的模糊測試框架，能夠緩解模糊測試代碼覆蓋率不足和符號執行路徑爆炸問題，從而提高大中型規模智能合約的漏洞挖掘效率。

關鍵詞：區塊鏈安全;智能合約;以太坊;漏洞挖掘;自動化工具

Abstract： The second generation of blockchain represented by smart contract has experienced an explosive growth of its platforms and applications in recent years. However， frequent smart contract vulnerability incidents pose a serious risk to blockchain ecosystem security. Since code auditing based on expert experience is inefficient in smart contracts vulnerability mining， the significance of developing universal automated tools to mining smart contracts vulnerability was proposed. Firstly， the security threats faced by smart contracts were investigated and analyzed. Top 10 vulnerabilities， including code reentrancy， access control and integer overflow， as well as corresponding attack modes were summarized. Secondly， mainstream detection methods of smart contract vulnerabilities and related works were discussed. Thirdly， the performance of three existing tools based on symbolic execution were verified through experiments. For a single type of vulnerability， the highest false negative rate was 0.48 and the highest false positive rate was 0.38. The experimental results indicate that existing studies only support incomplete types of vulnerability with many false negatives and positives and depend on manual review. Finally， future research directions were forecasted aiming at these limitations， and a symbolic-execution-based fuzzy test framework was proposed. The framework can alleviate the problems of insufficient code coverage in fuzzy test and path explosion in symbolic execution， thus improving vulnerability mining efficiency for large and medium-sized smart contracts.

Key words： blockchain security; smart contract; Ethereum; vulnerability mining; automated tool

0 引言

區塊鏈技術已經成為目前金融業關注度最高的技術之一，經歷了以比特幣應用為代表的區塊鏈1.0時代，目前已經進入了以智能合約為標志的區塊鏈2.0時代。智能合約適應于區塊鏈分布式、去中心化的特點，具有獨立運行、不可篡改的優良特性，可用于實現包含金融工具在內的各類分布式應用。然而，智能合約無法避免地存在安全漏洞。從2016年The DAO（Decentralized Autonomous Organization）事件中360萬以太幣被盜，到2017年Parity錢包因多重簽名錢包合約漏洞導致上億美元資金被凍結，到2018年美鏈BEC（Beauty Chain）百億美金項目瞬時歸零、BAI（Blockchain of Artificial Intelligence and Internet of things）和EDU（EduCoin）任意賬戶轉賬，再到EOS（Enterprise Operation System）漏洞允許惡意合約穿透虛擬機從而危害礦工節點，智能合約儼然成為區塊鏈安全的重災區。當前尚沒有通用的自動化手段來驗證智能合約代碼是否包含漏洞，安全保障主要依靠開發者的技能水平以及基于專家經驗的代碼審計，這已無法滿足智能合約數量及規模不斷擴大、功能日益復雜、漏洞挖掘難度提升的新形勢下漏洞分析與發現的需求。本文對智能合約相關知識進行了系統的闡述，根據大量調研并結合其特性分析了當前智能合約面臨的安全威脅問題，從近年來發生的安全事件和代碼審計工作總結出智能合約漏洞的主要類型和攻擊方式。歸納了智能合約漏洞檢測手段及相關工作，通過對現有工具的實驗驗證與對比分析，討論目前工作存在的問題和挑戰，并針對這些不足提出未來研究的改進方法與建議。

1 智能合約概述

1.1 智能合約的概念

智能合約的誕生可以追溯到20世紀末，跨領域法律學者Nick Szabo提出智能合約的定義為：“一個智能合約是一套以數字形式定義的承諾，包括合約參與方可以在上面執行這些承諾的協議。”[1]他描述了自動售貨機在物理設定下，將產品直接給付過款的用戶的場景，認為可以使用計算機代碼代替機械設備來完成更為復雜的交易。然而當時缺少可信的執行環境，缺乏支持可編程合約的數字系統和技術，智能合約并未被應用于實際產業中。直到區塊鏈技術的興起使得該問題得以解決，區塊鏈不僅能夠支持可編程合約，并具有去中心化、不可篡改、過程透明、可追蹤等優勢，為智能合約提供了一個完美的解決信任問題的機制。2013年底，Vitalik Buterin發布的以太坊白皮書《以太坊：下一代智能合約和去中心化應用平臺》[2]將智能合約引入了區塊鏈，拓展了區塊鏈在貨幣領域之外的應用，引領了區塊鏈2.0時代的到來。如今，以太坊已成為最主流的智能合約開發和運行平臺。

簡而言之，智能合約是傳統合約的數字化版本，它是一種計算機程序，運行在區塊鏈數據庫上。智能合約程序代碼規定了合約條款，包含一些觸發條件，一旦滿足觸發條件合約便會自行執行。

表1從不同維度對智能合約與傳統合約進行比較，智能合約具備許多優勢：第一，智能合約不依賴中間人進行交易，例如金錢、股票、財產等具有一定價值的東西，無需第三方執行合約，大幅度縮減了成本;第二，消除了第三方供應商，用戶間得以直接進行交易，加速了合約驗證和執行的整個過程;第三，智能合約條款不可篡改的特性意味著它免于各種人為干預，降低了用戶受騙的風險;第四，智能合約存儲于分布式賬本，即每個聯網設備均存有一份合約副本，難以出現斷電、節點故障等問題。

首先，用戶注冊為區塊鏈的用戶，區塊鏈會返回用戶一個公私鑰對，公鑰作為用戶在區塊鏈上的賬戶地址，私鑰作為操作該賬戶的唯一鑰匙;然后由區塊鏈內的多個用戶共同商定一份承諾，以電子化的方式明確雙方的權利和義務，參與者分別用各自私鑰進行簽名以確保合約的有效性;最后，根據承諾內容將合約傳入區塊鏈網絡中。

2）智能合約的存儲。

合約通過P2P（Peer-to-Peer）的方式擴散到區塊鏈全網中的每個節點。接收到合約后，區塊鏈中的驗證節點將它保存至內存并等待新一輪的共識時間，觸發對該份合約的共識和處理。到達共識時間后，驗證節點將近一段時間內保存的所有合約打包成集合并計算其Hash值，并將這個合約集合的Hash值組裝成一個區塊結構，擴散到全網。其他驗證節點收到該區塊結構后，取出Hash值，對比自己保存的合約集合，并且向其他的驗證節點發送一份自己認可的合約集合。經過多輪發送和對比，在規定的時間內，所有的驗證節點最終對最新的合約集合達成一致。最新達成的合約集合通過區塊的形式擴散至全網，接收到合約集的節點對其逐條驗證，只有通過驗證的合約會被寫入區塊鏈，驗證的內容主要是合約參與者的私鑰簽名是否與賬戶匹配。

3）智能合約的執行。

智能合約定期對自動機狀態進行檢查，驗證滿足條件的事務，若達成共識則自動執行并通知用戶。

1.3 以太坊與智能合約

以太坊是第一個提供完善的智能合約開發框架的區塊鏈底層系統，提供了充足的應用程序編程接口（Application Programming Interface， API），支持迅速開發各種區塊鏈應用。微軟云服務上提供了智能合約工具箱，運行在于太坊區塊鏈，其平臺憑功能的多樣性和較高的智能合約執行能力獲得銀行業和互聯網金融行業的青睞，多家知名金融機構，如摩根大通、納斯達克、VISA等，都采用了以太坊的智能合約系統，目前開發在以太坊上的應用已有200多個。下文從賬戶模型、交易費用和以太坊虛擬機（Ethereum Virtual Machine， EVM）三個方面介紹以太坊的運行機制。

1.3.1 賬戶模型

以太坊的基礎單元是賬戶，以太坊區塊鏈上所有的狀態轉換皆為賬戶之間價值和信息的轉移。賬戶分為兩類，分別是由私鑰控制的外部賬戶（Externally Owned Account， EOA）以及由合約代碼控制的合約賬戶，它們共用同一個地址空間，每個賬戶都由一個長度為160位的地址來標識。外部賬戶不存儲代碼，但可以通過創建和使用私鑰簽署交易向其他外部賬戶或合約賬戶發送消息;而合約賬戶無法自動發起新的交易，只有接收到外部賬戶的消息，合約賬戶內部的代碼才會被激活，允許它執行轉移代幣、寫入內存、生成新的代幣、執行計算、創建新合約等操作。

1.3.2 交易費用

以太坊用戶必須為合約的執行向網絡支付適當的交易費用gas，使得以太坊區塊鏈免受無關緊要或惡意運算任務的干擾，例如無限循環和分布式拒絕服務（Distributed Denial of Service， DDoS）攻擊。發送方需要為每筆交易設置好gas的兩個部分，即gas limit和gas price。gas limit表示用戶愿意為某筆交易支付的最大gas量（至少為21000），gas price表示用戶承諾給每個gas單位的花銷，一般以gwei為單位，因此發送者愿意花費最多gas limit×gas price來執行這一交易。如果發送者賬戶余額中以太幣的數量大于此最大值，則可以進行交易。gas used表示執行實際花費的gas值總和，則實際支付的費用總額為gas used×gas price。交易結束時，如果仍有gas剩余，則將之返還給發送者;但若發送方未支付足夠的gas，導致gas被耗盡，則觸發out-of-gas異常，當前交易失敗，調用幀所做的所有狀態修改都會被回滾，且已支付的gas不會被返還。

1.3.3 以太坊虛擬機

Solidity是開發以太坊智能合約的主流語言，它的語法類似于JavaScript。類似于Java程序通過Java虛擬機（Java Virtual Machine， JVM）將代碼解釋成字節碼執行，以太坊智能合約經由以太坊虛擬機（EVM）解釋成為字節碼方可執行。換言之，EVM是被沙箱封裝起來、完全與外界隔離的以太坊智能合約運行環境，因此運行于EVM的所有智能合約都無法訪問托管虛擬機的計算機上運行的網絡架構、文件系統或其他進程。EVM是一個圖靈完備的虛擬機，能夠完成的計算量實際上受限于用戶提供的gas數量。

EVM基于堆棧架構，一切運算都在棧上進行，棧上的數值可能是指令需要取用的參數，也可能是被壓入棧的運算結果。堆棧的最大深度為1024，每個棧條目的大小為256位，意味著EVM是一個256位的機器。高級語言編寫的智能合約編譯成EVM字節碼后方可執行，EVM字節碼是一串十六進制數字編碼的字節數組。字節碼的解析以一個字節為單位，每個字節都表示一個EVM指令或一個操作數據。保留最小規模的EVM指令集合，從而盡量減少引起共識問題的錯誤實現。所有EVM指令操作都在256bit的基本數據類型上進行，具備常用的算術、位、邏輯和比較操作，也可以做到條件和無條件跳轉。

2 智能合約安全性問題

隨著智能合約數量的增多，去中心化應用（Decentralized Application， DApp）的推廣，智能合約涉及的數字資產呈指數級別增長。相比傳統軟件，智能合約的安全問題更加棘手，現實情況也更加嚴峻。

1）智能合約的可信度源自其不可篡改性，一旦被部署上線便無法修改。任何人都可對合約存在的安全漏洞發起攻擊，如果合約沒有相應的防御措施，便將無法遏止安全問題的惡化，從而嚴重損害合約本身的經濟價值以及公眾對項目的信任。

2）很多項目會公開智能合約源碼。源碼的公開透明雖能提升用戶對合約的信任度，卻也大幅度降低了黑客攻擊的成本，每一個暴露在開放網絡上的智能合約都有可能成為專業黑客團隊的金礦和攻擊目標。

3）智能合約的開發過程存在紕漏。由于起步晚，發展時間短，智能合約本身就有很多不足;同時市面上專業的技術人員嚴重匱乏，不嚴謹的代碼參考、拷貝和修改等人為因素都會引起漏洞。

NCC Group總結出智能合約中出現頻率最高的10類安全問題為分別：代碼重入、訪問控制、整數溢出、未嚴格判斷不安全函數調用返回值、拒絕服務（Denial of Service， DoS）、可預測的隨機處理、競爭條件/非法預先交易、時間戳依賴、短地址攻擊以及其他未知漏洞類型[4]。安比（SECurity of BITcoin， SECBIT）實驗室安全團隊深度掃描檢測了當前正在運行的23357個智能合約源代碼，通過智能合約安全審計模型掃描，實驗室安全專家發現其中大量合約代碼存在著不同程度的安全隱患。掃描結果顯示，這23357個智能合約源代碼中共有405882處不符合安全開發規范，平均每個合約有超過17個規范違反項。其中低級別（Low）的安全問題有26821個，主要集中在未指明版本號以及高gas消耗等問題;中級（Medium）安全問題有7202個，主要集中在整數溢出、除法、依賴時間戳、區塊哈希的運算;中高危（High）安全問題有572個，主要集中在代碼重入、短地址攻擊、強制轉賬、使用合約余額來做判斷、高地址臟數據、tx-origin的誤用上[5]。

下文將依據已發生的安全事件和已有的代碼審計工作，對部分智能合約漏洞類型及利用方式進行分析，并提出一些防范方法。

2.1 代碼重入

以太坊智能合約能夠調用和使用其他外部合約的代碼。合約也通常能夠處理以太幣，因此常常會把以太幣傳送到外部賬戶的地址。調用外部合約或將以太幣發送至某指定地址的操作要求合約提交一個外部調用，然而這些外部調用若是被攻擊者劫持，就會迫使合約進一步執行其他惡意代碼，包括回調自己，這就等同于代碼執行了重新進入合約的操作。The DAO事件即是重入攻擊的典型案例，可以采取多種方法規避潛在的重入漏洞：第一種是將以太幣發送至外部合約時，使用內置的transfer（）函數，該函數僅發送的2300個gas不足夠目的地址上的合約調用另一個合約;第二種方法是先保證所有改變狀態變量的邏輯發生后，再允許以太幣被從合約或任何外部調用發送出去;第三種方法是引入一個互斥系統，即添加一個代碼執行期間鎖定合約的狀態變量，從而防止重新入口的調用[6]。

2.2 權限控制問題

智能合約的權限控制問題大多是由于未能明確函數的可見性，或者未能作充足權限檢查，導致攻擊者能夠訪問或修改到不該訪問的函數或變量。Solidity為函數和狀態變量設置了external、public、internal和private四種可見性說明符，函數默認可見性為public，即對應函數既允許內部調用，也可以作為合約對外接口的一部分被外部合約調用訪問，因此，若轉賬等重要和敏感函數未能明確可見性，很可能導致合約中的資金流失。另外，智能合約中存在管理員Owner的概念，Owner一般擁有超級權限，而合約的初始化和Owner地址綁定則是由智能合約的構造函數實現的。一方面，如果構造函數聲明方式有誤，就會成為普通函數，任何人都可以調用，并將自己設為合約的管理員;另一方面，部分敏感函數需要onlyOwner權限，若未給該函數添加onlyOwner函數修飾器，則任何人能夠操縱該函數，破壞合約的執行邏輯。2017年11月，Parity錢包合約越權訪問漏洞被觸發，攻擊者通過調用錢包初始化函數，使自己成為walletlibrary的管理員，隨后以管理員身份調用kill函數，殺死walletlibrary，導致價值超過1.5億美元的以太幣被凍結。

規避權限控制漏洞的一般方法是，正確添加函數可見性說明符或修飾符來控制函數調用的范圍和權限，并對敏感操作作出嚴格的權限檢查。

2.3 整數溢出

以太坊虛擬機用幾種固定長度的數據類型表示整數。這意味著一個整數變量只可以表示一定范圍的數字。以變量類型uint8為例，其變量長度為8bit，支持存儲的數字范圍是[0，255]，若試圖將大小超過這個范圍的數據存儲到uint8中，虛擬機則自動截斷高位，導致運算結果異常。整數溢出包括加法溢出、減法溢出和乘法溢出三種類型。整數溢出漏洞屬于高危漏洞，若被攻擊者利用，很容易造成超額鑄幣、下溢增持、高賣低收等事故。已曝出的安全事件如SMT（SmartMesh Token）、BEC、EDU、BAI漏洞，都是由于轉賬邏輯中產生了整數溢出，導致代幣的無限增發或任意轉賬。防范整數溢出漏洞的一般方法是使用或構建數學庫來替代標準的數學運算符，OpenZeppelin[7]提供了有安全檢查的SafeMath數學計算庫，使用SafeMath庫函數進行開發能夠有效避免溢出漏洞。

2.4 異常處理問題

Solidity在執行到gas耗盡、調用棧溢出、執行到throw語句這幾種場景下會拋出異常，并通過回退狀態的方式來處理異常，即撤銷當前調用及其所有子調用所改變的狀態，同時給調用者返回一個錯誤標識。當子調用中發生異常時，異常通常會自動向上傳播;但是send以及底層調用函數call、delegatecall、callcode發生異常時，只是返回false，而不拋出異常，因此不能僅僅根據有無異常拋出判斷合約是否成功執行，在使用底層方法時，必須通過檢查返回值，對可能的異常進行處理。

2.5 短地址攻擊

短地址攻擊針對基于ERC20類型的代幣轉發問題。轉發代幣需要調用函數transfer（address addr， uint amount），addr表示發送代幣的目標地址，amount為發送代幣的數額。對于EVM層面，交易的消息輸入實際上是傳入了一串16進制字節碼，分為三部分，分別是4字節的方法名哈希值、32字節的目標以太坊地址以及32字節的代幣數額。假如賬戶地址addr以0結尾，而攻擊者故意少輸入末尾的0，EVM解析時就會從下一個參數，即代幣數額amount的高位取缺少的編碼位數對地址進行補全，而amount高位又恰好是0，這樣地址就會保持不變;然后，EVM對于amount參數從末位補0直至正常的編碼位數，這意味著將amount左移了數位，從而實現轉移超出實際應該轉發的token數。實踐中預防短地址攻擊的措施是對用戶輸入進行嚴格的檢測，避免接受畸形地址。

2.6 操縱區塊時間戳

有些智能合約的執行依賴于當前區塊的時間戳，時間戳直接或通過產生隨機數間接影響著執行的結果，但是這存在很多安全問題：一方面，時間戳由礦工打包交易時設置，礦工很可能利用自主權對時間戳作些微的改動;另一方面，以太坊未來有可能會對出塊時間上作出調整，因此通過塊高度來預估時間是存在不合理性[8]，因此，區塊時間戳不應該用于熵或產生隨機數，例如，它們不應成為贏得一場比賽或一個重要狀態轉移的決定性因素。

2.7 拒絕服務攻擊

針對智能合約的拒絕服務（DoS）攻擊本質是讓用戶在一小段時間內或在某些情況下永久性地無法使用合約，這可能會使合約中的以太幣（Ether）永遠無法提取出來。攻擊方法有三種[8]：第一種是通過（Unexpected）Revert發動DoS攻擊，在外部函數執行的結果決定著智能合約狀態的轉移而這個執行一直失敗的情況下，若不采取防護措施，則該智能合約可能會受到DoS攻擊。2016年以太坊游戲The King of the Ether Throne遭到的攻擊即為典型案例，DoS攻擊下退位君王的補償以及未接受款項均無法退回玩家的錢包。第二種是通過區塊gas limit發動DoS攻擊。以太坊給每個區塊能消耗的gas limit設定了上限，超過此上限交易便會失敗，即便沒有蓄意的攻擊也可能產生問題。然而，更糟糕的情況是如果攻擊者操控了gas的花銷，導致達到區塊gas limit的上限，整個轉賬的操作也會以失敗告終。第三種是所有者操作發動DoS攻擊。很多代幣合約的Owner賬戶擁有開啟或暫停交易的權限，若是沒有妥善保管Owner賬戶，代幣合約交易可能會被永久凍結，形成非主觀的拒絕服務攻擊。

2.8 偽隨機問題

Solidity無法創建隨機數，實際上，每個創建隨機數的算法都是偽隨機的，合約開發者編寫隨機數生成函數時，往往利用區塊號（block.number）、區塊時間戳（block.timestamp）、區塊難度（block.difficulty）和區塊gas限制（block.gaslimit）等區塊頭相關的參數或者其他區塊信息，如合約中存儲的數據來產生隨機數;但是，區塊頭參數可以被礦工獲知的特性和鏈上數據公開的問題，都導致生成的隨機數是可預測的，攻擊者可以利用這一點進行攻擊。

防范偽隨機問題的措施是，使得隨機數的來源不依賴于區塊參數，而是盡量從區塊鏈之外，例如Oraclize等第三方服務來獲取隨機數。

2.9 delegatecall委托調用

Solidity中提供了delegatecall函數，用于實現合約之間的相互調用以及交互，它的特點是調用后內置變量msg的值不會修改為調用者，但執行環境為調用者的運行環境，不當使用delegatecall會導致非預期代碼的執行。例如，若delegatecall的調用地址和調用的字符序列均由用戶傳入，則完全可以調用任意地址的函數。另外，由于delegatecall的執行環境為調用者環境，調用者與被調用者擁有相同變量的情況下，若被調用的函數修改該變量值，則修改的是調用者中的變量。Parity Multisig錢包的第二次攻擊就是delegatecall濫用的代表案例。防護措施是謹慎使用此類底層函數，對用戶輸入的調用發起地址及調用參數作出嚴格限定。

2.10 競爭條件/非法預先交易

用戶可以通過競爭代碼的執行，得到非預期的狀態。以太坊中，各節點把發生的交易匯集起來并形成區塊，一旦礦工解決了共識機制，就把這些交易認定為有效的。解決該區塊的礦工根據gas price，選擇把該礦池中的哪些交易記錄到該區塊中。這里就形成了一個潛在的攻擊面：攻擊者通過監視有可能包含問題解決方案的交易池，更改合約中對攻擊者不利的狀態或者修改攻擊者的權限。攻擊者于是能夠獲得此交易的數據，以更高的gas price創建自己的交易，并且將該交易包含在原始數據之前的區塊中，從而獲得優勢競爭條件得以預先交易。

3 智能合約漏洞檢測手段及相關工作

出于“代碼即規則”，智能合約一旦被部署便不可更改，即便有惡意交易被記錄下來，也不可以將其從區塊鏈中刪除。回滾交易的唯一方法是執行硬分叉，即通過修改區塊鏈中的共識協議把區塊鏈中的數據恢復到過去某一狀態，而這無法回避開發者客觀上存在濫用“專業壟斷”的質疑，一定程度上沖擊了區塊鏈系統去中心化的理念，所以必須在智能合約上線之前，對其進行全面深入的代碼安全審計與測試，充分分析潛在的安全威脅，盡可能規避漏洞。

針對智能合約安全問題，應該從開發人員使用安全庫進行開發、安全團隊開展合約測試、合約審計這三個角度采取措施。其中，合約測試指用大量的測試用例引導合約的執行，驗證其是否符合預期行為，但測試用例無法確保覆蓋所有可能的路徑，所以即便測試結果沒有發現問題，也不能排除漏洞存在的可能性。合約審計是安全團隊通過專業的手段，檢查出合約的代碼實現和業務邏輯中存在的漏洞和隱患，并向項目方提出業務邏輯上的指導和建議。這雖能發現大部分常見的漏洞和風險，但由于現有的審計工作在一定程度上依賴于審計人員的主觀判斷和經驗，無法根除安全風險和漏洞。借鑒傳統軟件漏洞檢測方法，可以采用以下幾種手段檢測智能合約漏洞。

3.1 形式化驗證

形式化驗證用邏輯語言對智能合約文檔和代碼進行形式化建模，通過嚴密的數學推理邏輯和證明，檢查智能合約的功能正確性和安全屬性[9]，克服了用傳統測試手段無法窮舉所有可能輸入的缺陷，能完全覆蓋代碼的運行期行為，可以確保在一定范圍內的絕對正確，彌補了合約測試和合約審計工作的局限性，因此形式化驗證已初步應用于高鐵、航天、核電等安全攸關的領域，并且取得了非常好的效果。另外，一些較為復雜的業務邏輯以及更高階的性質，例如經濟學、博弈論領域的問題，很難通過安全測試或審計手段得到有效驗證，所以對于規模較小但功能設計復雜的智能合約來說，形式化驗證必定是維護其安全性的有效方法之一。形式化驗證方法包括模型檢驗和定理證明兩種。模型檢驗是列舉出系統所有可能的狀態并逐一進行檢驗，這種方法全自動化卻只適用于小型系統;而定理證明首先把系統代碼提取成抽象的數學模型，然后對定理進行證明，這種方法能夠適應大規模系統，但需要首先將系統的運作方法轉換成驗證系統能夠理解的語言。成都鏈安科技研發的VaaS（Verification as a Service）[10]是全球首個同時支持EOS、以太坊區塊鏈智能合約的自動形式化驗證平臺，支持多種合約開發語言，可以對整型溢出、可重入攻擊、異常可達狀態、多簽名錢包、Tx.origin漏洞等10多種常規安全漏洞進行“一鍵式”自動化檢查。

由耶魯大學、哥倫比亞大學安全團隊研發的Certik[11]是一個形式化驗證框架，經過Certik驗證的智能合約、DApp以及區塊鏈會被附上證書形式的標志，來表示其正確性和安全性。Certik平臺的主要功能包括應用深度學習技術來構建智能標簽框架;通過層級分解將復雜的證明任務分解為更小的任務;可插拔的驗證引擎;認證的DApp庫等。

Bhargavan等[12]提出了一個智能合約分析和驗證框架，該框架通過Solidity*和EVM*工具將智能合約源碼和字節碼轉化成函數編程語言F*，以便分析和驗證合約運行時安全性和功能正確性。目前，Coq[13]、Isabelle/HOL[14]、Why3[15]等工具也實現了EVM的語義表示，并做了一些形式化驗證智能合約的工作。

3.2 模糊測試

模糊測試是一種通過構造非預期的輸入數據并監視目標軟件在運行過程中的異常結果來發現軟件故障的方法[16]。對智能合約進行模糊測試時，利用隨機引擎生成大量的隨機數據，構成可執行交易，參考測試結果的反饋，隨機引擎動態調整生成的數據，從而探索盡可能多的智能合約狀態空間。基于有限狀態機分析每一筆交易的狀態，檢測是否存在攻擊威脅。自動化工具Echidna[17]采用了模糊測試技術來對EVM字節碼進行檢測，但是不能保證API功能的穩定性。

文獻[18]中提出的ContractFuzzer是第一個基于Ethereum平臺的智能合約安全漏洞模糊測試框架，支持gas耗盡終止、異常處理混亂、重入、時間戳依賴、區塊號依賴、危險的delegatecall調用和以太幣凍結七種漏洞的檢測。ContractFuzzer包含離線EVM測試工具和在線模糊測試工具。構建了一個Web爬蟲，從Etherscan網站上獲得部署在以太坊上的智能合約，爬蟲可以提取合約創建代碼（智能合約的二進制文件）、應用程序二進制接口（Application Binary Interface， ABI）以及這些合約的構造函數參數。和其他智能合約漏洞檢測工具相比，ContractFuzzer支持更多的漏洞類型，有效降低了誤報率;但由于測試用例生成的隨機性，所能涵蓋的系統行為有限，無法達到理想的路徑覆蓋率，很難找出所有的潛在錯誤。

3.3 符號執行

符號執行的核心思想是使用符號值代替具體值執行程序。對于程序分析過程中任意不確定值的變量，包括環境變量和輸入等，都可以用符號值代替。符號執行中的“執行”是指解析程序可執行路徑上的指令，根據其語義更新程序執行狀態，等同于解釋執行[19]。借助符號執行檢測智能合約漏洞的一般過程為，首先將按需將智能合約中不確定值的變量符號化，然后逐條解釋執行程序中的指令，在解釋執行過程中更新執行狀態、搜集路徑約束，并在分支節點處做fork執行，以完成程序中所有可執行路徑的探索，發現安全問題。約束求解技術能夠對符號執行中搜集的路徑約束進行求解，判斷路徑是否可達，并在特定的程序點上檢測變量的取值是否符合程序安全的規定或者可能滿足漏洞存在的條件。

Luu等[20]開發了一種基于符號執行的靜態分析工具Oyente，可以直接運行在EVM字節碼上，而無需訪問Solidity或Serpent等高級語言。Oyente支持檢測交易順序依賴、時間戳依賴、代碼重入、錯誤處理異常等漏洞。Oyente覆蓋了大部分的EVM操作碼，但由于缺失類型、不同函數調用對相同字節碼的重用等上下文信息，僅從EVM字節碼很難重建開發意圖，因此Oyente無法驗證一些公平性和正確性問題（包括整數溢出等）。此外，Oyente簡化地處理循環，通過限制循環次數防止路徑爆炸，這導致了部分缺陷的漏報。

Manticore[21]是另一款基于符號執行且支持EVM的動態二進制分析工具，可以枚舉出合約的所有可到達執行狀態以及觸發這些路徑的輸出參數，并驗證關鍵功能的安全性，標記出整形數此處是否應該為整型？請明確溢出、未初始化內存等安全問題的類型。

上述工具都致力于檢測低級別的安全違規行為和漏洞，例如整數溢出、可重入和未處理的異常等，大多只對單個調用行為進行建模，均沒有對合同執行流進行推理。為解決此問題，Nikolic等開發了基于符號執行的MAIAN[22]工具，針對貪婪合約、浪子合約、自殺合約，精確定義這三類漏洞合約可核查的trace特性，著重分析對合約的調用序列，測試了近100萬個合約，以較快的速率發現大量真陽性漏洞。

Tsankov等開發了一種基于符號抽象的合約靜態分析工具Securify[23]，改進了市面上其他工具無法確切判定合約是否包含漏洞的缺陷，針對各安全屬性定義了遵從模式和違反模式兩種模式。Securify從合約的字節碼（或者源代碼，可以編譯為字節碼）開始，符號化地分析合約的依賴關系圖，提取出精確的語義事實，并使用這些事實匹配遵從和違反模式。根據檢查結果，Securify將所有合約行為分為違規、警告和遵從三類，所有與違規模式匹配的行為報告為違規，所有與遵從模式匹配的報告為遵從，其他行為報告為警告，因此，用戶需要手動分類為真陽性或假陽性的行為只有警告行為（標記為warning），減少了大約65.9%的工作量。

Johannes Krupp等開發的TEETHER[24]工具，在僅提供EVM字節碼的情況下支持智能合約的自動漏洞識別和漏洞利用。TEETHER的工作流程為：首先根據EVM字節碼，使用反向切片迭代地重建控制流圖（Control Flow Graph， CFG）;其次尋找關鍵指令，共有四條，要從合約中提取以太幣必須至少執行其中一條，CALL和SELFDESTRUCT能夠導致以太幣的直接傳輸，CALLCODE和DELEGATECALL指令允許在合約的上下文中執行任意EVM字節碼;接著對于提取出的每條關鍵指令，根據其關鍵參數計算后向程序切片，隨后使用A*算法探索路徑，其中路徑的成本定義為該路徑在CFG中遍歷的分支數;一旦生成關鍵路徑，路徑約束生成模塊就以符號方式執行路徑，收集一組路徑約束;根據約束求解結果，推斷出導致智能合約利用的事務列表。相比其他工具，TEETHER不僅實現了漏洞檢測，還實現了漏洞的自動利用，但其局限性在于只支持檢測單個合約內的漏洞，而不能發現調用其他合約產生的漏洞。

3.4 污點分析

本質上來說，污點分析是針對污點變量的數據流分析技術。污點分析的一般流程為：首先識別污點信息在智能合約中的產生點并對其進行標記;然后按照實際需求和污點傳播規則進行前向或后向數據依賴分析，得到污點的數據依賴和被依賴關系的指令集合;最終在一些關鍵的程序點檢查關鍵的操作是否會受到污點信息的影響。Bernhard Muller研發了一種全新的智能合約安全分析工具Mythril[25]，Mythril集成了混合符號執行、污點分析和控制流檢查，可以檢測出整數溢出、不可信合約的外部調用等一系列的常見安全問題;但它無法檢測出智能合約的業務邏輯問題，且極易產生誤報。

4 總結與展望

4.1 現有研究的不足

如前所述，近年來雖出現了一些智能合約漏洞自動化檢測工具，但都存在一定的缺陷，主要體現在以下幾個方面。

1）各工具涵蓋的漏洞類型不完整，總結部分現有工具支持的漏洞類型如表2所示。

可以看出，各工具檢測手段單一，涵蓋的漏洞類型不完整，它們大多只能檢測低級別的安全違規行為和漏洞，缺乏對合約執行流的推理，難以發現不同合約間調用產生的安全問題，且無法有效檢測公平性等邏輯缺陷，因此，使用單個工具對合約進行更全面的安全驗證是一個待解決的技術難題。

2）代碼覆蓋率低，漏報率和誤報率高。本文選取了150個智能合約Solidity源碼樣本，就交易順序依賴（Transaction-Ordering Dependence， TOD）、代碼重入（Reentrancy）、未處理的異常（Mishandled Exception）三種漏洞類型，對Securify、Oyente和Mythril三種工具的檢測效果進行對比，結果如表3所示。其中，TW（True Warning）、FW（False Warning）和UV（Unreported Vulnerability）分別表示正確警告、錯誤警告和未報告的漏洞占樣本總數的比例。

3）現有研究工作大多不能做到完全自動化，無法明確報告合約行為是否違規，對于檢測出來的所有疑似漏洞，需要用戶手動將其分類為真陽性或假陽性，這大幅度增加了智能合約安全檢測的工作量，因此，下一步研究需要對于挖掘出的疑似漏洞，使用工具直接驗證其是否能實際造成安全威脅，減少人工驗證環節工作量，并盡可能地提供漏洞利用方案，提出漏洞修補措施和智能合約安全編程建議。

4）審計時間較長，漏洞挖掘效率低下。對于每個合約的檢測時間，Mythril平均花費60s，Oyente大約為30s，而Securify大約為20s。面對數目和規模與日俱增的智能合約，提高漏洞發現效率也是亟需解決的重難點。

4.2 未來研究方向與改進思路

1）擴展形式化驗證的應用范圍。

對于目前學術界頗為關注的形式化驗證方法，用數學推演來驗證復雜系統，安全有效但難度很高。未來的研究應針對不同的業務目標定制對應的驗證規范描述，突破成本昂貴、不適應大規模合約等技術限制，并擴展形式化驗證的應用范圍，從驗證一般功能屬性和安全屬性、檢測常見漏洞到逐步實現經濟學、博弈論范疇中復雜業務邏輯及公平性等高階性質的證明。

2）提取重點路徑，縮減路徑空間。

基于攻擊者目標是非法竊取加密貨幣的假設，結合現有智能合約審計經驗和已曝漏洞分析，尋找智能合約中易產生漏洞的高危指令，如SUICIDE、CALL、ORIGIN、ASSERT_FAIL等，定義涉及這些操作碼的路徑為重點路徑。為了提高漏洞挖掘效率，實踐中不必對所有可能的執行路徑進行檢查，僅符號執行關注的重點路徑并進行漏洞驗證，可以有效地縮減路徑空間。

3）符號執行輔助的模糊測試。

現有的工具通常是對一種典型方法的具體實現，但是在執行具體漏洞挖掘任務時，因需求和重點不同，使用不同的輔助工具或者不同的檢測方法組合往往能達到更好的效果，可以考慮符號執行輔助的模糊測試方法：一方面，對于已有的智能合約模糊測試工具Echidna和ContractFuzzer，雖簡單有效，執行效率高，適合發現隱藏的未知漏洞，但局限性在于隨機性強，生成的測試用例的質量影響著代碼覆蓋率，難以對合約進行全面的測試，并且缺乏對智能合約語義的洞察力，很難發現多階段安全漏洞、多點觸發漏洞、訪問控制漏洞、糟糕的邏輯設計等。另一方面，對于已有的基于符號執行的工具，如Oyente和Manticore，在處理智能合約中較多的不定常數組時，或是合約規模龐大、跳轉指令較多時，容易產生路徑爆炸，導致測試效率不高。

因此未來可以研究動態符號執行輔助的模糊測試技術，使用動態符號執行彌補模糊測試理解語義的缺失，推斷出到達特定程序狀態的約束條件，通過約束求解產生能夠觸發測試者所關注邏輯的合理輸入。據此恰當地改變模糊測試的輸入，提供額外的測試用例，觸發先前未覆蓋的代碼區域，因此本文設計一種符號執行輔助的智能合約模糊測試框架，如圖1所示。

框架采用模糊測試作為前端處理，利用種子測試用例來驅動被檢測智能合約的執行;采用EVM字節碼覆蓋率監測處理作為中間層處理，其中在被測試程序的執行過程中，記錄被測試合約覆蓋的基本塊，由此計算模糊測試的覆蓋率;在符號執行處理中生成重點關注代碼區域的新測試用例，然后將新的測試用例反饋至模糊測試，使得模糊測試利用新的測試用例來驅動被測試合約的執行。這樣既能融合模糊測試快速高效、低消耗的優勢與符號執行探索能力強的優勢，又克服了模糊測試代碼覆蓋率不足和符號執行路徑爆炸的缺陷，可以有效提高大中型規模智能合約的漏洞分析與驗證效率。

4）完善智能合約漏洞庫，建立漏洞挖掘工具效率評價方法。

當前關于智能合約的測試尚未有標準的案例集，因此，為了驗證智能合約漏洞挖掘工具的有效性，同時給智能合約的安全開發提供參考，下一步工作需要根據已爆發的安全事件以及合約審計經驗，總結歸納出涵蓋類型完善的智能合約漏洞庫。綜合考慮漏報率、誤報率、檢測時間、支持漏洞類型和漏洞的危害等級等因素，建立漏洞挖掘工具效率的綜合評價指標，將市面上的相關工具進行對比分析，驗證其有效性，并為新工具的研發和改進提供指導。

5 結語

智能合約極大地擴展了區塊鏈的應用場景與現實意義，但頻發的安全事故嚴重阻礙了它的發展。本文梳理了智能合約面臨的安全問題，討論了形式化驗證、模糊測試和符號執行等主流的智能合約漏洞檢測手段，通過對幾個現有漏洞挖掘工具的驗證分析發現，當前研究主要存在涵蓋的漏洞類型不完整、誤報及漏報率高、檢測效率低下、依賴人工復核等缺陷，并針對相關工作中存在的不足，提出幾點未來研究方向。下一步工作的重難點在于采用不同的檢測方法組合，著力提高漏洞挖掘的準確性、效率和自動化程度，滿足智能合約規模和復雜度與日俱增的漏洞挖掘需求。

參考文獻 （References）

[1] 馬昂，潘曉，吳雷，等.區塊鏈技術基礎及應用研究綜述[J].信息安全研究，2017，3（11）：968-983.（MA A， PAN X， WU L， et al. A survey of the basic technology and application of block chain[J]. Journal of Information Security Research， 2017， 3（11）： 968-983.）

[2] BUTERIN V. Ethereum： a next-generation smart contract and decentralized application platform [EB/OL]. （2014-01-23） [2018-09-08]. https：//bitcoinmagazine.com/articles/ethereum-next-generation-cryptocurrency-decentralized-application-platform-1390528211/.

[3] 長鋏，韓鋒，楊濤.區塊鏈：從數字貨幣到信用社會[M].北京：中信出版社，2016：62-73.（CHANG J， HAN F， YANG T. Blockchain： From Digital Currency to Credit Society[M]. Beijing： China CITIC Press， 2016： 62-73.）

[4] NCC Group. Decentralized application security project top 10 of 2018 [EB/OL]. （2018-07-08） [2018-09-08]. https：//www.dasp.co/index. html.

[5] SECBIT. Frequent smart contracts events， security development requires standardization [EB/OL]. （2018-05-07） [2018-10-20]. https：//www.jianshu.com/p/9d78f5110af1.

[6] MANNING A. Solidity security： comprehensive list of known attack vectors and common anti-patterns [EB/OL]. （2018-05-30） [2019-01-03]. https：//blog.sigmapri-me.io/solidity-security.html.

[7] ARIAS L， SPAGNUOLO F， GIORDANO F， et al. OpenZeppelin [EB/OL]. （2016-07-31）[2018-12-06]. https：//github.com/ OpenZeppelin/openzeppelin-Solidity.

[8] ATZEI N， BARTOLETTI M， CIMOLI T. A survey of attacks on Ethereum smart contracts （SoK） [C]// Proceedings of the 2017 International Conference on Principles of Security and Trust. Berlin： Springer， 2017： 164-186.

[9] FEY G. Assessing system vulnerability using formal verification techniques[C]// Proceedings of the 2011 International Conference on Mathematical and Engineering Methods in Computer Science. Berlin： Springer， 2011： 47-56.

[10] CSDN Research and Development Technology. Formal verification is a sharp weapon for smart contracts safety [EB/OL]. （2018-06-12） [2018-09-08]. https：//blog.csdn.net /CDLianan/article/details/80665163.

[11] Certik.用形式化驗證的方式構建安全的智能合約和區塊鏈生態系統[EB/OL].（2018-07-11）[2019-01-06]. https：//baijiahao.baidu.com/s？id=1605131670683321304&wfr=spider&for=pc.（Certik： Constructing secure smart contract and block chain ecosystem by formal verification [EB/OL]. （2018-07-11）[2019-01-06].https：//baijiahao.baidu.com/s？id=1605131670683321304&wfr=spider&for=pc.）

[12] BHARGAVAN K， SWAMY N， ZANELLA B S， et al. Formal verification of smart contracts： short paper[C]// Proceedings of the 2016 Association for Computing Machinery Workshop. New York： ACM， 2016： 91-96.

[13] YANG X， YANG Z， SUN H Y， et al. Formal verification for Ethereum smart contract using Coq[J]. International Journal of Information and Communication Engineering， 2018， 12（6）： 125-130.

[14] HIRAI Y. pirapira/eth-isabelle [EB/OL]. （2016-04-24）[2018-12-18]. https：//github.com/pirapira/eth-isabelle.

[15] MARCHE C， MELQUIOND G， FILLIATRE J C， et al. AdaCore/why3 [EB/OL]. （2009-11-29） [2018-12-18]. https：//github. com/AdaCore/why3.

[16] BEKRAR S， BEKRAR C， GROZ R， et al. Finding software vulnerabilities by smart fuzzing [C]// Proceedings of the 4th International Conference on Software Testing， Verification and Validation. Piscataway， NJ： IEEE， 2011： 427-430.

[17] SMITH J P， PEREZ B， CHRISTIE C， et al. Trailofbits/echidna [EB/OL].（2018-06-12）[2018-09-08]. https：//github.com/trailofbits/echidna.

[18] JIANG B， LI Y， CHAN W K. ContractFuzzer： fuzzing smart contracts for vulnerability detection[C]// Proceedings of the 33rd IEEE/ACM International Conference on Automated Software Engineering. New York： ASE， 2018： 259-268.

[19] 吳世忠，郭濤，董國偉.軟件漏洞分析技術[M].北京：科學出版社，2014：215-268.（WU S Z， GUO T， DONG G W. Software Vulnerability Analysis Technology[M]. Beijing： Science Press， 2014： 215-268.）

[20] LUU L， CHU D H， OLICKEL H， et al. Making smart contracts smarter[C]// Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. New York： ACM， 2016： 254-269.

[21] MOSSBERG M， IVNITSKIY Y， SMITH J P， et al. trailofbits/manticore [EB/OL]. （2017-02-12） [2018-09-08]. https：//github.com/trailofbits/manticore.

[22] NIKOLIC I， KOLLURI A， SERGEY I， et al. Finding the greedy， prodigal， and suicidal contracts at scale [EB/OL]. （2018-02-06） [2018-11-14]. https：//arxiv.org/pdf/1802.06038.pdf.

[23] TSANKOV P， DAN A， COHEN D D. Securify： practical security analysis of smart contracts[C]// Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. New York： ACM， 2018： 67-82.

[24] KRUPP J， ROSSOW C. teEther： gnawing at Ethereum to automatically exploit smart contracts[C]// Proceedings of the 27th USENIX Security Symposium. Berkeley， CA： USENIX Association， 2018： 1317-1333.

[25] MUELLER B， HONIG J， PARASARAM N， et al. ConsenSys/mythril [EB/OL]. （2017-09-17） [2018-12-04]. https：//github. com/ConsenSys/mythril.