智能合約安全漏洞挖掘技術(shù)研究

付夢琳 吳禮發(fā) 洪 征 馮文博

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

關(guān)鍵詞：區(qū)塊鏈安全;智能合約;以太坊;漏洞挖掘;自動化工具

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 引言

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

1 智能合約概述

1.1 智能合約的概念

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

簡而言之，智能合約是傳統(tǒng)合約的數(shù)字化版本，它是一種計算機程序，運行在區(qū)塊鏈數(shù)據(jù)庫上。智能合約程序代碼規(guī)定了合約條款，包含一些觸發(fā)條件，一旦滿足觸發(fā)條件合約便會自行執(zhí)行。

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

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

2）智能合約的存儲。

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

3）智能合約的執(zhí)行。

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

1.3 以太坊與智能合約

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

1.3.1 賬戶模型

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

1.3.2 交易費用

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

1.3.3 以太坊虛擬機

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

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

2 智能合約安全性問題

隨著智能合約數(shù)量的增多，去中心化應(yīng)用（Decentralized Application， DApp）的推廣，智能合約涉及的數(shù)字資產(chǎn)呈指數(shù)級別增長。相比傳統(tǒng)軟件，智能合約的安全問題更加棘手，現(xiàn)實情況也更加嚴(yán)峻。

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

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

3）智能合約的開發(fā)過程存在紕漏。由于起步晚，發(fā)展時間短，智能合約本身就有很多不足;同時市面上專業(yè)的技術(shù)人員嚴(yán)重匱乏，不嚴(yán)謹(jǐn)?shù)拇a參考、拷貝和修改等人為因素都會引起漏洞。

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

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

2.1 代碼重入

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

2.2 權(quán)限控制問題

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

規(guī)避權(quán)限控制漏洞的一般方法是，正確添加函數(shù)可見性說明符或修飾符來控制函數(shù)調(diào)用的范圍和權(quán)限，并對敏感操作作出嚴(yán)格的權(quán)限檢查。

2.3 整數(shù)溢出

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

2.4 異常處理問題

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

2.5 短地址攻擊

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

2.6 操縱區(qū)塊時間戳

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

2.7 拒絕服務(wù)攻擊

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

2.8 偽隨機問題

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

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

2.9 delegatecall委托調(diào)用

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

2.10 競爭條件/非法預(yù)先交易

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

3 智能合約漏洞檢測手段及相關(guān)工作

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

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

3.1 形式化驗證

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

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

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

3.2 模糊測試

模糊測試是一種通過構(gòu)造非預(yù)期的輸入數(shù)據(jù)并監(jiān)視目標(biāo)軟件在運行過程中的異常結(jié)果來發(fā)現(xiàn)軟件故障的方法[16]。對智能合約進行模糊測試時，利用隨機引擎生成大量的隨機數(shù)據(jù)，構(gòu)成可執(zhí)行交易，參考測試結(jié)果的反饋，隨機引擎動態(tài)調(diào)整生成的數(shù)據(jù)，從而探索盡可能多的智能合約狀態(tài)空間?；谟邢逘顟B(tài)機分析每一筆交易的狀態(tài)，檢測是否存在攻擊威脅。自動化工具Echidna[17]采用了模糊測試技術(shù)來對EVM字節(jié)碼進行檢測，但是不能保證API功能的穩(wěn)定性。

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

3.3 符號執(zhí)行

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

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

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

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

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

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

3.4 污點分析

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

4 總結(jié)與展望

4.1 現(xiàn)有研究的不足

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

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

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

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

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

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

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

1）擴展形式化驗證的應(yīng)用范圍。

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

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

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

3）符號執(zhí)行輔助的模糊測試。

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

因此未來可以研究動態(tài)符號執(zhí)行輔助的模糊測試技術(shù)，使用動態(tài)符號執(zhí)行彌補模糊測試?yán)斫庹Z義的缺失，推斷出到達特定程序狀態(tài)的約束條件，通過約束求解產(chǎn)生能夠觸發(fā)測試者所關(guān)注邏輯的合理輸入。據(jù)此恰當(dāng)?shù)馗淖兡：郎y試的輸入，提供額外的測試用例，觸發(fā)先前未覆蓋的代碼區(qū)域，因此本文設(shè)計一種符號執(zhí)行輔助的智能合約模糊測試框架，如圖1所示。

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

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

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

5 結(jié)語

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

參考文獻 （References）

[1] 馬昂，潘曉，吳雷，等.區(qū)塊鏈技術(shù)基礎(chǔ)及應(yīng)用研究綜述[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] 長鋏，韓鋒，楊濤.區(qū)塊鏈：從數(shù)字貨幣到信用社會[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.用形式化驗證的方式構(gòu)建安全的智能合約和區(qū)塊鏈生態(tài)系統(tǒng)[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] 吳世忠，郭濤，董國偉.軟件漏洞分析技術(shù)[M].北京：科學(xué)出版社，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.