以太坊智能合約安全形式化驗(yàn)證方法研究進(jìn)展

王赫彬，鄭長(zhǎng)友，黃 松，孫金磊，丁一先

(1.中國(guó)人民解放軍陸軍工程大學(xué) 指揮控制工程學(xué)院，江蘇 南京 210007；2.中國(guó)人民解放軍陸軍工程大學(xué) 全軍軍事訓(xùn)練軟件測(cè)評(píng)中心，江蘇 南京 2100073.遼寧工程技術(shù)大學(xué)，遼寧 阜新 123000)

0 引 言

自2009年Satoshi Nakamoto的比特幣發(fā)布以來，出現(xiàn)了各種各樣的區(qū)塊鏈實(shí)現(xiàn)。而自從2013年底Vitalik Buterin發(fā)布的以太坊白皮書將智能合約的概念引入到區(qū)塊鏈之中，區(qū)塊鏈技術(shù)的應(yīng)用變得更加廣泛，并使得比特幣等加密貨幣的可編程能力更進(jìn)一步。智能合約提供了一個(gè)框架，允許以可信任、去中心化的方式執(zhí)行一個(gè)應(yīng)用程序的業(yè)務(wù)邏輯。智能合約用戶通常攜帶大量的價(jià)值數(shù)以億計(jì)的貨幣，但是智能合約作為一種計(jì)算機(jī)代碼可能具有未發(fā)現(xiàn)的和未知的漏洞，具有很大的安全隱患。2016年6月17日的The DAO攻擊事件中，一名攻擊者利用去中心化自治組織(decentralized autonomous organization，DAO)部署的智能合約代碼中的多個(gè)漏洞，控制了當(dāng)時(shí)價(jià)值約為5 000萬美元的以太坊網(wǎng)絡(luò)，并從合約中盜走了350多萬以太幣；2018年美鏈BEC上百億項(xiàng)目歸零、BAI(blockchain of artificial intelligence and internet of things)任意賬戶無限轉(zhuǎn)賬都是因?yàn)镋RC20代幣標(biāo)準(zhǔn)中出現(xiàn)的一系列漏洞，導(dǎo)致資金惡意發(fā)送轉(zhuǎn)移，正常的礦工節(jié)點(diǎn)受到了危害。對(duì)于難以避免的智能合約安全性問題來說，在部署鏈上前發(fā)現(xiàn)并修復(fù)漏洞至關(guān)重要。

雖然現(xiàn)有的一些工作通過基于測(cè)試的檢測(cè)方法來檢測(cè)漏洞，但不能完備地發(fā)現(xiàn)智能合約源碼和字節(jié)碼中所有的漏洞，而且對(duì)于智能合約在一些概念和屬性的正確表達(dá)缺乏全面的檢查。而現(xiàn)有的一些代碼及合約審計(jì)工作則依賴于審計(jì)專家的個(gè)人經(jīng)驗(yàn)和主觀判斷，缺乏嚴(yán)謹(jǐn)性和說服力。形式化驗(yàn)證方法則通過證明序列、邏輯語句檢查數(shù)學(xué)模型的邏輯，以證明某些規(guī)范的正確性并發(fā)現(xiàn)運(yùn)行時(shí)錯(cuò)誤，理論上可以發(fā)現(xiàn)更多的漏洞。智能合約對(duì)于安全性要求高，代碼量相對(duì)較小，這些特點(diǎn)很適用于進(jìn)行小型的形式化驗(yàn)證。文中對(duì)以太坊智能合約的相關(guān)概念進(jìn)行了系統(tǒng)的介紹，分析了智能合約常見的漏洞類型，總結(jié)了常見的形式化驗(yàn)證方法，進(jìn)行了實(shí)驗(yàn)結(jié)果分析并討論了目前形式化驗(yàn)證工作存在的問題和挑戰(zhàn)，提出了將來的改進(jìn)方法及意見建議。

1 背景及相關(guān)概念介紹

1.1 以太坊智能合約

