基于形式化方法的智能合約驗證研究綜述

張文博，陳思敏，魏立斐，宋巍，黃冬梅

基于形式化方法的智能合約驗證研究綜述

張文博1,2，陳思敏1，魏立斐1，宋巍1，黃冬梅3

（1. 上海海洋大學(xué)信息學(xué)院，上海 201306；2. 上海市高可信計算重點實驗室，上海 200062；3. 上海電力大學(xué)，上海 201306）

智能合約是區(qū)塊鏈技術(shù)應(yīng)用的一個重要場景，智能合約技術(shù)實現(xiàn)了區(qū)塊鏈的可編程化，提高了其擴展性，有廣闊的應(yīng)用前景。然而，一系列關(guān)于智能合約的安全事件造成了大量經(jīng)濟損失，削弱了人們的信心，安全性問題已經(jīng)成為制約智能合約進一步發(fā)展的關(guān)鍵問題。如果合約設(shè)計和代碼實現(xiàn)的過程中存在缺陷，可能會造成嚴重后果。而智能合約發(fā)布后無法修改，因此，在智能合約發(fā)布前對其正確性做出驗證尤為重要。近年來，國內(nèi)外學(xué)者在智能合約的驗證領(lǐng)域取得了大量成果，但對這些研究成果的系統(tǒng)分析和總結(jié)相對較少。對以太坊的交易過程、gas機制、存儲結(jié)構(gòu)、編寫語言做了簡要介紹，在此基礎(chǔ)上調(diào)查歸納了智能合約中常見的8種漏洞類型，解釋了漏洞產(chǎn)生的原因，回顧了一些真實發(fā)生的安全事件并給出了漏洞示例代碼；根據(jù)不同的技術(shù)手段，如符號執(zhí)行、模型檢測、定理證明等，對智能合約的形式化驗證工作做分類介紹，分析了各種方法的優(yōu)劣，并選取了3個開源的自動化驗證工具Mythril、Slither和Oyente，從運行效率、檢測漏洞類型以及準(zhǔn)確率等方面作出實驗評估和對比；研究了目前已有的相關(guān)綜述文章，總結(jié)了這些研究的區(qū)別與優(yōu)勢；概述了智能合約的漏洞檢測技術(shù)中仍存在的關(guān)鍵問題，對智能合約驗證工作的現(xiàn)狀進行了分析和展望，提出了未來能夠進一步研究的方向。

智能合約；形式化方法；區(qū)塊鏈；以太坊；程序驗證

0 引言

2008年，中本聰在其發(fā)表的文章中第一次闡述了區(qū)塊鏈技術(shù)[1]。早期的區(qū)塊鏈平臺只能實現(xiàn)數(shù)字貨幣的簡單交易，但區(qū)塊鏈技術(shù)的去中心化、匿名性、不易篡改性等優(yōu)勢[2]，以及在長期實踐中表現(xiàn)出的安全性和穩(wěn)定性，使越來越多的研究者開始探索區(qū)塊鏈技術(shù)更廣闊的應(yīng)用場景。智能合約便是較為成功的一個應(yīng)用場景。智能合約的概念最早由密碼學(xué)家Szabo[3]提出，是指以數(shù)字形式存儲的，可以自動執(zhí)行合約條款的計算機交易協(xié)議。區(qū)塊鏈技術(shù)[1]為智能合約的實現(xiàn)提供了解決方案：將智能合約的代碼寫入?yún)^(qū)塊鏈中，自動按照代碼內(nèi)容執(zhí)行合約條款，并為智能合約提供去中心化分布式的存儲介質(zhì)，保證智能合約代碼的不易篡改性。同時，智能合約為區(qū)塊鏈提供更豐富的業(yè)務(wù)場景。以太坊是第一個大規(guī)模應(yīng)用智能合約功能的區(qū)塊鏈平臺[2]，目前已經(jīng)成為僅次于比特幣的第二大區(qū)塊鏈交易平臺。

智能合約在金融[4]、醫(yī)療[5-6]、物聯(lián)網(wǎng)[7]、政府管理[8]、能源[9]、供應(yīng)鏈管理[10]等領(lǐng)域都顯示出了廣闊的應(yīng)用前景，但伴隨的安全問題層出不窮[11]。攻擊者能夠利用合約代碼中的漏洞獲取較大的經(jīng)濟利益。2016年6月，眾籌項目The DAO合約代碼中的重入漏洞被攻擊者利用，竊取了價值約4 000萬美元的以太幣[12]。此次事件造成了深遠影響，以太坊社區(qū)關(guān)于解決方案的分歧，導(dǎo)致了以太坊的硬分叉，并且引發(fā)了關(guān)于智能合約安全性的信任危機。2017年7月，多重簽名錢包項目Parity中價值數(shù)千萬美元的以太幣被竊取[13]。同年11月，Parity錢包中價值上億美元的以太幣被凍結(jié)[14]。以上多次漏洞事件表明，對智能合約的正確性做嚴格的驗證是十分必要的。

形式化驗證基于嚴格的數(shù)學(xué)基礎(chǔ)，驗證軟件系統(tǒng)和硬件系統(tǒng)滿足特定的安全性質(zhì)，在航空航天、核電、高鐵動車等安全攸關(guān)的領(lǐng)域中有難以取代的價值[15]。由于智能合約代碼上鏈后無法修改，出現(xiàn)漏洞則可能帶來重大損失，因此在代碼上鏈前做安全性驗證十分必要。合約代碼通常體量較小，能夠避免形式化方法在處理大規(guī)模程序時的效率短板。因此，形式化方法非常適合于解決智能合約的安全問題。

近年來，基于形式化方法的智能合約驗證研究取得了大量研究成果。在IEEE、ACM、Springer、Elsevier等論文數(shù)據(jù)庫中以“smart contract”“blockchain”“formal verification”等關(guān)鍵詞的組合進行檢索后，本文從中篩選出了較為重要的文章，并對這些研究成果做出系統(tǒng)的分析和總結(jié)。

1　以太坊概述

本節(jié)將介紹與以太坊相關(guān)的一些背景知識，這些知識是理解后文中智能合約漏洞產(chǎn)生原因的重要基礎(chǔ)，對于以太坊中基本概念的更全面的介紹可參考文獻[2]。

1.1　以太坊簡介

2013年，Buterin在以太坊白皮書[2]中描述了一個智能合約和去中心化的應(yīng)用平臺。以太坊已經(jīng)成為規(guī)模最大的、面向用戶的智能合約開發(fā)平臺，也是市值僅次于比特幣的區(qū)塊鏈交易平臺[16]。以太坊的發(fā)展經(jīng)歷了4個階段，包括Frontier（2015年）、Homestead（2016年）、Metropolis（2017—2019年）和Serenity（2020年至今）。

相較于比特幣系統(tǒng)，以太坊平臺不僅借助區(qū)塊鏈技術(shù)來維護去中心化支付，并且支持用戶編寫智能合約以完成復(fù)雜的合約邏輯。智能合約是運行在區(qū)塊鏈上的一段程序代碼[3]，可在去中心化的環(huán)境中執(zhí)行。任何用戶都可編寫智能合約，并將智能合約部署到區(qū)塊鏈上[17]，這一過程是不可逆的，用戶可以通過外部賬戶調(diào)用合約中的函數(shù)，實現(xiàn)與以太坊的交互。智能合約可以通過向其他合約發(fā)送消息或調(diào)用函數(shù)來完成交易，全網(wǎng)節(jié)點交易驗證通過后，將狀態(tài)改動記錄在區(qū)塊中。

1.2 以太坊的交易

以太坊中包含兩類賬戶：外部賬戶（EOA，externally owned accounts）與合約賬戶（CA，contracts accounts）[2]。EOA即用戶賬戶，由公?私鑰對控制，公鑰經(jīng)過哈希運算后可得到外部賬戶的地址。CA由智能合約控制，除了包括160位的地址信息和以太幣余額信息外，還包括一段可執(zhí)行的代碼和一部分私有的存儲空間[3]。合約賬戶無法主動發(fā)起交易，但可通過合約之間的調(diào)用完成合約功能[17]。以太坊中兩種交易的方式如圖1所示。第一種是采用創(chuàng)建合約的方式，利用Solidity語言編寫智能合約源代碼，再編譯為智能合約字節(jié)碼，并向“0”地址發(fā)送包含智能合約字節(jié)碼的交易來生成合約地址。第二種是采用消息調(diào)用的方式。

圖1 以太坊中的交易方式

Figure 1 Transactions way in Ethereum

相較于比特幣系統(tǒng)直接進行的簡單交易，在以太坊中，外部賬戶將經(jīng)過數(shù)字簽名的數(shù)據(jù)包發(fā)送到另外的賬戶，賬戶狀態(tài)發(fā)生變化并被記錄到區(qū)塊鏈中，在此過程中合約賬戶通過消息調(diào)用與其他合約賬戶交互。交易結(jié)束后系統(tǒng)狀態(tài)發(fā)生改變。以太坊中的去中心化應(yīng)用程序（Dapp，decentralized application）可由交易或消息觸發(fā)，消息可由交易或以太坊虛擬機（EVM，Ethereum virtual machine）字節(jié)碼觸發(fā)。消息觸發(fā)方式有4種，如圖2所示。當(dāng)某些被調(diào)用的功能是惡意的，消息觸發(fā)不當(dāng)可能會導(dǎo)致漏洞。交易具有原子性，無法撤回和打斷執(zhí)行過程。以太坊賬戶發(fā)起的交易包括3類：創(chuàng)建新合約；直接向其他合約或用戶轉(zhuǎn)賬；調(diào)用其他合約中的某個可執(zhí)行函數(shù)。當(dāng)出現(xiàn)第3類交易時，合約代碼將載入以太坊虛擬機中運行。當(dāng)交易被礦工節(jié)點打包提交并得到其他節(jié)點的共識，區(qū)塊鏈上所有的節(jié)點都會執(zhí)行該合約代碼[18]。

