一種代幣智能合約的形式化建模與驗(yàn)證方法

歐陽恒一,熊 焰,黃文超

(中國科學(xué)技術(shù)大學(xué) a.網(wǎng)絡(luò)空間安全學(xué)院; b.計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,合肥 230026)

0 概述

智能合約是一種無需中介、自我驗(yàn)證、自動(dòng)執(zhí)行合約條款的計(jì)算機(jī)交易協(xié)議,近年來隨著區(qū)塊鏈技術(shù)的日益普及而備受關(guān)注。區(qū)塊鏈技術(shù)去中心化和數(shù)據(jù)防篡改等特性,解決了智能合約的信任問題,因此使得智能合約更適合在區(qū)塊鏈上進(jìn)行實(shí)現(xiàn)。智能合約[1-3]作為一種能自動(dòng)執(zhí)行合約條款的計(jì)算機(jī)程序,需要盡量避免語法和語義錯(cuò)誤,并且對(duì)于正確性及其他屬性具有較高要求,以保證用戶的財(cái)產(chǎn)安全。由于現(xiàn)有通過專家審計(jì)和人工復(fù)查生成可信合約代碼的方法很難確保代碼的絕對(duì)安全,因此導(dǎo)致智能合約存在安全隱患。2016年,惡意攻擊者通過以太坊Solidity[4]語言中的遞歸調(diào)用漏洞對(duì)運(yùn)行在以太坊公有鏈上的The DAO[2-3]智能合約進(jìn)行攻擊,導(dǎo)致360萬以太幣被盜。2017年,以太坊Parity電子錢包因多重簽名漏洞導(dǎo)致數(shù)億美元資金遭到凍結(jié)[5]。2018年,黑客利用ERC-20標(biāo)準(zhǔn)代幣合約整數(shù)溢出漏洞攻擊了美鏈BEC的智能合約,導(dǎo)致BEC貨幣急劇貶值,價(jià)值幾乎歸零。同年,BAI和EDU智能合約出現(xiàn)重大漏洞,其代幣(token)可被隨意轉(zhuǎn)走?？梢?智能合約已成為區(qū)塊鏈應(yīng)用安全的重災(zāi)區(qū),但是到目前為止能夠?qū)χ悄芎霞s漏洞進(jìn)行完備性和安全性分析的方法仍未被提出,當(dāng)前對(duì)于智能合約的安全保障主要依靠專家審計(jì)和人工復(fù)查,然而該方式不能保證代碼的絕對(duì)安全。

形式化方法[6]的本質(zhì)是基于數(shù)學(xué)的方法來描述目標(biāo)軟件系統(tǒng)屬性的一種技術(shù),適用于計(jì)算機(jī)軟硬件系統(tǒng)的規(guī)范、開發(fā)和驗(yàn)證。形式化驗(yàn)證[7]是使用基于數(shù)學(xué)變換的靜態(tài)分析方法來確定程序規(guī)范和代碼行為,如從協(xié)議規(guī)約出發(fā)驗(yàn)證程序的安全屬性等,其是目前安全級(jí)別最高的一種驗(yàn)證方法。為對(duì)智能合約漏洞進(jìn)行分析與研究,本文提出一種針對(duì)智能合約整數(shù)溢出漏洞的形式化建模與驗(yàn)證方法,先對(duì)合約代碼進(jìn)行建模分析,再利用形式化驗(yàn)證方法解決建模過程中的無限狀態(tài)問題。

1 相關(guān)研究

1.1 智能合約概念

智能合約概念由跨領(lǐng)域法律學(xué)者尼克·薩博于1995年提出,智能合約是一套以數(shù)字形式定義的承諾,包括合約參與方可以在上面執(zhí)行這些承諾的協(xié)議[8]。然而,受限于可編程的合約數(shù)字系統(tǒng),智能合約并未在當(dāng)時(shí)得到具體應(yīng)用。中本聰于2008年底在比特幣[9]系統(tǒng)中提出了區(qū)塊鏈概念。區(qū)塊鏈技術(shù)去中心化、防篡改、可編程和高可用等特性,解決了智能合約的信任問題。BUTERIN于2013年底發(fā)表《以太坊:下一代智能合約和去中心化應(yīng)用平臺(tái)》一文[10],致力于將以太坊打造成最佳智能合約平臺(tái),通過將智能合約與區(qū)塊鏈技術(shù)進(jìn)行融合,拓寬區(qū)塊鏈技術(shù)的應(yīng)用領(lǐng)域?？梢?以太坊已成為主流的智能合約開發(fā)和運(yùn)行平臺(tái)。