以太坊平臺(tái)于2015年提出，是使用區(qū)塊鏈平臺(tái)執(zhí)行智能合約的最流行的底層系統(tǒng)之一[1]。其市場(chǎng)容量達(dá)到了1 000億美元，每天處理超過40萬筆資金交易。以太坊包含以太坊虛擬機(jī)、執(zhí)行環(huán)境(賬戶管理、默克樹等)和共識(shí)算法三個(gè)部件，適用于公有鏈、私有鏈和聯(lián)盟鏈三種區(qū)塊鏈環(huán)境。不同的區(qū)塊鏈環(huán)境可以通過擴(kuò)展包的形式，將以太坊智能合約部署到鏈上。以太坊智能合約是部署在其平臺(tái)上的一種計(jì)算機(jī)協(xié)議，具有可編程、可維護(hù)和安全可信等特點(diǎn)[2]。特別地，智能合約的執(zhí)行過程是從一個(gè)狀態(tài)到另一個(gè)狀態(tài)[3]，可以用有限狀態(tài)機(jī)將智能合約形式化地表示為一個(gè)五元組自動(dòng)機(jī)Q*:

Q*=(Q0,Ω,ζ,t*,G*)

其中，Q0是合約執(zhí)行自動(dòng)機(jī)的所有狀態(tài)的集合，Ω為所有輸入事件的集合，ζ:Q0×Ω→Q0則是轉(zhuǎn)移函數(shù)的集合，t*∈Q0為初始狀態(tài),G*?Q0為終止?fàn)顟B(tài)集合。

1.1.1 以太坊虛擬機(jī)

智能合約通常用有別于現(xiàn)有編程語言的高級(jí)語言編寫，開發(fā)人員在編寫完智能合約代碼后，代碼被編譯成以太坊虛擬(Ethereum virtual machine，EVM)字節(jié)碼在計(jì)算機(jī)上執(zhí)行。EVM是一種完全基于堆棧的虛擬機(jī)架構(gòu)，支持一個(gè)包含134個(gè)操作碼的指令集，運(yùn)行在256比特的基本數(shù)據(jù)類型之上。與Java虛擬機(jī)(Java virtual machine，JVM)相比，EVM相對(duì)更加簡(jiǎn)單，執(zhí)行效果更加具有確定性。圖1是一個(gè)合約代碼被EVM編譯成字節(jié)碼的示例。

圖1 智能合約代碼編譯過程示例

1.1.2 智能合約語言

智能合約通常使用專門的智能合約語言進(jìn)行編寫[4]。智能合約語言包含高級(jí)語言、中間級(jí)語言(intermediate representation，IR)和低級(jí)語言三種類型。開發(fā)人員通常使用高級(jí)語言編寫智能合約，因?yàn)楦呒?jí)語言能夠提供期望的表達(dá)方式。IR語言介于高級(jí)語言和低級(jí)語言之間，可以用于編寫程序以推導(dǎo)屬性和檢查規(guī)范，也可以用于優(yōu)化代碼的結(jié)構(gòu)。而低級(jí)語言則提供了一種在分布式虛擬機(jī)上執(zhí)行的實(shí)現(xiàn)方式?；诤霞s語言不同的安全特性，可以采用不同的方法對(duì)合約進(jìn)行形式化驗(yàn)證。其中Solidity、Vyper是以太坊平臺(tái)常用的智能合約高級(jí)語言，EVM是其常用的低級(jí)語言，而EthIR和Yul是其常用的中間語言。

1.2 常用的形式化驗(yàn)證方法

形式化驗(yàn)證方法[5]是指在形式化建模的基礎(chǔ)上，對(duì)具有精確語法和語義的形式化語言的系統(tǒng)建立事務(wù)及性質(zhì)等的關(guān)系，從而驗(yàn)證系統(tǒng)所應(yīng)具有的功能正確性和其他關(guān)鍵性質(zhì)。

1.2.1 定理證明

定理證明[6]適用于很多系統(tǒng)，方法流程是對(duì)其進(jìn)行形式化規(guī)約，并將要證明的命題寫為“待驗(yàn)證系統(tǒng)滿足形式化規(guī)約”，從而將驗(yàn)證問題轉(zhuǎn)化為證明一個(gè)可滿足性問題，使用預(yù)先定義的公理和推理規(guī)則作為輸入來完成證明過程。定理證明分為交互式定理證明、自動(dòng)化定理證明和混合定理證明三種[7]，而不同類型系統(tǒng)的復(fù)雜度決定了不同定理證明方式的可行性。復(fù)雜度較小的可以使用自動(dòng)化定理證明，復(fù)雜度較大的則可以使用交互式定理證明。

1.2.2 模型檢測(cè)