圖2 4種消息觸發(fā)方式

Figure 2 Four ways of triggering a message

1.3 以太坊的gas機制

EVM字節(jié)碼中除了return與stop以外的任意指令都需要支付gas費。讀操作指令不改變區(qū)塊鏈的狀態(tài)，執(zhí)行速度較快，gas費較低[19]；而寫操作指令會導(dǎo)致賬戶的存儲狀態(tài)改變，執(zhí)行代價較高，因此gas消耗量較高。交易的創(chuàng)建者可以指定gasPrice和gasLimit兩個變量。其中g(shù)asPrice表示在交易執(zhí)行時消耗的每單元gas所支付的以太幣數(shù)額，gasLimit表示交易執(zhí)行所消耗的以太幣上限。而當(dāng)消耗的以太幣達到上限時，程序?qū)o法繼續(xù)執(zhí)行并回退到初始狀態(tài)。gas機制保證了合約程序總會在有限步之內(nèi)終止。

以太坊的gas機制如圖3所示，以太坊中的不同操作會消耗gas，如操作指令、創(chuàng)建合約或進行消息調(diào)用、使用存儲結(jié)構(gòu)等，且不同情況下gas的消耗量也是不同的。當(dāng)操作回退時，多余的gas會返還給賬戶，但已消耗的gas無法退還。

圖3 以太坊的gas機制

Figure 3 The Ethereum's gas mechanism

類似于傳統(tǒng)的區(qū)塊鏈系統(tǒng)，以太坊中的記賬工作是由獨立的礦工節(jié)點完成的[18]。礦工節(jié)點收集用戶提交的交易信息，將交易信息打包成區(qū)塊并提交到鏈上。這些交易信息可能會觸發(fā)對合約代碼的調(diào)用。合約代碼執(zhí)行時消耗的gas費會成為礦工的收益，因此礦工節(jié)點通常優(yōu)先打包 gasPrice值較高的交易。

1.4 以太坊虛擬機的存儲結(jié)構(gòu)

EVM作為智能合約和以太坊操作系統(tǒng)的中介，將由高級程序語言編寫的智能合約源代碼編譯為可在EVM上自動執(zhí)行的、低級的機器操作碼[3]，并將機器碼與執(zhí)行環(huán)境隔離。EVM中包含3種數(shù)據(jù)存儲結(jié)構(gòu)：易失性堆棧（stack）、易失性內(nèi)存（memory）以及非易失性存儲結(jié)構(gòu)（storage）[20]。了解EVM的存儲結(jié)構(gòu)有助于理解整數(shù)溢出[11]、變量類型聲明不當(dāng)?shù)嚷┒串a(chǎn)生的方式和原因。

EVM的堆棧用于存儲值類型的局部變量，是易失性的存儲結(jié)構(gòu)。從圖4可以看出，堆棧深為1 024，當(dāng)遞歸調(diào)用深度超過1 024時，會產(chǎn)生相應(yīng)的溢出錯誤。對棧的訪問僅限于其頂部的16層，且不會造成gas消耗。當(dāng)合約中聲明保存的局部變量超過16時，會造成棧溢出的錯誤，EVM可以使用除STOP、JUMPDEST和INVALID外的操作碼對堆棧進行數(shù)據(jù)的讀取或者寫入，使用POP、PUSH、SWAP等指令進行操作。

EVM的內(nèi)存與普通CPU的內(nèi)存類似，用于臨時保存代碼運行時的指令和數(shù)據(jù)，如緩存的數(shù)據(jù)或子合約調(diào)用時函數(shù)產(chǎn)生的臨時變量[20]。如圖4所示，內(nèi)存位寬為8 bit，按字節(jié)數(shù)組形式存儲，并按字節(jié)級尋址。內(nèi)存作為易失性的線性存儲結(jié)構(gòu)，當(dāng)EVM重新開始執(zhí)行時，內(nèi)存中保存的數(shù)據(jù)將被清空，程序計數(shù)器歸0。在以太坊的內(nèi)存中進行數(shù)據(jù)的讀取和寫入時，可選擇256 bit或8 bit作為單位，對gas的消耗相較于存儲更低，通過MSTORE、MSTORE8、MLOAD指令訪問。

EVM的存儲作為非易失性存儲器，所記錄的數(shù)據(jù)被同步到區(qū)塊鏈中，如圖4右側(cè)所表示的存儲區(qū)的結(jié)構(gòu)，存儲區(qū)的數(shù)據(jù)按照鍵值對應(yīng)存儲，并以256 bit進行讀取或?qū)懭耄?dāng)沒有更小的存儲空間時，單值存儲uint8與uint256類型的數(shù)據(jù)消耗的gas相同，因此智能合約驗證過程中，會判斷是否存在gas消耗可優(yōu)化的情況。存儲區(qū)中保存了合約狀態(tài)和合約代碼，如合約中聲明的公共狀態(tài)變量和越過局部作用域后無法訪問的局部變量。EVM通過SLOAD、SSTORE等指令對存儲進行操作，storage類型的參數(shù)通常采用指針傳遞，對存儲進行讀寫會消耗大量gas。

1.5 智能合約高級語言

Solidity是以太坊中最常用的編寫智能合約的高級語言[17]，其語法類似于Javascript。Solidity支持如繼承、庫函數(shù)、用戶自定義類型等較為復(fù)雜的特性。

當(dāng)智能合約的編寫中對變量的引用類型聲明錯誤時，會造成安全漏洞。如果在編寫合約時，混亂地使用引用類型，將會造成函數(shù)的類型聲明錯誤，進而影響合約運行。Solidity中數(shù)據(jù)的類型通常分為值類型（如布爾類型、地址、函數(shù)等）和引用類型（如數(shù)組、結(jié)構(gòu)體等）。對于引用類型，需要說明數(shù)據(jù)的存儲位置。編寫合約時，不同的引用類型可按照默認位置進行存儲，也可以通過聲明類型名關(guān)鍵字storage或memory的方式修改存儲位置。其中，編譯合約時會將合約聲明的公共狀態(tài)變量強制為storage的存儲結(jié)構(gòu)，交易通過調(diào)用函數(shù)修改狀態(tài)變量的值，從而改變交易狀態(tài)。局部變量默認為存儲[2]。在存儲中，狀態(tài)變量通過引用傳遞賦值給局部變量，對局部變量的修改可影響狀態(tài)變量,因此不能將內(nèi)存中的變量賦值給局部變量，否則會影響狀態(tài)變量的值。圖5反映了賬戶與交易、區(qū)塊的聯(lián)系，并且展示了區(qū)塊中包含的信息。

storage中包含合約代碼中全局變量的值，當(dāng)一個交易執(zhí)行成功后，全局變量更新后的值將被記錄在區(qū)塊鏈上。storage和賬戶余額balance共同構(gòu)成了合約賬戶當(dāng)前的狀態(tài)，整個EVM的狀態(tài)被稱為世界狀態(tài)，是從賬戶地址到賬戶狀態(tài)的映射。

圖4 以太坊的執(zhí)行資源及存儲結(jié)構(gòu)

Figure 4 Execution resources and storage structure of Ethernet

圖5 以太坊中的交易與世界狀態(tài)

Figure 5 Transactions and state of the world in Ethereum

2 智能合約的漏洞分類

智能合約中漏洞產(chǎn)生的原因不盡相同。本節(jié)參考了SmartContractSecurity和CWE漏洞庫，將智能合約的常見漏洞進行分類，包括未聲明函數(shù)的可見性、重入漏洞、整數(shù)溢出漏洞、代理調(diào)用漏洞、tx.origin認證漏洞、異常處理不當(dāng)、時間戳依賴、交易順序依賴等。以下將分別對這些漏洞做簡要介紹。

2.1 未聲明函數(shù)

Solidity的合約代碼中規(guī)定了函數(shù)的4種可見性聲明，包括public、private、external、internal，在未指定智能合約函數(shù)訪問權(quán)限時默認為 public，聲明為public函數(shù)的允許被內(nèi)部函數(shù)和外部函數(shù)調(diào)用；聲明為external的函數(shù)可被其他外部函數(shù)調(diào)用，但不能被合約內(nèi)的其他函數(shù)調(diào)用；聲明為internal的函數(shù)可被本合約及其子合約調(diào)用；聲明為private的函數(shù)僅可在本合約中被調(diào)用，外部合約不可訪問此類函數(shù)或更改數(shù)據(jù)。表1中對不同函數(shù)的可見性做出總結(jié)。

表1 函數(shù)的可見性總結(jié)

注：“√”表示可被調(diào)用，“×”表示不可被調(diào)用、訪問或更改。

在編寫合約代碼時，不正確地聲明函數(shù)的可見性，尤其是不恰當(dāng)?shù)厥褂每梢娦阅J為public的函數(shù)，可能會導(dǎo)致黑客能夠隨意調(diào)用函數(shù)，破壞智能合約的執(zhí)行邏輯，產(chǎn)生安全漏洞。