1.2 智能合約安全問題

智能合約是部署在區(qū)塊鏈系統(tǒng)上的有狀態(tài)的鏈上代碼。由于執(zhí)行代碼不能保證絕對(duì)安全,因此造成智能合約容易受到黑客攻擊。表1給出了4種智能合約漏洞引發(fā)的攻擊實(shí)例。智能合約除了面臨軟件安全性和可信性問題外,還存在以下問題:1)智能合約的不可篡改性使其一旦被部署上線,便無法進(jìn)行修改;2)智能合約的源碼公開導(dǎo)致其被惡意攻擊的成本大幅降低;3)智能合約在代碼開發(fā)過程中存在的Bug容易產(chǎn)生智能合約漏洞。由此可見,智能合約需要一種安全高效的審計(jì)方式來保障其安全性。

表1 智能合約攻擊實(shí)例Table 1 Attack examples of smart contract

1.3 形式化方法

為解決智能合約中存在的安全問題,本文引入形式化方法。形式化方法通常運(yùn)用數(shù)學(xué)歸納法驗(yàn)證目標(biāo)的完備性和安全性,主要包括:

1)基于類BAN邏輯的形式化方法[11]。該方法本質(zhì)上是基于知識(shí)和信念推理的模態(tài)邏輯分析方法,其從事先定義的公理出發(fā),通過一系列推理公理推證協(xié)議滿足安全性,但不能確保驗(yàn)證結(jié)果的可靠性。

2)基于模型檢驗(yàn)的形式化方法[12]。該方法是分析有窮狀態(tài)系統(tǒng)正確性的重要方法。BOREALE提出基于符號(hào)化模型檢驗(yàn)的形式化方法[13],該方法的基本思想是推遲實(shí)例化,在只進(jìn)行值的匹配或比較時(shí),才對(duì)變量進(jìn)行實(shí)例化。符號(hào)化方法可以緩解攻擊者生成無窮多個(gè)消息導(dǎo)致的狀態(tài)組合爆炸問題?，F(xiàn)有的智能合約形式化驗(yàn)證工作主要使用該方法對(duì)合約進(jìn)行檢驗(yàn)[14-15],但是其不能驗(yàn)證智能合約的完備性。

3)基于密碼學(xué)原語代數(shù)屬性的形式化方法。該方法能對(duì)含有代數(shù)運(yùn)算算子的協(xié)議或者合約進(jìn)行形式化驗(yàn)證,如文獻(xiàn)[16]給出了能對(duì)含有異或算子的一類無窮會(huì)話并發(fā)協(xié)議完成驗(yàn)證的方法。

4)基于定理證明的形式化方法。該方法將協(xié)議形式化描述為一系列邏輯子句,并通過歸納證明[17]和Applied Pi演算[18-19]等方式驗(yàn)證其相應(yīng)的安全屬性是得到滿足還是遭到破壞,該方法的主流驗(yàn)證工具包括Tamarin、ProVerif等,但是上述驗(yàn)證工具在驗(yàn)證過程中均需要人工輔助,且學(xué)習(xí)成本較高。SmartVerif[20]是一款支持全自動(dòng)形式化驗(yàn)證的工具。本文使用基于定理證明的SmartVerif形式化驗(yàn)證工具對(duì)模型進(jìn)行驗(yàn)證。

2 形式化建模與驗(yàn)證方法設(shè)計(jì)

為對(duì)代幣智能合約進(jìn)行形式化驗(yàn)證,需先對(duì)程序的一系列邏輯代碼進(jìn)行建模,再通過演算證明其相應(yīng)的安全屬性是得到滿足還是遭到破壞,但由于目前智能合約的形式化驗(yàn)證只針對(duì)單個(gè)協(xié)議進(jìn)行建模,因此無法對(duì)某類漏洞合約進(jìn)行建模,如整數(shù)溢出漏洞,并且因?yàn)橹悄芎霞s沒有固定的主函數(shù)入口,每個(gè)外部可見的函數(shù)都可被任意用戶進(jìn)行任意多次調(diào)用,所以建模后得到的模型狀態(tài)空間為無限大,驗(yàn)證時(shí)無法對(duì)所有情況進(jìn)行遍歷。針對(duì)以上問題,本文設(shè)計(jì)一種基于數(shù)學(xué)歸納法的形式化建模與驗(yàn)證方法。

2.1 模型角色

2.1.1 不誠實(shí)的用戶