模型檢測(cè)[8]是指對(duì)于一個(gè)協(xié)議框架利用邏輯公式進(jìn)行檢查，觀察該協(xié)議描述的需求或系統(tǒng)是否具有某些期望的性質(zhì)。通常需要驗(yàn)證的性質(zhì)包括安全性(safety)、活躍性(liveness)、無阻性(non-blocking)和非嚴(yán)格順序性(no strict sequencing)等。該方法適用于可以用有限狀態(tài)模型表示的系統(tǒng)。模型檢測(cè)器可以自動(dòng)化完成精準(zhǔn)模型和規(guī)范的檢測(cè)，給出可用的判斷結(jié)果。

1.3 常見的漏洞類型

隨著智能合約語言的迭代更新，不斷有新的漏洞被修復(fù)，但同時(shí)新的版本語言的語法也會(huì)帶來新的安全漏洞隱患。截至2020年8月，Solidity語言從0.3.x版本更新到了0.7.0版本。按照漏洞來源依賴，以太坊智能合約漏洞可以分為區(qū)塊鏈依賴漏洞、軟件安全依賴漏洞和以太坊及合約語言依賴漏洞[9]。圖2是一些以太坊智能合約的常見漏洞。

2 相關(guān)研究進(jìn)展

本節(jié)將介紹智能合約形式化驗(yàn)證的一些最新技術(shù)研究進(jìn)展。暫時(shí)沒有一個(gè)固定的標(biāo)準(zhǔn)對(duì)于這些形式化驗(yàn)證方法進(jìn)行分類，但是已經(jīng)有很多研究對(duì)于智能合約的正確設(shè)計(jì)和漏洞挖掘產(chǎn)生了效果。借鑒了1.2節(jié)傳統(tǒng)的形式化驗(yàn)證方法，可以采用以下幾種技術(shù)手段對(duì)智能合約進(jìn)行形式化驗(yàn)證。

2.1 類型推斷

基于類型推斷的形式化驗(yàn)證使用數(shù)十行或數(shù)百行的核心類型理論來替換智能合約語言的類型或類型子集，能夠用來快速證明數(shù)學(xué)定理。這種方法使用函數(shù)式程序語言，更多地關(guān)注類型檢查，而不是運(yùn)行程序，具有相對(duì)簡(jiǎn)單的語法。這種方法的一般流程為：首先將智能合約高級(jí)語言翻譯成函數(shù)式程序語言，指定源語言中的數(shù)據(jù)在驗(yàn)證語言中的數(shù)據(jù)格式和數(shù)據(jù)類型，并轉(zhuǎn)換包含這些數(shù)據(jù)的源語言中的函數(shù)；然后提出并證明關(guān)于這些函數(shù)的定理，可以完成運(yùn)行時(shí)程序正確性的驗(yàn)證。

微軟研究院和哈佛大學(xué)研究團(tuán)隊(duì)的Bhargavan等人[10]提出了一個(gè)用于形式化分析的F*框架，試圖通過將合約代碼翻譯成F*語言后，通過類型推斷來驗(yàn)證智能合約。該框架包括Solidity*和EVM*兩個(gè)工具原型，Solidity*支持Solidity的部分語法類型轉(zhuǎn)換，將智能合約從Solidity語言翻譯成F*語言，EVM*再從EVM字節(jié)碼形式反編譯成F*語言。轉(zhuǎn)換過程中支持遞歸，不支持循環(huán)。Solidity*運(yùn)用類型推導(dǎo)發(fā)現(xiàn)運(yùn)行時(shí)函數(shù)和變?cè)腻e(cuò)誤和違反的規(guī)范，EVM*則可以分析低層次的屬性，估算gas消耗的上界。驗(yàn)證了396份合約，其中46份成功地進(jìn)行了翻譯和類型檢查，發(fā)現(xiàn)了一些可重入漏洞和未經(jīng)檢查的send語句返回調(diào)用問題。

Coblenz等人[11]研發(fā)的Obsidian是一種面向類型的安全區(qū)塊鏈編程語言，該語言以用戶為中心，用戶實(shí)驗(yàn)反饋與語言開發(fā)同時(shí)進(jìn)行，類型狀態(tài)依賴系統(tǒng)保證了程序員編寫正確的合約。針對(duì)可用操作依賴的高級(jí)狀態(tài)、代碼錯(cuò)誤導(dǎo)致的資金損失或挪用和不一致狀態(tài)導(dǎo)致的重入攻擊等三種嚴(yán)重的bug源，類型狀態(tài)會(huì)將動(dòng)態(tài)信息記錄到類型之中，之后進(jìn)行靜態(tài)的類型推斷，同時(shí)，線性類型系統(tǒng)計(jì)算貨幣的數(shù)量，完成對(duì)于交易過程中的財(cái)務(wù)信息追蹤溯源。