除了函數(shù)的可見性聲明可以約束函數(shù)的調(diào)用，修飾器modifier也能起到約束函數(shù)行為的作用。在合約邏輯層面，一般使用關(guān)鍵字modifier添加函數(shù)約束，用于在函數(shù)執(zhí)行之前對所有權(quán)的檢查，如修飾符onlyOwner會檢查當(dāng)前是否為部署者執(zhí)行函數(shù)調(diào)用，未添加修飾符可能會造成非合約部署者操作關(guān)鍵函數(shù)，從而導(dǎo)致漏洞。例如，為了實現(xiàn)代碼復(fù)用，以太坊中提供了delegatecall指令用于調(diào)用外部的庫函數(shù)。庫函數(shù)中關(guān)鍵函數(shù)被默認為public，任意攻擊者都可以調(diào)用函數(shù)竊取賬戶余額，導(dǎo)致parity多重簽名錢包的項目中，被竊取了價值3 100萬左右美元的以太幣[13]。

2.2 重入漏洞

以太坊中的智能合約可以相互調(diào)用完成交易。當(dāng)合約C1在調(diào)用合約C2后，必須要等C2執(zhí)行完畢，C1才會繼續(xù)執(zhí)行。重入漏洞是指C2在被調(diào)用后利用合約C1所處狀態(tài)可能存在的不一致問題，對合約C1發(fā)起攻擊。在The DAO[12]事件中，攻擊者利用的就是合約代碼中的重入漏洞。圖6表示一個重入漏洞的代碼示例。惡意用戶可以構(gòu)建合約Attacker，先調(diào)用Wallet合約的deposit函數(shù)存入一定的金額，再調(diào)用withdrawAll函數(shù)將金額取出，withdrawAll函數(shù)的第7行執(zhí)行向Attacker轉(zhuǎn)賬的命令。在以太坊中，當(dāng)合約收到以太幣的轉(zhuǎn)賬時會自動執(zhí)行一個無函數(shù)名、無參數(shù)以及無返回值的回退（fallback）函數(shù)。Attacker合約的第7行到第9行重寫了回退函數(shù)，再次調(diào)用Wallet的withdrawAll函數(shù)，但此時Wallet合約還沒有執(zhí)行第8行對Attacker賬戶余額的置0操作，這個暫時的不一致狀態(tài)被Attacker所利用，導(dǎo)致Wallet合約的所有余額被轉(zhuǎn)入Attacker的賬戶中。重入漏洞造成的損失較大，是以太坊中頻繁發(fā)生的安全事故，因此，重入漏洞是各類工具檢測的重點。

圖6 重入漏洞示例

Figure 6 An example of the reentrancy bug

2.3 整數(shù)溢出漏洞

以太坊虛擬機與通用計算機的存儲空間特性類似，編程語言中的整數(shù)類型長度在存儲空間中具有存儲限制。Solidity語言中的整型變量步長以8遞增，支持從uint8到uint256類型的數(shù)。圖4表示了EVM的存儲結(jié)構(gòu)。EVM中的存儲空間最多存儲uint8的無符號整數(shù)類型，當(dāng)需要存儲的數(shù)據(jù)超過EVM數(shù)據(jù)空間的范圍時，EVM會執(zhí)行截斷，可能會造成溢出。溢出類型通常有乘法溢出、加法溢出、減法溢出。當(dāng)智能合約缺少完善的數(shù)值檢測語句，在算術(shù)運算時容易出現(xiàn)上溢或下溢的錯誤。例如，2018年，美鏈合約未使用標(biāo)準(zhǔn)數(shù)學(xué)運算庫SafeMath庫中定義的運算，在交易過程中直接使用了乘法運算符而沒有進行相應(yīng)的溢出檢測，造成整數(shù)溢出漏洞[21]，最終導(dǎo)致BEC合約的價值蒸發(fā)。

2.4 代理調(diào)用漏洞

以太坊中存在多個調(diào)用函數(shù)類型，其中委托調(diào)用函數(shù)delegatecall可直接使用外部合約的庫代碼，以實現(xiàn)代碼復(fù)用。攻擊者可以在外部合約中惡意注入有害代碼，當(dāng)被調(diào)用的函數(shù)違反合約邏輯時，會造成極大的安全隱患。

2018年4月，parity多重簽名錢包經(jīng)歷了第二次攻擊[14]，如圖7所示，代理調(diào)用漏洞可能伴隨函數(shù)未聲明可見性的漏洞。由于walletLibrary可見性聲明為public，攻擊者通過調(diào)用WalletLibrary合約中的initWallet()函數(shù)，成為該庫的owner，隨機調(diào)用kill()函數(shù)刪除該庫函數(shù)。錢包內(nèi)的以太幣轉(zhuǎn)出完全依賴于walletLibrary，walletLibrary的銷毀使得錢包余額被凍結(jié)。

圖7 代理調(diào)用漏洞示例

Figure 7 An example of mishandled exception

2.5 tx.origin認證漏洞

Solidity語言中，tx.origin作為全局變量，可以返回最初發(fā)送交易的地址。當(dāng)合約使用tx.origin授權(quán)聲明所有者的權(quán)限時，只能返回最初的交易發(fā)起者的賬戶地址。例如，用戶A調(diào)用合約C5，合約C5再調(diào)用合約C6。對于合約C6來說，msg.sender地址唯一，為合約C5的地址，但實際上調(diào)用C6的是tx.origin所聲明的用戶A的地址。具體的tx.origin漏洞示例如圖8所示。合約Wallet的withdraw函數(shù)中用tx.origin來確認交易的發(fā)起者就是賬戶的所有者。此時，如果合約Wallet向Attacker發(fā)起任意一筆轉(zhuǎn)賬時，會自動調(diào)用Attacker合約第3行的回調(diào)函數(shù)，進一步調(diào)用合約Wallet的withdrawAll函數(shù)。由于交易最初的發(fā)起人確實是Wallet的所有者，因此第7行的條件驗證可以通過，合約Wallet的所有余額都將被轉(zhuǎn)給 Attacker合約。攻擊者利用tx.origin聲明所有者的權(quán)限，通過惡意調(diào)用繞過授權(quán)檢查，可能導(dǎo)致重入漏洞。

圖8 tx.origin認證漏洞示例

Figure 8 An example of mishandled exception

2.6 異常處理不當(dāng)

智能合約在以太坊的運行中具有順序性和原子性，當(dāng)存在如下3種情況時會拋出異常：執(zhí)行過程中耗盡gas值；調(diào)用棧深超過1 024；采用assert與require函數(shù)進行條件檢查后拋出revert函數(shù)或throw關(guān)鍵字。

執(zhí)行合約出現(xiàn)異常時會進行回滾。合約調(diào)用其他合約時可能無法識別其他合約的錯誤標(biāo)識。例如，智能合約的底層調(diào)用函數(shù)send、call和delegatecall等發(fā)生異常時只返回false，而不會拋出異常。在以太坊中，當(dāng)合約C1在調(diào)用合約C2時，如果C2在執(zhí)行過程中出現(xiàn)了異常，C2的狀態(tài)將回退并返回false，此時合約C1應(yīng)當(dāng)檢查智能合約C2的返回情況再繼續(xù)執(zhí)行，否則可能造成合約狀態(tài)的不一致。KoET智能合約是存在異常處理不當(dāng)問題的典型例子[22]。KoET是基于以太坊的智能合約游戲，參與游戲的玩家需支付一定數(shù)量的以太幣給現(xiàn)任“國王”稱號的所有者。圖9是一段KoET合約代碼的示例。這段代碼的問題在于沒有檢查第7行中的調(diào)用是否執(zhí)行成功，攻擊者可以故意構(gòu)造出異常來獲利。例如，通過以太坊虛擬機對調(diào)用棧深度不超過1 024的限制，攻擊者可以通過自調(diào)用使調(diào)用深度達到1 023再調(diào)用claimThrone函數(shù)競爭“國王”稱號，此時轉(zhuǎn)賬將會因為超出棧的調(diào)用深度而失敗，原“國王”稱號的所有者將失去稱號但無法收到相應(yīng)的報酬。上述情況說明，每當(dāng)出現(xiàn)外部調(diào)用時都應(yīng)當(dāng)對調(diào)用結(jié)果做檢查，當(dāng)調(diào)用成功后再繼續(xù)執(zhí)行后續(xù)操作。

圖9 異常處理不當(dāng)示例

Figure 9 An example of mishandled exception

2.7 時間戳依賴攻擊

時間戳依賴指智能合約在選擇程序執(zhí)行路徑時將時間戳作為關(guān)鍵的隨機變量。礦工在打包區(qū)塊時要設(shè)置區(qū)塊的時間戳信息，通常設(shè)置為礦工節(jié)點的本地時間，但惡意礦工可能會有意將時間戳設(shè)置為特定的值。如果合約以時間戳作為隨機數(shù)來決定是否轉(zhuǎn)賬，那么很可能被礦工節(jié)點利用。

2.8 交易順序依賴

2.9 小結(jié)

本節(jié)總結(jié)了8種常見的智能合約漏洞。從中可以看出，依靠傳統(tǒng)測試的方法保證智能合約的安全性是很困難的。智能合約間存在相互調(diào)用的情況，開發(fā)者無法預(yù)知其他合約的執(zhí)行邏輯，智能合約的實際執(zhí)行情況可能會超出合約開發(fā)者的想象。大量軟件存在缺陷的根本原因是開發(fā)者對語義的理解與智能合約系統(tǒng)的實際語義之間存在語義鴻溝[23]。在保證智能合約安全性的工作中引入形式化方法顯得十分必要。