在以太坊中有外部賬戶(Externally Owned Accounts,EOA)和合約賬戶(Contract Accounts,CA)兩種不同類型的賬戶,其共用一個(gè)地址空間,如圖1所示。外部賬戶由公鑰-私鑰對(duì)控制,即被分配給用戶,其地址由公鑰決定。合約賬戶由存儲(chǔ)在賬戶中的代碼控制,其地址在創(chuàng)建合約時(shí)確定。

圖1 外部賬戶與合約賬戶Fig.1 EOA and CA

以太坊中的賬戶包括隨機(jī)數(shù)(nonce)、賬戶余額(balance)、合約代碼(codeHash)和存儲(chǔ)(storageRoot)4個(gè)字段,其中只有合約賬戶才有代碼且存儲(chǔ)codeHash,即該賬戶的以太坊虛擬機(jī)代碼的哈希值,并且由于codeHash在生成后不可修改,因此意味著智能合約代碼也不可修改。外部賬戶可以觸發(fā)交易,而合約賬戶不能主動(dòng)發(fā)起交易,只能在被觸發(fā)后按預(yù)先編寫的智能合約代碼執(zhí)行,其交易流程如圖2所示。

圖2 外部賬戶與合約賬戶的交易流程Fig.2 Transaction process of EOA and CA

由于不誠實(shí)用戶可能是外部賬戶也可能是合約賬戶,因此本文構(gòu)建的模型角色需要包含兩個(gè)賬戶的功能。若不誠實(shí)的用戶是外部賬戶,則其惡意構(gòu)造函數(shù)會(huì)使轉(zhuǎn)賬邏輯中產(chǎn)生整數(shù)溢出漏洞,導(dǎo)致代幣的任意轉(zhuǎn)賬或無限增發(fā)。若不誠實(shí)的用戶是合約賬戶,則其會(huì)通過直接實(shí)現(xiàn)某段惡意代碼并等待智能合約轉(zhuǎn)賬,從而觸發(fā)合約代碼。當(dāng)調(diào)用外部合約或指定合約進(jìn)行外部調(diào)用時(shí),若此時(shí)外部調(diào)用被攻擊者劫持,則合約會(huì)執(zhí)行惡意代碼,包括利用fallback函數(shù)回調(diào),其等同于代碼重入攻擊,The DAO事件就是典型的重入攻擊實(shí)例。

2.1.2 合約自身及合約擁有者

因?yàn)楹霞s中存在一些函數(shù)只有合約擁有者才能調(diào)用執(zhí)行,所以模型建立時(shí)要有合約擁有者才能進(jìn)行后續(xù)建模。因此,本文需要對(duì)合約的擁有者進(jìn)行模型構(gòu)建,滿足合約中函數(shù)的正常調(diào)用執(zhí)行。

2.2 建模屬性

智能合約具有獨(dú)立運(yùn)行、不可篡改等特性。由于開發(fā)者可以自定義智能合約的交易邏輯并將其代碼發(fā)布在區(qū)塊鏈上,因此智能合約無法避免地存在與傳統(tǒng)程序類似的安全漏洞,但不同的是智能合約代碼運(yùn)行于開放的區(qū)塊鏈網(wǎng)絡(luò)且可被任意調(diào)用,合約執(zhí)行后具有不可篡改的特性,因此若有不誠實(shí)的用戶利用了合約漏洞,則會(huì)造成更大的危害。

本文主要針對(duì)智能合約的整數(shù)溢出漏洞進(jìn)行研究。整數(shù)溢出漏洞是一種常見的高危漏洞。因?yàn)橛?jì)算機(jī)中整型變量存在上下界,所以如果在算術(shù)運(yùn)算中結(jié)果超出其上下界,即整型變量最大或者最小表示范圍,則虛擬機(jī)會(huì)自動(dòng)截?cái)喔呶?導(dǎo)致運(yùn)算結(jié)果異常。典型的智能合約整數(shù)溢出漏洞事件有BEC、SMT、EDU和BAI等,惡意攻擊者通過構(gòu)造參數(shù)繞過合約中的檢測語句,使得轉(zhuǎn)賬邏輯中產(chǎn)生了整數(shù)溢出,導(dǎo)致代幣無限增發(fā)或任意轉(zhuǎn)賬。產(chǎn)生整數(shù)溢出漏洞的主要原因?yàn)橹苯油ㄟ^簡單的加減乘除等數(shù)值運(yùn)算操作,而未使用assert或require語句以保證運(yùn)算不產(chǎn)生整數(shù)溢出。

2.3 建模與驗(yàn)證流程