Schrans等人[12]開發(fā)了一種專門用于編寫魯棒性智能合約的靜態(tài)類型編程語言Flint，引入保護(hù)塊(protection blocks)根據(jù)類型狀態(tài)限制運(yùn)行代碼的時(shí)間和用戶，對(duì)于狀態(tài)的寫入進(jìn)行了限制，簡(jiǎn)化了合約的推理。具有調(diào)用保護(hù)、默認(rèn)不變量、資產(chǎn)類型推理和安全語義等安全特性，實(shí)現(xiàn)了安全的內(nèi)部及外部資金轉(zhuǎn)移(asset transfer)、事件監(jiān)控和安全的算術(shù)運(yùn)算等代碼保護(hù)功能，通過限制交易過程中的類型狀態(tài)，將Solidity語言的安全性進(jìn)行了提升，避免了智能合約重入漏洞和整數(shù)溢出等問題的出現(xiàn)。目前，智能合約交互語言Rholang[13]和Plutus[14]分別使用ρ演算和λ演算等抽象演算方法，完成了一些驗(yàn)證工作。

2.2 交互式定理證明

智能合約的交互式定理證明是傳統(tǒng)的定理證明方法在智能合約驗(yàn)證中的應(yīng)用。智能合約高級(jí)語言如Solidity和低級(jí)語言如EVM上的字節(jié)碼需要被定義成可以為定理證明器編譯的語言，然后再利用交互式定理證明驗(yàn)證以太坊智能合約的安全性質(zhì)。定理證明器也可以選擇用一些自動(dòng)化SMT定理證明器，SMT求解器使用一階邏輯語言來表示命題，然后通過枚舉賦值的方式進(jìn)行證明?？蓾M足命題的賦值為程序提供正確的輸入，可以證明在執(zhí)行路徑中給定的狀態(tài)是可達(dá)的。

Amani等[15]研發(fā)的eth-isabelle是一種作用于EVM字節(jié)碼的Isabelle/HOL定理證明器。首先將EVM字節(jié)碼序列語義用Lem語言形式化構(gòu)造成線性代碼塊，將EVM指令劃分為以JUMPDEST為開始的基本塊、JUMP、JUMPI等跳轉(zhuǎn)指令以及其他指令基本塊三種，然后再翻譯到Isabelle/HOL或Coq中進(jìn)行定理證明。基于以太坊的gas機(jī)制給出了一種out-of-gas異常處理方法，使用分離邏輯(separation logic)驗(yàn)證以太坊虛擬內(nèi)存中的字節(jié)碼程序，支持使用程序規(guī)則、基本塊規(guī)則和指令規(guī)則自動(dòng)生成驗(yàn)證條件和驗(yàn)證規(guī)范，降低了EVM操作碼形式智能合約形式化驗(yàn)證的時(shí)間復(fù)雜度。

Lei等[16]提出的Lolisa是Solidity語言的一個(gè)大型子集的形式化語法和語義，采用了更魯棒的靜態(tài)類型系統(tǒng)，不僅包含了Solidity中映射符、修改器、合約類型和地址類型等語法組件，而且還包含了諸如多個(gè)返回值、指針?biāo)惴ㄒ约敖Y(jié)構(gòu)和字段訪問等通用編程語言特性?；赟olidity語言的可擴(kuò)展性，提出將Lolisa擴(kuò)展到其他合約編程語言的方案。接著開發(fā)了一種支持不同驗(yàn)證范式的可擴(kuò)展、可重用的形式化內(nèi)存框架GREM，模擬了物理內(nèi)存的硬件結(jié)構(gòu)，并且使用Coq提供了一套防干擾的應(yīng)用程序編程接口(application programming interfaces，API)，實(shí)現(xiàn)了一個(gè)獨(dú)立可定制的框架。之后開發(fā)的執(zhí)行時(shí)驗(yàn)證同構(gòu)體(execution verification isomorphism，EVI)將符號(hào)執(zhí)行與定理證明結(jié)合，提高了高階邏輯定理證明輔助工具的自動(dòng)化程度，并且證明了Lolisa可滿足于EVI。