3 智能合約的形式化驗證

形式化驗證方法包括符號執(zhí)行[24]、模型檢測[25]、定理證明[26]等。本節(jié)將分別介紹不同驗證方法的代表研究成果。

3.1 符號執(zhí)行

符號執(zhí)行是較常見的智能合約分析技術(shù)。符號執(zhí)行的主要思想是符號化地執(zhí)行程序，程序的輸出為變量的表達式。每一條路徑對應(yīng)一個路徑可達的條件公式，通常需要約束求解器來判定程序路徑的可達性。符號執(zhí)行能夠遍歷程序的路徑空間，從而檢查程序是否滿足給定的安全性質(zhì)。Luu等[23]開發(fā)的漏洞檢測工具Oyente是利用符號執(zhí)行技術(shù)驗證智能合約的開創(chuàng)性工作。Oyente以智能合約的EVM字節(jié)碼和當(dāng)前以太坊的全局狀態(tài)作為輸入，分析合約是否存在安全問題，并返回存在問題的程序執(zhí)行路徑。Oyente能夠檢測交易順序依賴漏洞、時間戳依賴漏洞、異常處理不當(dāng)、重入漏洞等智能合約漏洞。Oyente定義了一個簡化的EVM操作語義，通過分析程序生成控制流圖，并符號化執(zhí)行合約代碼，以Z3[27]作為求解器判定程序路徑可達性，針對每一類漏洞類型定義了相應(yīng)的代碼模式，根據(jù)符號執(zhí)行的結(jié)果判斷是否滿足其中一類模式。Mueller[28]開發(fā)的漏洞檢測工具Mythril與Oyente的技術(shù)路線基本一致，基于以太坊官方的操作語義[19]，并引入了污點分析技術(shù)。Nikoli?等[29]在Oyente的基礎(chǔ)上開發(fā)了驗證工具Maian，相對于Oyente只考慮一個合約被單次調(diào)用后的行為，Maian對一個合約多次被調(diào)用的情況建模，側(cè)重檢測程序的軌跡缺陷。Maian重點研究了兩類安全性質(zhì)（資金泄露與賬戶銷毀）和一類活性性質(zhì)（資金凍結(jié)）。Maian以EVM字節(jié)碼為輸入，支持133個字節(jié)碼指令中的121個，遇到不支持的指令將跳過該路徑并回溯，因此不能覆蓋所有路徑。Mossberg等[30]用動態(tài)符號執(zhí)行技術(shù)開發(fā)了驗證工具Manticore，其優(yōu)勢是使用較為簡單。Krupp等[31]定義了易受攻擊的合約并基于此開發(fā)了驗證工具TEETHER。VerX是一個基于符號執(zhí)行的工具[32]，將時序邏輯的安全性驗證歸約為程序可達性分析，因而能夠驗證表達為時序邏輯的安全性質(zhì)。Torres等開發(fā)的符號執(zhí)行驗證工具Osiris[33]和HoneyBadger[34]分別能夠識別整數(shù)相關(guān)的漏洞、蜜罐合約。Chen等[35]開發(fā)的TokenScope分析了智能合約的不一致問題。

Tsankov等[36]開發(fā)了一個基于數(shù)據(jù)流、控制流分析的可擴展驗證工具Securify。該研究基于如下觀察：如果合約代碼滿足或違反了一個性質(zhì)，它大概率滿足或違反若干更加簡單的模式，如超過九成的重入漏洞代碼有在外部函數(shù)調(diào)用后修改storage的行為。該研究定義了一個描述代碼模式的領(lǐng)域?qū)Ｓ谜Z言Securify（與驗證工具同名），在此基礎(chǔ)上定義了以太幣流動性、調(diào)用操作后沒有寫操作等7類代碼模式。用戶可以利用Securify語言自定義新的代碼安全模式。Securify驗證工具以EVM字節(jié)碼和自定義安全性質(zhì)為輸入，驗證合約代碼滿足或違反給定的性質(zhì)，其分析過程分為3步：首先，對EVM字節(jié)碼反匯編，使代碼不依賴于棧結(jié)構(gòu)；之后，借助Datalog[37]和Soufflé[38]推導(dǎo)合約代碼的語義，得到數(shù)據(jù)流和控制流的依賴關(guān)系；最后，根據(jù)合約的語義信息驗證是否滿足給定的代碼模式。Securify的缺點在于無法處理與整數(shù)相關(guān)的性質(zhì)。Kalra等[39]開發(fā)了基于抽象解釋的檢測工具Zeus。一個交易的執(zhí)行過程一定是若干public函數(shù)的連續(xù)調(diào)用，Zeus應(yīng)用此特點顯著減少了待驗證的狀態(tài)空間，提高了驗證效率。

Feist等[40]開發(fā)了靜態(tài)分析框架Slither，該框架將Solidity代碼轉(zhuǎn)換為中間表示SlithIR，可利用數(shù)據(jù)流分析、污點分析等技術(shù)檢測程序漏洞。Tikhomirov等[41]開發(fā)了靜態(tài)分析工具SmartCheck。SmartCheck分析Solidity代碼生成XML解析樹，根據(jù)路徑語言Xpath檢測漏洞。Schneidewind等[42]開發(fā)了基于靜態(tài)分析技術(shù)的驗證工具EThor。EThor利用Horn邏輯分析程序的可達性，并由此分析程序的安全性質(zhì)。Grech等[43]基于靜態(tài)分析技術(shù)開發(fā)了檢測工具MadMax，其能夠識別由gas耗盡帶來的安全問題。

以符號執(zhí)行為代表的程序分析技術(shù)對于合約開發(fā)人員避免常見漏洞是很好的輔助工具，但無法作出安全性的保證。這些工具通常需要依賴于專家對危險代碼模式的定義，但簡單的模式匹配并不能完全刻畫復(fù)雜的安全性質(zhì)，會帶來不同程度的誤報和漏報。

3.2 模型檢測

模型檢測是形式化驗證的一類重要驗證技術(shù)。首先，將待驗證系統(tǒng)抽象為狀態(tài)空間有限的形式模型；然后，通過搜索有限的狀態(tài)空間分析形式模型的行為是否滿足給定的時序性質(zhì)，當(dāng)性質(zhì)不滿足時給出違反該性質(zhì)的執(zhí)行路徑。

模型檢測技術(shù)已經(jīng)發(fā)展得比較成熟，有許多優(yōu)秀的模型檢測工具，如SPIN[44]、UPPAAL[45]、NuSMV[46]等。目前已有一些將這些方法應(yīng)用在智能合約驗證工作中的嘗試，如Nehai等[47]用NuSMV語言對智能合約建模，建模分為3個層次，分別是內(nèi)核層、應(yīng)用層和環(huán)境層。內(nèi)核層建模以太坊的行為，應(yīng)用層建模智能合約的行為，環(huán)境層建模合約的執(zhí)行環(huán)境框架，待驗證的性質(zhì)被刻畫為CTL邏輯公式，借助NuSMV工具驗證模型是否滿足給定性質(zhì)。Abdellatif等[48]用模型檢測語言BIP建模智能合約，不僅對合約做建模，還包括用戶和簡化的區(qū)塊鏈環(huán)境的行為。Bai等[49]將智能合約建模為狀態(tài)遷移系統(tǒng)，將待驗證性質(zhì)表示為LTL公式，并用模型檢測工具SPIN進行驗證。智能合約程序中可能涉及一些與時間相關(guān)的執(zhí)行邏輯。Andrychowicz等[50]用時間自動機建模，并提出了在模型檢測工具UPPAAL中驗證的方法。

智能合約不存在并發(fā)行為[51]。在合約間發(fā)生調(diào)用時，只有當(dāng)被調(diào)用合約執(zhí)行完畢后，原合約才會繼續(xù)執(zhí)行。但Sergey等[51]指出，智能合約的一些特性類似于并發(fā)系統(tǒng)，如合約之間的相互調(diào)用類似于并發(fā)系統(tǒng)中不同進程間的通信行為；交易順序的不確定性對交易結(jié)果的影響也類似于并發(fā)系統(tǒng)中的數(shù)據(jù)競爭問題。Sergey等[51]認為可以引入傳統(tǒng)并發(fā)模型的研究方法來解決智能合約的驗證問題。受此觀點影響，有許多用傳統(tǒng)并發(fā)模型如進程演算、Petri網(wǎng)對智能合約建模的研究工作。例如，Bartoletti等[52]定義了領(lǐng)域?qū)Ｓ谜Z言BitML幫助用進程演算來建模智能合約；Laneve定義了進程演算scl對智能合約建模[53]；Qu等[54]用通信順序進程建模合約代碼，并用模型檢測工具FDR（failure divergence refinement）[55]驗證合約正確性；Li等[56]將智能合約建模為Pi演算的一個變種，并用Tamarin工具做驗證。Wang等[57]和Liu等[58]的建模方法都基于著色Petri網(wǎng)，以ASK-CTL表示待驗證性質(zhì)，在模型檢測工具CPN Tools中驗證以太坊系統(tǒng)的性質(zhì)。

應(yīng)用模型檢測技術(shù)能夠嚴格證明合約是否滿足給定的安全性或活性，是較為嚴格的驗證技術(shù)。但是模型檢測方法存在一些局限性，如要求待驗證的模型是有限狀態(tài)的，并且由于模型檢測存在狀態(tài)爆炸問題，驗證效率會受到影響。