對(duì)于一個(gè)給定的智能合約C,本文提出一個(gè)將智能合約轉(zhuǎn)化為形式化模型的通用方法并對(duì)其進(jìn)行驗(yàn)證。智能合約的建模與驗(yàn)證流程如圖3所示。

圖3 智能合約的建模與驗(yàn)證流程Fig.3 Modeling and verification process of smart contract

2.3.1 切片

程序切片是對(duì)程序進(jìn)行理解和分析的常用技術(shù)?？紤]到直接利用合約進(jìn)行建模得到的模型狀態(tài)空間過大,不便于后續(xù)驗(yàn)證。因此,本文根據(jù)智能合約C={f1,f2,…,fx}和安全屬性φ生成切片準(zhǔn)則,在對(duì)合約進(jìn)行切片后得到簡化合約C={f′1,f′2,…,f′x}。

2.3.2 建模

本文建模后得到的模型為M={m′1,m′2,…,m′x},使用基于定理證明的SmartVerif形式化驗(yàn)證工具對(duì)其進(jìn)行驗(yàn)證。根據(jù)SmartVerif的建模要求,需要引入多重集合重寫規(guī)則。多重集合重寫規(guī)則為m′1三元組,記為l-[a]→r,其中,l代表一組前提或假設(shè),a代表待選的動(dòng)作或者行為,[a]表示動(dòng)作a的集合,r代表假設(shè)成立并采取動(dòng)作a后產(chǎn)生的結(jié)果。

本文主要的建模過程是將智能合約的各類語句轉(zhuǎn)換為多重集合重寫規(guī)則:

1)對(duì)于賦值語句,由于SmartVerif的模型語言暫不支持全局變量,為能對(duì)合約進(jìn)行建模,因此本文引入全局變量約束,具體如下:

1.restriction set_in:

2.“All x y #t3 .Exist(x,y)@t3==>