Yang等人[17]開發(fā)的FEther編譯器是一種基于Coq的混合定理證明工具，基于Solidity語言的形式化語法和語義子集Lolisa，結(jié)合符號(hào)執(zhí)行和高階邏輯定理證明，提高了執(zhí)行和驗(yàn)證合約的自動(dòng)化程度，同時(shí)FEther具有很好的可重用性，可以將驗(yàn)證過的代碼片段復(fù)用檢查其他代碼段的屬性，其運(yùn)行效率遠(yuǎn)遠(yuǎn)超過Coq標(biāo)準(zhǔn)教程中的解釋器。是第一個(gè)在Coq中對(duì)于Solidity語言進(jìn)行語法和語義定義的證明引擎。Annenkov等人[18]提出了一個(gè)基于Coq的框架ConCert，可以對(duì)于智能合約進(jìn)行形式化證明鑒定。

Sergey等[19]研發(fā)的中間語言Scilla提供了一個(gè)編程組件，為智能合約間的通信提供了一個(gè)計(jì)算與交互的分離、效率和純計(jì)算的分離及調(diào)用動(dòng)作和連續(xù)過程的分離等，允許豐富的交互模式，具有規(guī)則形式寫成的語義，將Scilla嵌入Coq之中，易于進(jìn)行形式化驗(yàn)證。描述了基于自動(dòng)機(jī)[20]的Scilla模型，展示了自動(dòng)機(jī)關(guān)于安全和時(shí)間等屬性的簡(jiǎn)化驗(yàn)證過程。除了Coq和Isabelle/HOL等工具外，Why3[21]也實(shí)現(xiàn)了EVM的語義表示，可以基于EVM字節(jié)碼進(jìn)行一些智能合約的定理證明。

2.3 有界模型檢測(cè)

智能合約的模型檢測(cè)中常用的方法為有界模型檢測(cè)(bounded model check，BMC)，有界模型檢查器系統(tǒng)地、象征性地研究系統(tǒng)的行為，直到某個(gè)邊界k，尋找對(duì)給定屬性的違反，其中邊界k表示允許從某個(gè)初始狀態(tài)進(jìn)行的轉(zhuǎn)換的數(shù)量。使用單個(gè)邏輯語句檢查智能合約的性質(zhì)及規(guī)范，若合約狀態(tài)轉(zhuǎn)移符合規(guī)范，則證明智能合約滿足所驗(yàn)證的安全特性；否則構(gòu)造模型檢測(cè)器會(huì)構(gòu)造一個(gè)狀態(tài)轉(zhuǎn)移的反例，證明合約違反了該條規(guī)范，存在安全性問題。

牛津大學(xué)的Antonino等[22]開發(fā)了一種基于Solid語言的有界模型檢測(cè)工具Solidifier，Solid語言對(duì)于Solidity語言和以太坊區(qū)塊鏈進(jìn)行形式化描述，之后將Solid轉(zhuǎn)換成中間語言Boogie[23]，使用Corral[24]對(duì)于Boogie語言形式的合約進(jìn)行有界模型檢測(cè)。提出合約驗(yàn)證和函數(shù)驗(yàn)證兩種工具，定義main過程和捕獲Solid調(diào)用結(jié)構(gòu)的callP過程，探索區(qū)塊鏈的行為，尋找合約錯(cuò)誤。通過特定代碼模式匹配或未預(yù)料到的行為方式，查找不符合開發(fā)人員意圖的程序錯(cuò)誤及狀態(tài)。

Joel等[26]開發(fā)了一種基于符號(hào)執(zhí)行的有界模型檢測(cè)工具ETHBMC，設(shè)定了Keccak256函數(shù)、Memcopy-like指令和Inter-Contract交互等測(cè)試斷言，建立了以太坊的攻擊模型、內(nèi)存模型和數(shù)據(jù)調(diào)用模型等，然后符號(hào)執(zhí)行檢測(cè)模塊中的漏洞，對(duì)于每個(gè)具有易受攻擊的路徑生成交易過程實(shí)例。通過對(duì)于當(dāng)前go-ethereum區(qū)塊鏈工具套件中活躍的大約220萬個(gè)用戶大規(guī)模分析，自動(dòng)生成5 905個(gè)觸發(fā)漏洞的有效輸入，與之前的分析方法相比較，具有22.8%的更多輸入。