3.3 定理證明

定理證明通常將待驗證系統(tǒng)和性質(zhì)統(tǒng)一描述在合適的邏輯系統(tǒng)中。根據(jù)公理和推理規(guī)則，借助定理證明器去證明待驗證性質(zhì)，目前的定理證明器大多是交互式的，如Coq[59]、Isabelle/HOL[60]。

首次基于定理證明的智能合約驗證工作是由Hirai[61]提出的。Hirai首先用Lem語言[62]描述EVM字節(jié)碼，Lem語言支持當(dāng)前大多數(shù)定理證明器，再利用Isabelle/HOL驗證合約的相關(guān)簡單安全性質(zhì)。Annenkov等[63]提出了基于元編程的方式，將智能合約代碼轉(zhuǎn)換為Coq程序，構(gòu)建了驗證框架ConCert。Bhargavan等[64]分別將Solidity代碼和編譯后的EVM字節(jié)碼翻譯到F*語言，驗證翻譯后結(jié)果的一致性。Amani等[65]利用以太坊的gas機制對合約終止性的保證，定義了一個類似Hoare邏輯的程序邏輯，并提出了基于Isabelle/HOL的面向EVM字節(jié)碼的驗證方法。Yang等[66]基于Coq定理證明器，在Solidity語言的一個子集上[67]開發(fā)了FEther，F(xiàn)Ether包含部分自動化策略，提高了驗證的自動化程度。除了Solidity和EVM 字節(jié)碼外，還有一些面向智能合約的中間語言的研究。例如，Li等[68]給出了基于Isabelle/HOL 驗證智能合約中間語言Yul的方法。Sergey等[69]提出了基于Coq驗證智能合約時序性質(zhì)的方法。Sun等[70]提出了基于Coq驗證BNB智能合約的方法。

相比于模型檢測，定理證明技術(shù)的優(yōu)勢是可以驗證無限狀態(tài)系統(tǒng)。但是目前的工作都依賴于交互式的定理證明器，在驗證過程中需要有相關(guān)知識背景的專家參與，因此缺少高度自動化的驗證工具。

3.4 其他工作

智能合約嚴格的形式語義是符號執(zhí)行、定理證明等工作的基礎(chǔ)。以太坊發(fā)布的黃皮書是描述EVM語義的官方文檔[19]，但未過多考慮實際應(yīng)用時的復(fù)雜場景，其定義并不完備，無法支撐形式化驗證的工作。基于F*語言[71]，Grishchenko等[72]定義了EVM字節(jié)碼的完備的小步語義。基于K框架[73]，Hildenbrandt等[74]定義了EVM的可執(zhí)行的形式語義KEVM。

不同于此前大部分語義定義中的EVM字節(jié)碼，Jiao等[75]根據(jù)Solidity語言的語義，將Solidity源碼編譯成中間語言。合約開發(fā)者可以用Solidity語言編寫合約，再編譯成便于驗證器操作的中間語言，驗證合約代碼的正確性，如Sergey等[76]定義的中間語言Scilla。Scilla的設(shè)計遵循幾個原則：程序中合約內(nèi)部的計算被設(shè)計為獨立的狀態(tài)遷移，這一方式區(qū)分了合約的內(nèi)部計算和合約間的交互；劃分了改變狀態(tài)的計算和不改變狀態(tài)的計算；便于識別普通調(diào)用和續(xù)體傳遞[77]。這表明Scilla中間語言適用于驗證，且由于其代碼可自動生成，能夠避免合約開發(fā)者在編寫中引入漏洞。代碼自動生成方面的代表工作是Mavridou等[78-79]提出的FSolidM框架，用戶可以將合約行為定義為有限狀態(tài)機，利用FSolidM能夠生成對應(yīng)的合約代碼。在FSolidM的基礎(chǔ)上Mavridou等[80]又提出了VeriSolid框架，進一步擴展了語法和語義，并集成了基于模型檢測的工具，如nuXmv和BIP等。存在專門針對某類安全漏洞的工作，如重入漏洞[81-82]、資金凍結(jié)問題[83]、交易順序依賴漏洞[84]等。此外，將形式化方法與模糊測試[85-86]、運行時驗證[87]、博弈論[88]等方式結(jié)合來驗證智能合約安全性的研究逐漸成為主流。

4 驗證工具的總結(jié)與實驗分析

第3節(jié)介紹了智能合約形式化驗證的代表工作，表2對這些工作做了一個簡要的總結(jié)。本節(jié)選擇其中具有代表性的工具進行實驗，并對分析結(jié)果進行對比。基于模型檢測及定理證明方法的智能合約驗證工具多數(shù)需要建模或?qū)⒅悄芎霞s源代碼、EVM字節(jié)碼轉(zhuǎn)換成中間語言，自動化程度較低，實驗時需要較多的人為干預(yù)。且部分工具如Zeus無可用開源代碼。基于以上原因，本節(jié)選取3個開源的基于符號執(zhí)行的智能合約檢測工具（Mythril、Slither以及Oyente），對Smartbugs數(shù)據(jù)集中的143個合約文件進行檢測。該數(shù)據(jù)集中的合約包含208個標(biāo)記的漏洞，可用于評估合約工具的準(zhǔn)確性。

表2 智能合約工具

在Smartbugs數(shù)據(jù)集中已經(jīng)開源了其中69份已標(biāo)記漏洞的合約。本節(jié)使用Mythril和Slither工具對這69份合約進行檢測，根據(jù)實驗結(jié)果，對69份合約（除處理超時或版本錯誤的合約文件）中之前未被檢測出的漏洞進行補充標(biāo)記，結(jié)果如表3所示。

Mythril作為以太坊官方推薦的智能合約靜態(tài)分析檢測工具，使用了污點分析、控制流驗證等技術(shù)。表3列舉了在實驗過程中，數(shù)據(jù)集中的合約新檢測出的漏洞。Mythril適合檢測任意存儲位置的寫入漏洞、重入漏洞、無保護的以太幣提款漏洞。Mythril在Oyente工具的基礎(chǔ)上進行了擴展，利用多次符號執(zhí)行可以還原實際合約執(zhí)行過程中復(fù)雜的調(diào)用情況。

Slither將Solidity源碼轉(zhuǎn)換為混合中間語言SlithIR，利用Solidity抽象語法樹生成合約的繼承關(guān)系。Slither中包含20多種對不同類型的漏洞進行檢測的探測器，并且用戶可以使用第三方工具基于中間語言SlithIR來建立更高級的分析。如表3所示，Slither對使用過時的編譯器版本漏洞、重入漏洞、未聲明狀態(tài)變量可見性漏洞、時間戳依賴攻擊漏洞、使用密碼學(xué)上較弱的偽隨機數(shù)發(fā)生器漏洞的檢測效果較好。Slither工具的檢測結(jié)果，可以幫助用戶和審查員理解代碼。用戶還可以通過第三方接口與Slither檢測工具進行交互，輔助代碼的審查。

通過實驗發(fā)現(xiàn)，Slither工具對代碼的覆蓋率較高。表4的實驗結(jié)果說明，Slither的平均處理速度快于Mythril工具，且檢出的漏洞種類較多。

表3 對smartbugs數(shù)據(jù)集中合約的漏洞檢測進行補充標(biāo)記

表4 Mythril，Slither和Oyente工具的處理結(jié)果

對于重入漏洞的檢測，Slither工具檢測的準(zhǔn)確率高于Mythril；在算數(shù)漏洞中，Mythril工具的處理結(jié)果準(zhǔn)確率更高。而Oyente工具由于長時間未更新，實驗效果并不理想。

此次實驗表明，用戶使用第三方接口基于中間語言自定義漏洞類型進行檢測，可以結(jié)合不同的測試方法，擴展檢測漏洞的類型[89]。在后續(xù)工作中將會對漏洞類型進一步細分，明確分類標(biāo)準(zhǔn)，并嘗試在現(xiàn)有的一些工具中，自定義第三方接口，提高代碼檢測的覆蓋率和準(zhǔn)確率。

5 相關(guān)工作總結(jié)

本節(jié)對相關(guān)的綜述文章做一個總結(jié)。

Atzei等[11]對智能合約可能遭受的攻擊方式的總結(jié)是早期的一個經(jīng)典工作。Delmolino等[90]在馬里蘭大學(xué)做了教學(xué)實驗，總結(jié)了學(xué)生在智能合約編碼中常犯的一些錯誤。Chen等[91]對智能合約攻擊和防御方式的總結(jié)是一個比較詳盡的補充。

Durieux等[92]對包括Oyente、Mythril、Securify、Smartcheck在內(nèi)的各種測試工具做了詳細的實驗比較。從準(zhǔn)確度，對不同類型漏洞的檢測能力，以及運行效率等方面分析了各類工具。Angelo等[93]總結(jié)了基于符號執(zhí)行的漏洞檢測工具。Imeri等[94]的綜述則主要側(cè)重模型檢測方面的結(jié)果。Parizi等[95]總結(jié)了不同類型的智能合約領(lǐng)域?qū)Ｓ镁幊陶Z言。

Grishchenko等[96]的綜述涵蓋了形式語義，性質(zhì)定義，檢測工具等不同方面的內(nèi)容。Tolmach等[97]給了一個相對全面的綜述，對已有的形式化建模工作分為兩類。一類是合約層面，將合約實現(xiàn)細節(jié)忽略，著重考慮合約與其他合約或外部環(huán)境之間的交互關(guān)系；另一類是程序?qū)用妫P(guān)注合約在執(zhí)行時的內(nèi)部細節(jié)。