3.(Ex #t2 .Store(x,y)@t2 & #t2<#t3

4.& (All #t1 .Del(x)@t1==> (#t1<#t2 | #t3<#t1))

5.& (All #t1 yp .Store(x,yp)@t1==> (#t1<#t2#t1=#t2 | #t3<#t1))

6.)”

7.restriction set_notin:

8.“All x #t3 .NotExist(x)@t3 ==>

9.(All #t1 y .Store (x,y) @t1 ==> #t3<#t1)

10.(Ex #t1 .Del(x)@t1 & #t1<#t3

11.&(All #t2 y .Store(x,y)@t2 & #t2<#t3 ==> #tw<#t1))”

在全局變量約束中,Store(x,y)事件表示全局變量的賦值操作,Del(x)事件表示對(duì)全局變量做清空操作,Exist(x,y)表示獲取全局變量x的y值,Set_in約束表示Exist(x,y)操作獲得的y值需滿足以下條件:

(1)在Exist(x,y)操作前存在給x賦值的Store(x,y)事件。

(2)該Store(x,y)事件和Exist(x,y)事件之間不存在Del(x)事件。

(3)該Store(x,y)事件是距Exist(x,y)事件時(shí)間最近的一個(gè)Store(x,y)事件。

Set_notin約束與Set_in約束相反。在引入上述約束條件后,即可對(duì)全局變量進(jìn)行建模。

2)對(duì)于條件語句,由于SmartVerif的模型語言沒有實(shí)現(xiàn)數(shù)值比較的相關(guān)約束,因此本文引入數(shù)值比較約束,具體如下:

1.restriction predicate l:

2.“All #i a b.Pred_not_equals (a,b)@i==>not((a=b))”

3.restriction predicate 2:

4.“All #i a b.Pred_equals (a,b)@i==>(a=b)”

5.restriction predicate 3:

6.“All #i a b.Pred_not_Bigger(a,b)@i==>not(Ex c.(a=(b)+(c)))”

7.restriction predicate 4:

8.“All #i a b.Pred_Bigger (a,b)@i==>(Exc.(a=(b)+(c)))”

以predicate 4為例,當(dāng)Pred_Bigger(a,b)事件發(fā)生時(shí),一定存在a=b+c,其他約束也與此類似。

3)對(duì)于循環(huán)語句,本文只處理有界循環(huán),將其展開為條件語句和賦值語句的集合。

2.3.3 驗(yàn)證

因?yàn)橹悄芎霞s沒有固定的主函數(shù)入口,每個(gè)外部可見的函數(shù)都可被任意用戶進(jìn)行任意多次調(diào)用,所以建模后得到的模型狀態(tài)空間為無限大,驗(yàn)證時(shí)無法對(duì)所有情況進(jìn)行遍歷。本文借鑒數(shù)學(xué)歸納法的思想優(yōu)化模型驗(yàn)證過程:對(duì)于每個(gè)函數(shù),假設(shè)其安全屬性φ在運(yùn)行前成立,并通過驗(yàn)證工具判斷其在驗(yàn)證后是否成立。如果成立,則該函數(shù)的安全屬性得到證明,即此函數(shù)不存在溢出漏洞;反之,則證明此函數(shù)存在溢出漏洞,并可以得到反例。智能合約的抽象過程表示為:

1.while true

2.(user,func,args):= // arbitrary

3.run func (args) as user

3 實(shí)驗(yàn)結(jié)果與分析

3.1 整數(shù)溢出漏洞分析

通過對(duì)代幣合約FountainToken進(jìn)行建模分析后,找出以下代碼中的第12行和第14行為整數(shù)溢出漏洞:

1.function batchTransfers (address[] receivers,uint256[] amounts) {

2.uint receiveLegth = receivers.length;

3.requuire (receiveLength == amounts.length);

4.unit receiverCount = 0;

5.unit256 totalAmount = 0;

6.unit i;

7.address r;

8.for(i=0;i < receiveLength;i++) {

9.r=receivers[i];

10.if (r==address(0) || r==owner) continue;

11.receiverCount++;

12.totalAmount+=amounts[i];

13.}

14.require(totalAmount >0);

15.require(canPay(msg.sender,totalAmount)):

16.wallets[msg.sender]-=totalAmount;

17.unit256 amount;

18.for (i = 0; i

19.r=receivers[i];

20.if (r==address(0) || r==owner) continue;

21.amount = amounts[i];

22.if (amout == 0) continue;

23.wallets[r]=wallets[r].add(amount);

24.emit Transfer (msg.sender,r,amount);

25.}

26.return true;

27.}

分析發(fā)現(xiàn):由于該溢出漏洞的攻擊發(fā)生條件是amounts數(shù)組中的元素存在極大值,receivers數(shù)組中的地址賬戶余額為極小值,因此totalAmount在累加過程中會(huì)發(fā)生上溢出,最終wallets[msg.sender]只減少極小值,而receivers數(shù)組中某一地址r的wallets[r]余額增加為極大值,使得合約不具備本文定義的安全屬性φ。本文共對(duì)5個(gè)存在整數(shù)溢出漏洞的代幣智能合約進(jìn)行建模與驗(yàn)證,成功找出了其中的溢出漏洞,如表2所示。

表2 代幣智能合約的整數(shù)溢出漏洞Table 2 Integer overflow vulnerabilities of token smart contract

3.2 其他漏洞分析

本文提出的代幣智能合約形式化建模與驗(yàn)證方法同樣適用于其他類型的合約漏洞。以The DAO攻擊為例驗(yàn)證該建模方法對(duì)重入漏洞的有效性,發(fā)現(xiàn)不誠實(shí)的用戶利用重入漏洞攻擊代幣智能合約的主要目的是從賬戶中非法重復(fù)提取代幣,因此本文定義了安全屬性φ2:balanceu+etheru=balance′u+ether′u,其中,u表示任意賬戶,balanceu表示u的代幣余額,etheru表示u的以太幣余額,balance′u和ether′u表示任意一次交易后的兩類余額。通過驗(yàn)證該屬性可以發(fā)現(xiàn)當(dāng)合約存在重入漏洞時(shí),一定存在某次交易使得該安全屬性不成立。由此得出,本文提出的形式化建模與驗(yàn)證方法對(duì)智能合約的漏洞檢測具有通用性。

4 結(jié)束語

隨著智能合約應(yīng)用的快速增長,其頻發(fā)的安全事件嚴(yán)重威脅大眾經(jīng)濟(jì)財(cái)產(chǎn)安全。針對(duì)代幣智能合約的安全問題,本文提出一種形式化建模與驗(yàn)證方法。使用切片技術(shù)和基于數(shù)學(xué)歸納法的形式化驗(yàn)證方法,解決了狀態(tài)空間爆炸和函數(shù)無限調(diào)用問題。對(duì)5個(gè)存在整數(shù)溢出漏洞的代幣智能合約和The DAO攻擊進(jìn)行形式化建模與驗(yàn)證實(shí)驗(yàn),結(jié)果表明本文方法能成功找出代幣智能合約漏洞。下一步可將研究范圍擴(kuò)展至更多的智能合約及漏洞類型,通過歸納總結(jié)不同類型的漏洞得到其特有的安全屬性,從而實(shí)現(xiàn)智能合約的形式化建模與驗(yàn)證。