Zhang等[27]開發(fā)了一個(gè)用4 800多行Python和C++寫成的有界模型檢測(cè)工具NPCHECKER，處理Solidity及Vyper語言的不確定性對(duì)于合約付款等交易過程的影響。發(fā)現(xiàn)由于不可預(yù)測(cè)的事務(wù)調(diào)度和外部未知的被調(diào)用者行為而讀寫更改的合約全局變量，公開了各種不確定性因素和問題。NPCHECKER的工作流程為：首先將EVM字節(jié)碼反編譯，然后利用內(nèi)聯(lián)匯編將匯編指令轉(zhuǎn)換成LLVM，恢復(fù)控制流圖，最后使用SMACK[28]和Boogie等模型檢測(cè)工具檢查恢復(fù)的IR代碼中是否含有NPⅠ和NPⅡ兩種付款bug。在以太坊主網(wǎng)上收集到3萬多份在線合約并對(duì)其進(jìn)行了評(píng)估。NPCHECKER在1 111份合約中檢測(cè)到不確定性支付，識(shí)別了六種未知的新漏洞類型。目前，NuSMV[29]、SPIN[30]等傳統(tǒng)的模型檢測(cè)工具被用于能源交易市場(chǎng)、網(wǎng)上購物等智能合約，完成需求規(guī)范開發(fā)階段和最終系統(tǒng)驗(yàn)證集成階段的交互驗(yàn)證。

2.4 其他驗(yàn)證方法

除了以上研究深入廣泛的以太坊智能合約形式化驗(yàn)證方法外，根據(jù)以太坊智能合約框架的性質(zhì)用途和工作流程，還有很多結(jié)合緊密的驗(yàn)證方法產(chǎn)生更加具有領(lǐng)域自適應(yīng)性的應(yīng)用。本節(jié)介紹幾種在主流的智能合約形式化驗(yàn)證之上有所改進(jìn)的方法。

2.4.1 用戶和區(qū)塊鏈行為建模

傳統(tǒng)的模型檢測(cè)方法可以對(duì)智能合約及其用戶進(jìn)行建模，但是不能對(duì)底層的區(qū)塊鏈進(jìn)行建模。Abdellatif等[31]提出了一種對(duì)于區(qū)塊鏈及其用戶進(jìn)行建模的方法，按照行為交互優(yōu)先級(jí)(behavior interaction priorities，BIP)使用統(tǒng)計(jì)型模型檢測(cè)器(statistical model checking，SMC)進(jìn)行驗(yàn)證。對(duì)于給定的系統(tǒng)B和性質(zhì)δ，SMC模型檢測(cè)器使用概率有界線性時(shí)序邏輯(probabilistic bounded linear time logic，PB-LTL)來判斷B是否滿足δ。令B滿足δ記為B|=δ，首先判斷公式：

P({B|=δ})>θ

是否成立，其中P(.)為某個(gè)事件發(fā)生的概率，θ為某個(gè)選定的閾值；然后估算P({B|=δ})的值p，使得估計(jì)值p0滿足：

P(|p-p0|≤α)≥1-β

其中，α為估計(jì)精度，β為攻擊風(fēng)險(xiǎn)水平。運(yùn)用該方法能夠發(fā)現(xiàn)傳統(tǒng)模型檢測(cè)方法難以發(fā)現(xiàn)的易受攻擊用戶行為和交易路徑。

2.4.2 博弈論

Giancarlo等[32]提出了一種利用博弈論(game theory)來對(duì)涉及物理行為的智能合約進(jìn)行驗(yàn)證的方法。首先通過博弈論分析交易過程中顧客和商家的行為，觀察兩方行為的相互影響，然后使用概率模型檢測(cè)器PRISM通過分析顧客和商家不確定的選擇行為對(duì)于選擇事件對(duì)應(yīng)的概率的影響，將行為建模成離散時(shí)間馬爾可夫決策過程(discrete time Markov decision process，DTMDP)，來解決不確定性問題。根據(jù)顧客的誠實(shí)度和商家的信譽(yù)使用了六種存款與出售價(jià)格比率，對(duì)于一組誠實(shí)的顧客與不誠實(shí)的商家，商家損失30%的可能性不大于2%，顧客損失30%的可能性卻可以達(dá)到50%。

2.4.3 著色Petri網(wǎng)