近年來已有一些中文的綜述文章[98-100]。相較于這些工作，本文進行以下3點補充。

1) 對以太坊的機制以及智能合約的常見漏洞作了較為詳細的介紹。在此基礎(chǔ)上，對已有驗證工作的理論總結(jié)更加深入。

2) 涵蓋了2021—2022年新工作進展，對形式化驗證工作的總結(jié)更加全面。

3) 對現(xiàn)有的基于不同理論的智能合約檢測工具進行了對比實驗，結(jié)合實驗結(jié)果對檢測工具作出更加客觀的評價。

6 總結(jié)與展望

在系統(tǒng)總結(jié)了基于形式化方法的智能合約驗證的研究進展后，發(fā)現(xiàn)智能合約仍存在大量安全問題，阻礙了區(qū)塊鏈技術(shù)的大范圍落地。利用形式化方法檢測智能合約漏洞已經(jīng)有了大量研究成果，但目前仍有部分關(guān)鍵問題需要解決。

（1）檢測工具的覆蓋率較低

部分工具需要提取智能合約Solidity源代碼或EVM字節(jié)碼的語義編譯成中間語言，轉(zhuǎn)換時語義信息不全面、不準(zhǔn)確。

檢測工具對代碼的覆蓋率低，難以對代碼中所有復(fù)雜的調(diào)用情況和判斷條件做到檢測和推斷，對于跨合約的調(diào)用、實際復(fù)雜環(huán)境中的執(zhí)行過程、執(zhí)行過程中惡意代碼的攻擊等，無法進行全面準(zhǔn)確的執(zhí)行前預(yù)測。

（2）檢測工具的自動化程度以及可擴展性較低

目前檢測工具的自動化程度較低，部分工具的檢測需要進行人工干預(yù)、核驗與專家分析，對檢測結(jié)果進行手動檢查，篩選出漏洞的誤報結(jié)果。此外，編寫智能合約的主流語言為Solidity語言，但仍有其他語言如：Serpent[101]和LLL[102]可支持合約的編寫，對智能合約檢測工具的適配性和可擴展性造成極大的挑戰(zhàn)。

（3）智能合約的語義鴻溝問題

智能合約驗證中大部分缺陷出現(xiàn)的根本原因是智能合約系統(tǒng)的實際語義與開發(fā)者對合約的理解之間存在偏差。為解決語義鴻溝的問題，利用領(lǐng)域特定語言（DSL）來規(guī)范合約的語義，設(shè)計漏洞檢測的模式，仍是未來研究的難點。此外，有不少研究常用中間語言表達合約邏輯和語義的準(zhǔn)確性[40-43]，提高中間表示的通用性，規(guī)范中間語言的表示形式，仍是未來研究中需要關(guān)注的關(guān)鍵問題。

（4）關(guān)于智能合約驗證的評估體系不規(guī)范

由于目前基于形式化驗證技術(shù)的部分工具的自動化程度不高，缺乏測試用例集等原因，對智能合約驗證工作的評價準(zhǔn)則仍不規(guī)范。因此，需要建立較為標(biāo)準(zhǔn)的綜合評價體系來判定驗證方式的有效性。

在上述研究的基礎(chǔ)上，有以下幾個方向是值得進一步研究的。

1) 自動生成合約代碼。基于用戶對合約功能的定義自動生成代碼，能夠避免不規(guī)范的合約編寫引入錯誤。此前的大量工作聚焦于如何檢測合約代碼中的漏洞，關(guān)于代碼生成的研究比較少。目前的研究主要基于簡單的有限狀態(tài)系統(tǒng)[78-79]，該方向還有很大的提升空間。

2) Solidity編譯器的正確性驗證。即便Solidity代碼是安全的，如果編譯器本身存在漏洞，那么可能在編譯后的代碼中引入安全問題。關(guān)于Solidity編譯器在gas消耗方面，目前還沒有對編譯器的正確性驗證的研究[103]。

3) 中間語言的一致性驗證。目前有一些中間語言被提出[76,104]。在Solidity代碼轉(zhuǎn)換為中間語言，以及中間語言轉(zhuǎn)換為EVM字節(jié)碼時需要保證語義的一致性。目前還缺乏對語義一致性的研究。

4) 開發(fā)新的智能合約高級語言。另一個方向是重新設(shè)計一門更加安全的智能合約語言，減少合約開發(fā)者出錯的可能性。

5) 規(guī)范智能合約漏洞數(shù)據(jù)集及工具的性能評估標(biāo)準(zhǔn)。對各類智能合約檢測工具的評估所用的數(shù)據(jù)集較少且不統(tǒng)一，不同工具的性能對比存在誤差，且工具的評估標(biāo)準(zhǔn)沒有統(tǒng)一的規(guī)定，無法準(zhǔn)確分析有效性。

6) 除以太坊外，還有一些支持智能合約的區(qū)塊鏈平臺如超級賬本、EOS、區(qū)塊鏈底層技術(shù)開源平臺（BCOS，be credible, open & secure）等。以超級賬本為例，編寫超級賬本合約用的不是領(lǐng)域?qū)Ｓ谜Z言，而是通用語言如Go、Java等，可能出現(xiàn)一些與具體編程語言相關(guān)的漏洞[105]，和本文介紹的漏洞類型有較大區(qū)別。由于缺乏一個影響力較大的公共平臺，出現(xiàn)的漏洞事件相對較少，相關(guān)的智能合約驗證的研究也不多[105-106]。但是以超級賬本為代表的平臺受到來自企業(yè)的關(guān)注越來越多，在這些平臺上驗證智能合約的正確性將是一個重要的方向。

[1] NAKAMOTO S. Bitcoin: a peer-to-peer electronic cash system[J]. Consulted, 2008:1-49.

[2] BUTERIN V. A next-generation smart contract and decentralized application platform[R]. White Paper, 2014.

[3] SZABO N. Formalizing and securing relationships on public networks[J]. First Monday, 1997, 2(9).

[4] PETERS G W, PANAYI E. Understanding modern banking ledgers through blockchain technologies: future of transaction processing and smart contracts on the internet of moneybanking beyond banks and money[M]. Springer, 2016.

[5] AZARIA A, EKBLAW A, VIEIRA T, et al. MedRec: using blockchain for medical data access and permission management[C]//Proceedings of 2016 2nd International Conference on Open and Big Data (OBD). 2016: 25-30.

[6] GRIGGS K N, OSSIPOVA O, KOHLIOS C P, et al. Healthcare blockchain system using smart contracts for secure automated remote patient monitoring[J]. Journal of Medical Systems, 2018, 42(7): 130.

[7] CHRISTIDIS K, DEVETSIKIOTIS M. Blockchains and smart contracts for the Internet of Things[J]. IEEE Access, 2016, 4: 2292-2303.

[8] ?LNES S, UBACHT J, JANSSEN M. Blockchain in government: benefits and implications of distributed ledger technology for information sharing[J]. Government Information Quarterly, 2017, 34(3): 355-364.

[9] MENGELKAMP E, NOTHEISEN B, BEER C, et al. A blockchain-based smart grid: towards sustainable local energy markets[J]. Computer Science-Research and Development, 2018, 33(1): 207-214.

[10] ABEYRATNE S A. Blockchain ready manufacturing supply chain using distributed ledger[J]. International Journal of Research in Engineering and Technology, 2016, 5(9): 1-10.

[11] ATZEI N, BARTOLETTI M, CIMOLI T. A survey of attacks on ethereum smart contracts (SOK)[C]//International Conference on Principles of Security and Trust. 2017: 164-186.

[12] The DAO smart contract[EB]. 2016.

[13] An in-depth look at the parity multisig Bug[EB]. 2017.

[14] The parity wallet vulnerability[EB]. 2017.

[15] 王戟, 詹乃軍, 馮新宇, 等. 形式化方法概貌[J]. 軟件學(xué)報, 2019, 30(1): 33-61.

WANG J, ZHAN N J, FENG X Y, et al. Overview of formal methods[J]. Journal of Software, 2019, 30(1): 33-61.

[16] BONNEAU J, CLARK J, GOLDFEDER S. On bitcoin as a public randomness source[J]. IACR Cryptology ePrint Archive, 2015: 1015.

[17] DANNEN C. Introducing Ethereum and solidity[M]. Berkeley: Apress, 2017.

[18] ANDRYCHOWICZ M, DZIEMBOWSKI S. Distributed cryptography based on the proofs of work[J]. IACR Cryptology ePrint Archive, 2014: 796.

[19] WOOD G. Ethereum: a secure decentralised generalised transaction ledger[J]. Ethereum Project Yellow Paper, 2014, 151: 1-32.

[20] BUTERIN V. Dagger: a memory-hard to compute, memory-easy to verify scrypt alternative[R]. 2013.

[21] BeautyChain Integer Overflow[EB]. 2018.

[22] KingOfTheEtherThrone smart contract[EB].

[23] 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. 2016: 254-269.

[24] KING J C. Symbolic execution and program testing[J]. Communications of the ACM, 1976, 19(7): 385-394.

[25] CLARKE E M, GRUMBERG O, PELED D. Model checking[M]. MIT Press, 1999.

[26] BIBEL W. Automated theorem proving[M]. Wiesbaden: Vieweg+Teubner Verlag, 1987.

[27] Microsoft Corporation. The Z3 theorem prover[EB].

[28] MUELLER B. Smashing Ethereum smart contracts for fun and real profit[C]//In 9th Annual HITB Security Conference (HITBSecConf). 2018.

[29] NIKOLI? I, KOLLURI A, SERGEY I, et al. Finding the greedy, prodigal, and suicidal contracts at scale[C]//Proceedings of the 34th Annual Computer Security Applications Conference. 2018: 653-663.

[30] MOSSBERG M, MANZANO F, HENNENFENT E, et al. Manticore: a user-friendly symbolic execution framework for binaries and smart contracts[C]//Proceedings of 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2019: 1186-1189.

[31] KRUPP J, ROSSOW C. TEETHER: gnawing at Ethereum to automatically exploit smart contracts[C]//Proceedings of 27th USENIX Security Symposium. 2018: 1317-1333.

[32] PERMENEV A, DIMITROV D, TSANKOV P, et al. VerX: safety verification of smart contracts[C]//Proceedings of 2020 IEEE Symposium on Security and Privacy. 2020: 1661-1677.

[33] TORRES C F, SCHüTTE J, STATE R. Osiris: hunting for integer bugs in Ethereum smart contracts[C]//Proceedings of the 34th Annual Computer Security Applications Conference. 2018: 664-676

[34] TORRES C F, STEICHEN M. The art of the scam: demystifying honeypots in Ethereum smart contracts[C]//Proceedings of the 28th USENIX Security Symposium. 2019: 1591-1607.

[35] CHEN T, ZHANG Y F, LI Z H, et al. TokenScope: automatically detecting inconsistent behaviors of cryptocurrency tokens in ethereum[C]//Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. 2019: 1503-1520.

[36] TSANKOV P, DAN A, DRACHSLER-COHEN D, et al. Securify: practical security analysis of smart contracts[C]//Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 2018: 67-82.

[37] ULLMAN J D. Principles of database and knowledge-base systems[J]. Computer Science, 1988.

[38] JORDAN H, SCHOLZ B, SUBOTI? P. Soufflé: on synthesis of program analyzers[C]//Computer Aided Verification. 2016: 422-430.

[39] KALRA S, GOEL S, DHAWAN M, et al. ZEUS: analyzing safety of smart contracts[C]//Proceedings 2018 Network and Distributed System Security Symposium. 2018: 1-12.

[40] FEIST J, GRIECO G, GROCE A. Slither: a static analysis framework for smart contracts[C]//Proceedings of 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). 2019: 8-15.

[41] TIKHOMIROV S, VOSKRESENSKAYA E, IVANITSKIY I, et al. SmartCheck: static analysis of ethereum smart contracts[C]//Pro- ceedings of 2018 IEEE/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). 2018: 9-16.

[42] SCHNEIDEWIND C, GRISHCHENKO I, SCHERER M, et al. Ethor: practical and provably sound static analysis of Ethereum smart contracts[C]//Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. 2020: 621-640.

[43] GRECH N, KONG M, JURISEVIC A, et al. MadMax: surviving out-of-gas conditions in Ethereum smart contracts[J]. Proceedings of the ACM on Programming Languages, 2018, 2: 1-27.

[44] HOLZMANN G J, CHECKER S M. The: primer and reference manual[J]. Septiembre del, 2003.

[45] BENGTSSON J, LARSEN K, LARSSON F, et al. UPPAAL—a tool suite for automatic verification of real-time systems[C]//International Hybrid Systems Workshop. 1995: 232-243.

[46] CAVADA R, CIMATTI A, JOCHIM C A, et alNusmv 2.4 user manual[J]. CMU and ITC-IRST, 2005.

[47] NEHA? Z, PIRIOU P Y, DAUMAS F. Model-checking of smart contracts[C]//Proceedings of 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data. 2018: 980-987.

[48] ABDELLATIF T, BROUSMICHE K L. Formal verification of smart contracts based on users and blockchain behaviors models[C]//Proceedings of 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS). 2018: 1-5.

[49] BAI X M, CHENG Z J, DUAN Z B, et al. Formal modeling and verification of smart contracts[C]//Proceedings of the 2018 7th International Conference on Software and Computer Applications. 2018: 322-326.

[50] ANDRYCHOWICZ M, DZIEMBOWSKI S, MALINOWSKI D, et al. Modeling bitcoin contracts by timed automata[C]//International Conference on Formal Modeling and Analysis of Timed Systems. 2014: 7-22.

[51] SERGEY I, HOBOR A. A concurrent perspective on smart contracts[C]//International Conference on Financial Cryptography and Data Security. 2017: 478-493.

[52] BARTOLETTI M, ZUNINO R. BitML: a calculus for bitcoin smart contracts[C]//Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 2018: 83-100.

[53] LANEVE C, COEN C S, VESCHETTI A. On the prediction of smart contracts’ behaviors[M]//From Software Engineering to Formal Methods and Tools, and Back. 2019: 397-415.

[54] QU M X, HUANG X, CHEN X, et al. Formal verification of smart contracts from the perspective of concurrency[C]//International Conference on Smart Blockchain. Springer, Cham, 2018: 32-43.

[55] ROSCOE A W. Understanding concurrent systems[M]. London: Springer London, 2010.

[56] LI X Y, SU C, XIONG Y, et al. Formal verification of BNB smart contract[C]//Proceedings of 2019 5th International Conference on Big Data Computing and Communications (BIGCOM). 2019: 74-78.

[57] WANG D, HUANG X, MA X F. Formal analysis of smart contract based on colored petri nets[J]. IEEE Intelligent Systems, 2020, 35(3): 19-30.

[58] LIU Z T, LIU J. Formal verification of blockchain smart contract based on colored petri net models[C]//Proceedings of 2019 IEEE 43rd Annual Computer Software and Applications Conference. 2019: 555-560.

[59] The coq proof assistant reference manual[EB].

[60] NIPKOW T, WENZEL M, PAULSON L C. Isabelle/HOL[M]. Berlin, Heidelberg: Springer, 2002.

[61] HIRAI Y. Defining the Ethereum virtual machine for interactive theorem provers[C]//International Conference on Financial Cryptography and Data Security. 2017: 520-535.

[62] MULLIGAN D P, OWENS S, GRAY K E, et al. Lem: reusable engineering of real-world semantics[J]. ACM SIGPLAN Notices, 2014, 49( 9): 175-188．

[63] ANNENKOV D, NIELSEN J B, SPITTERS B. ConCert: a smart contract certification framework in Coq[C]// Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2020: 215-228.

[64] BHARGAVAN K, DELIGNAT-LAVAUD A, FOURNET C, et al. Formal verification of smart contracts: short paper[C]//Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. 2016: 91-96.

[65] AMANI S, BéGEL M, BORTIN M, et al. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL[C]//Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2018: 66-77.

[66] YANG Z, LEI H. FEther: an extensible definitional interpreter for smart-contract verifications in coq[J]. IEEE Access, 2019, 7: 37770-37791.

[67] YANG Z, LEI H. Lolisa: formal syntax and semantics for a subset of the solidity programming language[J]. arXiv: 1803.09885, 2008.

[68] LI X M, SHI Z P, ZHANG Q Y, et al. Towards verifying ethereum smart contracts at intermediate language level[M]//Formal Methods and Software Engineering. 2019: 121-137.

[69] SERGEY I, KUMAR A, HOBOR A. Temporal properties of smart contracts[C]//International Symposium on Leveraging Applications of Formal Methods. 2018: 323-338.

[70] SUN T Y, YU W S. A formal verification framework for security issues of blockchain smart contracts[J]. Electronics, 2020, 9(2): 255.

[71] SWAMY N, HRI?CU C, KELLER C, et al. Dependent types and multi-monadic effects in F[C]//Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2016: 256-270.

[72] GRISHCHENKO I, MAFFEI M, SCHNEIDEWIND C. A semantic framework for the security analysis of Ethereum smart contracts[C]//Principles of Security and Trust. 2018: 243-269.

[73] STEF?NESCU A, PARK D, YUWEN S J, et al. Semantics-based program verifiers for all languages[J]. ACM SIGPLAN Notices, 2016, 51(10): 74-91.

[74] HILDENBRANDT E, SAXENA M, RODRIGUES N, et al. KEVM: a complete formal semantics of the Ethereum virtual machine[C]//Proceedings of 2018 IEEE 31st Computer Security Foundations Symposium. 2018: 204-217.

[75] JIAO J, KAN S L, LIN S W, et al. Semantic understanding of smart contracts: executable operational semantics of solidity[C]//Pro- ceedings of 2020 IEEE Symposium on Security and Privacy. 2020: 1695-1712.

[76] SERGEY I, KUMAR A, HOBOR A. Scilla: a smart contract intermediate-level language[J]. arXiv preprint arXiv:1801.00687, 2018.

[77] REYNOLDS J C. Definitional interpreters for higher-order programming languages[C]//Proceedings of the ACM Annual Conference. 1972: 717-740.

[78] MAVRIDOU A, LASZKA A. Designing secure ethereum smart contracts: a finite state machine based approach[C]//Financial Cryptography and Data Security, 2018: 523-540.

[79] MAVRIDOU A, LASZKA A. Tool demonstration: FSolidM for designing secure Ethereum smart contracts[C]//International Conference on Principles of Security and Trust. 2018: 270-277.