Wang等[33]改進(jìn)了字節(jié)碼的程序邏輯規(guī)則，應(yīng)用霍爾條件(Hoare condition)建立了著色Petri網(wǎng)(colored Petri Nets，CPN)模型。首先，對(duì)于Solidity源代碼形式的智能合約，利用ANTLR語法分析器建立抽象語法樹(abstract syntax tree，AST)模型并解析抽象語法樹中的元素，生成等價(jià)的CPN模型；然后，對(duì)于EVM字節(jié)碼形式的智能合約，對(duì)于字節(jié)碼序列對(duì)應(yīng)的操作語義進(jìn)行靜態(tài)分析，劃分出具有不同特征的基本塊，構(gòu)建控制流圖(control flow graph，CFG)，生成等價(jià)的CPN模型。最后，將之前建立的CPN模型放入CPN工具中完成動(dòng)態(tài)仿真和模型檢測(cè)。該方法設(shè)計(jì)了一種自動(dòng)化的建模方法，引入了一個(gè)自定義調(diào)用庫和一種基于回溯的路徑推導(dǎo)算法，提高了傳統(tǒng)模型檢測(cè)方法的針對(duì)性和有效性。

2.4.4 K框架

K框架[34]是一種可執(zhí)行的程序框架語義集，可以用于形式化智能合約，對(duì)事務(wù)進(jìn)行狀態(tài)和網(wǎng)絡(luò)演化進(jìn)行建模，并使用轉(zhuǎn)換規(guī)則來詳細(xì)闡述狀態(tài)的修改和網(wǎng)絡(luò)的演化。K框架在邏輯上可以分成三個(gè)模塊:data.k,language.k和ethereum.k，目的是與以太坊的依賴結(jié)構(gòu)保持一致。Hildenbrandt等[35]在K框架中定義了一個(gè)EVM的語義—KEVM，將EVM表示成K框架范式中的ENBF樣式提供的語言語法、狀態(tài)配置描述和驅(qū)動(dòng)程序執(zhí)行的轉(zhuǎn)換規(guī)則三個(gè)主要組件，深入解釋了KEVM的結(jié)構(gòu)定義描述，然后給出了幾種語義擴(kuò)展，根據(jù)ERC20標(biāo)準(zhǔn)驗(yàn)證了標(biāo)準(zhǔn)代幣的兩種不同語言實(shí)現(xiàn)，使用K框架的可達(dá)性邏輯證明器，表現(xiàn)了KEVM語義框架的可用性。此外，該框架還可用于gas消耗分析和解析以太坊白皮書中EVM的語言規(guī)范等。KVyper[36]由Vyper到LLL、LLL到EVM兩個(gè)翻譯器組成，可用于發(fā)現(xiàn)Vyper編譯器中存在的錯(cuò)誤。KSolidity[37]是K框架中Solidity語義的定義，可用于Solidity語言合約測(cè)試。

除此之外，ZEUS[38]和Oyente[39]也使用形式化驗(yàn)證的方法分別在源碼級(jí)和操作碼級(jí)進(jìn)行了自動(dòng)化的漏洞檢測(cè)，并發(fā)現(xiàn)了一些以太坊智能合約存在的安全漏洞。

3 總結(jié)與展望

3.1 現(xiàn)有研究存在的不足

如第二節(jié)所述，智能合約形式化驗(yàn)證工具發(fā)展迅速，但是仍有一些缺陷，主要問題如下：

(1)合約語言不完整。不同的形式化驗(yàn)證方法通常能夠驗(yàn)證合約語言的一個(gè)子集，而不能完整地驗(yàn)證所有智能合約可能出現(xiàn)的問題。總結(jié)一些常用形式化驗(yàn)證方法對(duì)于智能合約的處理，如表1所示。

表1 智能合約形式化驗(yàn)證框架/工具對(duì)比分析

可以看出，很多語言只能處理合約語言的一個(gè)語義語法子集，如FEther基于Solidity語言的Lolisa子集進(jìn)行證明，不能對(duì)整個(gè)Solidity語言進(jìn)行驗(yàn)證，查找漏洞的手段較少，發(fā)現(xiàn)漏洞的類型不足。有些待驗(yàn)證的規(guī)范可能包含類型特性子集之外的語義語法元素，導(dǎo)致難以驗(yàn)證智能合約滿足的性質(zhì)及規(guī)范。擴(kuò)展可驗(yàn)證的合約語言子集，建立更多的驗(yàn)證范式，發(fā)現(xiàn)更多的漏洞類型是一個(gè)需要解決的技術(shù)問題。

(2)應(yīng)用范圍受限。由于智能合約仍是一個(gè)較新的領(lǐng)域，因此形式化驗(yàn)證缺乏一個(gè)統(tǒng)計(jì)評(píng)價(jià)標(biāo)準(zhǔn)和最佳實(shí)踐，方法應(yīng)用沒有突破高昂成本、合約規(guī)模等技術(shù)局限。文中選取了106個(gè)Solidity源碼合約樣本結(jié)合偷以太幣(Steal Ether)、黑杰克(Hijack)和自毀(Suicidal)三種攻擊行為，對(duì)Solidifier和ETHBMC兩種有界模型檢測(cè)工具檢查效果進(jìn)行對(duì)比，其編譯通過率和漏報(bào)率結(jié)果如表2所示。三種工具都存在較多的問題漏報(bào)的情況。此外，形式化驗(yàn)證還只適用于簡(jiǎn)化的合約模型，采用的啟發(fā)式方法難以擴(kuò)展到復(fù)雜的合約中去。自動(dòng)化程度不高，且缺乏對(duì)于高階業(yè)務(wù)邏輯范式的證明。

(3)驗(yàn)證語言安全性未知。在驗(yàn)證的過程中，通常需要將源代碼形式或字節(jié)碼形式的合約翻譯成另一種語言，例如F*方法，但是驗(yàn)證語言的安全性沒有得到保證，具有很大的安全隱患。翻譯過程的正確性也是未知的，很有可能出現(xiàn)轉(zhuǎn)換前后的類型有很大差別。因此證明或提高驗(yàn)證語言的安全性及翻譯過程的正確性是形式化驗(yàn)證面臨的一些重難點(diǎn)工作。

3.2 未來研究方向和改進(jìn)思路

針對(duì)現(xiàn)有工具存在的問題，提出如下未來改進(jìn)思路：

(1)擴(kuò)展形式化驗(yàn)證方法的應(yīng)用范圍。由于缺乏測(cè)試判定準(zhǔn)則(test oracles)，驗(yàn)證好壞通常難以衡量。所以需要建立標(biāo)準(zhǔn)的測(cè)試判定用例集，對(duì)于驗(yàn)證方法的有效性進(jìn)行定性定量評(píng)估。通過建立綜合評(píng)價(jià)指標(biāo)體系，找出實(shí)踐性好的驗(yàn)證方法及工具，有助于在此基礎(chǔ)上對(duì)智能合約的形式化驗(yàn)證進(jìn)行改進(jìn)和提高。通過與符號(hào)執(zhí)行、污點(diǎn)分析等方法的結(jié)合，提高形式化驗(yàn)證方法的自動(dòng)化程度，創(chuàng)建可重用的驗(yàn)證模式庫，減少驗(yàn)證所需時(shí)間，增強(qiáng)合約驗(yàn)證方法的可用性。

(2)提高形式化驗(yàn)證方法的驗(yàn)證效果。針對(duì)智能合約形式化驗(yàn)證過程不直觀的問題，可以通過類型標(biāo)記、著色Petri網(wǎng)等增強(qiáng)合約驗(yàn)證的可視化效果，利用逆向工程重新構(gòu)造合約執(zhí)行的控制流圖。根據(jù)以太坊智能合約具有的一些性質(zhì)和用途，建立具有嚴(yán)謹(jǐn)可靠數(shù)學(xué)基礎(chǔ)的區(qū)塊鏈模型和智能合約機(jī)制模型，提高以太坊平臺(tái)合約驗(yàn)證的效果。

4 結(jié)束語

以太坊為代表的智能合約平臺(tái)的出現(xiàn)擴(kuò)展了區(qū)塊鏈的資金轉(zhuǎn)移能力，促進(jìn)了區(qū)塊鏈2.0時(shí)代的到來。文中梳理了以太坊智能合約常用的語言和常見的漏洞類型，討論了基于類型推斷的形式化驗(yàn)證、智能合約的交互式定理證明和智能合約的有界模型檢測(cè)等主流的智能合約形式化驗(yàn)證方法，通過對(duì)幾種現(xiàn)有形式化驗(yàn)證工具的實(shí)驗(yàn)結(jié)果分析研究發(fā)現(xiàn)，并針對(duì)現(xiàn)有方法的不足之處，提出了未來研究的改進(jìn)思路。下一步工作的重點(diǎn)和難點(diǎn)在于根據(jù)以太坊智能合約的實(shí)現(xiàn)機(jī)制、環(huán)境狀態(tài)和網(wǎng)絡(luò)演化等內(nèi)部性質(zhì)用途，提出具有自適應(yīng)性的理論著力提高驗(yàn)證的準(zhǔn)確性，減少時(shí)間和空間成本，擴(kuò)展驗(yàn)證的適用范圍，進(jìn)一步提高以太坊智能合約的安全開發(fā)部署能力。