[80] MAVRIDOU A, LASZKA A, STACHTIARI E, et al. VeriSolid: Correct-by-design smart contracts for Ethereum[C]//International Conference on Financial Cryptography and Data Security. 2019: 446-465.

[81] GROSSMAN S, ABRAHAM I, GOLAN-GUETA G, et al. Online detection of effectively callback free objects with applications to smart contracts[J]. Proceedings of the ACM on Programming Languages, 2018, 2: 1-28.

[82] XUE Y X, MA M L, LIN Y, et al. Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart contracts[C]//Proceedings of 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2020: 1029-1040.

[83] BARTOLETTI M, ZUNINO R. Verifying liquidity of Bitcoin contracts[C]//8th International Conference on Principles of Security and Trust, POST 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software. 2019: 222-247.

[84] KOLLURI A, NIKOLIC I, SERGEY I, et al. Exploiting the laws of order in smart contracts[C]//Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 2019: 363-373.

[85] JIANG B, LIU Y, CHAN W K. ContractFuzzer: fuzzing smart contracts for vulnerability detection[C]//Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. 2018: 259-269.

[86] NGUYEN T D, PHAM L H, SUN J, et al. sFuzz: an efficient adaptive fuzzer for solidity smart contracts[C]//Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering. 2020: 778-788.

[87] LI A, CHOI J A, LONG F. Securing smart contract with runtime validation[C]//Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 2020: 438-453.

[88] BIGI G, BRACCIALI A, MEACCI G, et al. Validation of decentralised smart contracts through game theory and formal methods[M]//Programming Languages with Applications to Biology and Security. Springer, Cham, 2015: 142-161.

[89] 田國華, 胡云瀚, 陳曉峰. 區(qū)塊鏈系統(tǒng)攻擊與防御技術(shù)研究進展[J]. 軟件學(xué)報, 2021, 32(5): 1495-1525.

TIAN G H, HU Y H, CHEN X F. Research progress on attack and defense techniques in block-chain system[J]. Journal of Software, 2021, 32(5): 1495-1525.

[90] DELMOLINO K, ARNETT M, KOSBA A,et alStep by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab[C]//International conference on Financial Cryptography and Data Security. 2016: 79-94.

[91] CHEN H S, PENDLETON M, NJILLA L, et al. A survey on Ethereum systems security[J]. ACM Computing Surveys, 2021, 53(3): 1-43.

[92] DURIEUX T, FERREIRA J F, ABREU R, et al. Empirical review of automated analysis tools on 47, 587 Ethereum smart contracts[C]//Proceedings of 2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE). 2020: 530-541.

[93] DI ANGELO M, SALZER G. A survey of tools for analyzing Ethereum smart contracts[C]//Proceedings of 2019 IEEE International Conference on Decentralized Applications and Infrastructures. 2019: 69-78.

[94] IMERI A, AGOULMINE N, KHADRAOUI D. Smart Contract modeling and verification techniques: a survey[C]//Proceedings of the 8th International Workshop on ADVANCEs in ICT Infrastructures and Services (ADVANCE 2020). 2020: 1-8.

[95] PARIZI R M, DEHGHANTANHA A. Smart contract programming languages on blockchains: An empirical evaluation of usability and security[C]//International Conference on Blockchain. 2018: 75-91.

[96] GRISHCHENKO I, MAFFEI M, SCHNEIDEWIND C. Foundations and tools for the static analysis of Ethereum smart contracts[C]//International Conference on Computer Aided Verification. 2018: 51-78.

[97] TOLMACH P, LI Y, LIN S W, et al. A survey of smart contract formal specification and verification[J]. ACM Computing Surveys, 2021, 54(7): 1-38.

[98] 錢鵬, 劉振廣, 何欽銘, 等. 智能合約安全漏洞檢測技術(shù)研究綜述[J]. 軟件學(xué)報, 2022, 33(8): 3059-3085.

QIAN P, LIU Z G, HE Q M. Smart Contract vulnerability detection technique: a survey[J]. Journal of Software, 2022, 33(8): 3059-3085.

[99] 章峰, 史博軒, 蔣文保. 區(qū)塊鏈關(guān)鍵技術(shù)及應(yīng)用研究綜述[J]. 網(wǎng)絡(luò)與信息安全學(xué)報, 2018, 4(4): 22-29.

ZHANG F, SHI B X, JIANG W B. Review of key technology and its application of blockchain[J]. Chinese Journal of Network and Information Security, 2018, 4(4): 22-29.

[100] 朱健, 胡凱, 張伯鈞. 智能合約的形式化驗證方法研究綜述[J]. 電子學(xué)報, 2021, 49(4): 792-804.

ZHU J, HU K, ZHANG B J. Review on formal verification of smart contract[J]. Acta Electronica Sinica, 2021, 49(4): 792-804.

[101] Ethereum Foundation. The serpent contract-oriented programming language[EB].

[102] Lisp-Like language[EB].

[103] CHEN T, LI X Q, LUO X P, et al. Under-optimized smart contracts devour your money[C]//Proceedings of 2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering. 2017: 442-446.

[104] O'CONNOR R. Simplicity: a new language for blockchains[C]//Pro- ceedings of the 2017 Workshop on Programming Languages and Analysis for Security. 2017: 107-120.

[105] YAMASHITA K, NOMURA Y, ZHOU E C, et al. Potential risks of hyperledger fabric smart contracts[C]//Proceedings of 2019 IEEE International Workshop on Blockchain Oriented Software Engineering. Piscataway: 2019: 1-10.

[106] BECKERT B, HERDA M, KIRSTEN M, et al. Formal specification and verification of Hyperledger Fabric chaincode[C]//3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM. 2018: 44-48.

State-of-the-art survey of smart contract verification based on formal methods

ZHANG Wenbo1,2, CHEN Simin1,WEI Lifei1, SONG Wei1, HUANG Dongmei3

1. College of Information Technology, Shanghai Ocean University, Shanghai 201306, China 2. Shanghai Key Laboratory of Trustworthy Computing, Shanghai 200062, China 3. Shanghai University of Electric Power, Shanghai 201306, China

Smart contract represents an essential application scenario of blockchain technology. Smart contract technology improves programmability and scalability of blockchain, and has broad development prospects. However, a series of security incidents caused a great number of economic losses and weakened users’ confidence in the Ethereum platform. The security of smart contract has become a critical problem that restricts the further development of smart contract. Defects in smart contract code may cause serious consequences and cannot be modified once deployed, it is especially important to verify the correctness of smart contract in advance. In recent years, researchers have obtained many achievements in verification of smart contract, but there is a lack of systematic summary of these research results. Therefore, some basic principles of Ethereum were introduced, including the transaction, gas mechanism, storage and programming language. Eight common types of vulnerabilities in smart contract were summarized and their causes were explained. Some real security events were reviewed and some examples of vulnerability codes were presented. Then, the research work on automatic verification of smart contract based on symbolic execution, model checking and theorem proving was classified and summarized. Three open-source automated tools were selected, including Mythril, Slither and Oyente. And experiments were implemented to evaluate and compare the three tools from the aspects of efficiency, accuracy and the types of vulnerability can be detected. Furthermore, related review articles were surveyed, and the advantages of this paper compared with these works were summarized. The critical problems in the vulnerability detection technology of smart contract were also summarized and the direction of future research was proposed at last.

smart contract, formal methods, blockchain, Ethereum, program verification

The National Natural Science Foundation of China (61872142, 62102243, 61972241), Shanghai Sailing Program (21YF1417000), The Open Project of Shanghai Key Laboratory of Trustworthy Computing, Shanghai Natural Science Foundation (18ZR1417300), The Program for the Capacity Development of Shanghai Local Colleges (20050501900), Startup Foundation for Young Teachers of Shanghai Ocean University

張文博, 陳思敏, 魏立斐, 等. 基于形式化方法的智能合約驗證研究綜述[J]. 網(wǎng)絡(luò)與信息安全學(xué)報, 2022, 8(4):12-28.

TP393

A

10.11959/j.issn.2096?109x.2022041

張文博（1992?），男，河南洛陽人，博士，上海海洋大學(xué)講師，主要研究方向為形式化驗證、理論計算機科學(xué)。

陳思敏（1998?），女，安徽合肥人，上海海洋大學(xué)碩士生，主要研究方向為形式化驗證、區(qū)塊鏈。

魏立斐（1982?），男，浙江紹興人，博士，上海海洋大學(xué)副教授，主要研究方向為密碼學(xué)與云計算安全。

宋巍（1977?），女，山西大同人，博士，上海海洋大學(xué)教授、博士生導(dǎo)師，主要研究方向為計算機視覺、海洋大數(shù)據(jù)分析、軟件工程等。

黃冬梅（1964?），女，河南鄭州人，上海電力大學(xué)教授、博士生導(dǎo)師，主要研究方向為大數(shù)據(jù)分析、機器學(xué)習(xí)及智能服務(wù)。

2022?05?16；

2022?07?04

黃冬梅，dmhuang@shou.edu.cn

國家自然科學(xué)基金（61872142，62102243，61972241）；上海市青年科技英才揚帆計劃（21YF1417000）；上海市高可信計算重點實驗室開放課題；上海市自然科學(xué)基金面上項目（18ZR1417300）；上海市科委部分地方高校能力建設(shè)項目（20050501900）；上海海洋大學(xué)青年教師科研啟動項目

ZHANG W B, CHEN S M, WEI L F, et al. State-of-the-art survey of smart contract verification based on formal methods[J]. Chinese Journal of Network and Information Security, 2022, 8(4): 12-28.