葉昊榀，劉 陽

(南京財(cái)經(jīng)大學(xué)信息工程學(xué)院，江蘇 南京 210023)

1 引言

近年來區(qū)塊鏈技術(shù)得到了快速的發(fā)展與推廣。作為可編程金融的區(qū)塊鏈2.0時(shí)代的代表技術(shù)[1]，智能合約在不遠(yuǎn)的未來將得到大量的推廣與應(yīng)用。智能合約無需可信中介、可以控制并處理大量的數(shù)字資產(chǎn)與交易，具有很高的經(jīng)濟(jì)價(jià)值。截至目前，市面上最為流行的智能合約應(yīng)用平臺以太坊的市值已經(jīng)超過1800億美元、完成了6.75億次交易。智能合約極高的經(jīng)濟(jì)價(jià)值也吸引了大量的不法分子利用智能合約本身存在的漏洞實(shí)施非法攻擊從而竊取數(shù)字資產(chǎn)。據(jù)相關(guān)研究表明，目前約有89%的智能合約都含有安全性漏洞，保守估計(jì)這些安全性漏洞所導(dǎo)致的損失已超過20億美元[2]。為了給智能合約提供高層次的保障性，使用形式化方法對智能合約進(jìn)行驗(yàn)證成為了許多學(xué)者的選擇。Nicola Atzei等人[3]從Solidity語言、EVM和區(qū)塊鏈三個(gè)層次對以太坊智能合約所存在的安全性隱患進(jìn)行了總結(jié)。Joshua Ellul 和 Gordon Pace[4]展示了如何在智能合約領(lǐng)域中應(yīng)用運(yùn)行時(shí)驗(yàn)證的標(biāo)準(zhǔn)化技術(shù)。胡凱等人[5]提出了一種可以應(yīng)用于智能合約生命周期的形式化驗(yàn)證框架和驗(yàn)證方法。Anastasia Mavridou[6]提出了用于智能合約形式化驗(yàn)證的VeriSolid框架、該框架同樣支持對合約函數(shù)體進(jìn)行建模。Anton Permenev等人[7]提出了VERX，能夠證明以太坊智能合約的函數(shù)屬性的自動驗(yàn)證器。Thomas Osterlanda等人[8]提出對Solidity語言的語義語法的形式化定義，并提出了一種將Solidity語言建模為PROMELA模型的轉(zhuǎn)換方法。Zheng Yang等人[9]發(fā)展并證明了一種用于證明以太坊智能合約的可靠性與安全性的全新的形式化符號進(jìn)程虛擬機(jī)。Giancarlo Bigi等人[10]通過將博弈論與形式化方法整合在一起的方式對智能合約進(jìn)行了驗(yàn)證。Sukrit Kalra等人[11]提出了一個(gè)用于驗(yàn)證智能合約的安全性和公平性的框架——ZEUS。Tesnim Abdellatif等人[12]提出了一種全新的形式化建模方法以驗(yàn)證智能合約在其執(zhí)行環(huán)境中的行為。Xiaomin BAI等人[13]介紹了形式化建模方法和形式化驗(yàn)證方法。

現(xiàn)有研究鮮有關(guān)注智能合約的函數(shù)性質(zhì)的成果。本文通過將隨機(jī)性引入到對合約函數(shù)的建模過程中，將函數(shù)建模為DTMC，實(shí)現(xiàn)了已有方法的改進(jìn)，提供了對合約運(yùn)行過程中可能產(chǎn)生的隨機(jī)性現(xiàn)象的關(guān)注；同時(shí)本文通過添加標(biāo)識符的方式提供了對break語句和continue語句的支持，實(shí)現(xiàn)了對以太坊智能合約所有控制語句的支持，進(jìn)一步提升了算法的適用范圍；通過對合約函數(shù)常用語句提供特定的處理方式提升了算法處理函數(shù)語句的能力。最終，本文的方法實(shí)現(xiàn)了更加普適地將智能合約的函數(shù)建模為DTMC并進(jìn)行驗(yàn)證的目標(biāo)。

2 建模智能合約函數(shù)

智能合約的實(shí)際功能是通過函數(shù)的觸發(fā)和運(yùn)行而得以實(shí)現(xiàn)的，因而智能合約在函數(shù)運(yùn)行時(shí)的狀態(tài)是值得研究的。同樣的，一些惡意攻擊者也會利用合約函數(shù)的漏洞破壞函數(shù)的原子性與隔離性，對合約狀態(tài)產(chǎn)生影響、從中非法牟利。

本文希望通過使用隨機(jī)模型檢驗(yàn)的方式來建模合約函數(shù)并實(shí)現(xiàn)對函數(shù)的性質(zhì)的驗(yàn)證，從而為智能合約的相關(guān)性質(zhì)提供保障。

2.1 概覽

為了實(shí)現(xiàn)以隨機(jī)模型檢驗(yàn)的方法建模并驗(yàn)證智能合約函數(shù)的函數(shù)體語句，本文將Mavridou A等人[6]的杰出工作進(jìn)行了拓展，實(shí)現(xiàn)了將智能合約函數(shù)的函數(shù)體語句建模為DTMC，并為函數(shù)體語句提供了更加全面的支持。

2.2 智能合約與隨機(jī)性

要將智能合約的函數(shù)建模為DTMC，需要解決兩大問題：合約函數(shù)是否擁有狀態(tài)和遷移？合約函數(shù)在運(yùn)行時(shí)是否伴隨隨機(jī)性現(xiàn)象？

首先回答合約函數(shù)是否擁有狀態(tài)與遷移。已有的相關(guān)研究[6]和Solidity官方文檔均已表明合約函數(shù)是可以擁有狀態(tài)與遷移的。

再回答合約函數(shù)在運(yùn)行時(shí)是否會伴隨隨機(jī)性現(xiàn)象。以太坊智能合約在設(shè)計(jì)時(shí)被限定為確定性的、非隨機(jī)的，其本身不會造成隨機(jī)性現(xiàn)象。但合約函數(shù)在運(yùn)行過程中會與環(huán)境產(chǎn)生交互，由于環(huán)境的不確定性，將會產(chǎn)生隨機(jī)現(xiàn)象。例如，由于環(huán)境產(chǎn)生的參數(shù)不確定，合約函數(shù)在收到不同的參數(shù)時(shí)，可能會觸發(fā)函數(shù)體內(nèi)不同的語句塊，從而造成函數(shù)運(yùn)行結(jié)果的不同，最終造成函數(shù)輸出狀態(tài)的差異。因此，合約函數(shù)在運(yùn)行時(shí)是伴隨著隨機(jī)性現(xiàn)象的。

基于此，認(rèn)為智能合約的函數(shù)是可以被建模為DTMC的。

2.3 將合約函數(shù)建模為DTMC

2.3.1 智能合約函數(shù)簡介

智能合約中聲明函數(shù)的語法如下：

function functionName (datatype dataName)public payable modifierName()returns (dataType){ …}

若函數(shù)沒有返回值，則“returns (dataType)”可以省略。函數(shù)名后緊跟的括號內(nèi)為輸入?yún)?shù)類型及參數(shù)名。modifierName()表示函數(shù)修飾器，其可以改變函數(shù)的行為。pubic為函數(shù)可見性，智能合約的函數(shù)可以分為public(external)和internal兩種，前者不僅可以被其它合約調(diào)用，而internal函數(shù)僅可在本合約內(nèi)部運(yùn)行，即通過本合約的public函數(shù)調(diào)用而觸發(fā)運(yùn)行。

而require(condition)語句是目前最常用的條件判定語句，當(dāng)condition表達(dá)式的值為false時(shí)，合約狀態(tài)將自動回滾至該條require語句所在函數(shù)執(zhí)行前的狀態(tài)。基于該性質(zhì)，require語句被大量的合約用于判定合約狀態(tài)是否滿足函數(shù)的觸發(fā)條件。

2.3.2 遷移概率的假設(shè)

本文的研究是在已有的將智能合約函數(shù)的函數(shù)體語句建模為有限狀態(tài)機(jī)的工作[6]上繼續(xù)進(jìn)行的，其將函數(shù)體語句的運(yùn)行作為產(chǎn)生新狀態(tài)的判定依據(jù)，通過對函數(shù)體語句進(jìn)行分類，每執(zhí)行一個(gè)特定的語句，便生成特定數(shù)量的狀態(tài)和遷移。工作以此為基礎(chǔ)，通過如下假設(shè)向遷移中加入了概率，以實(shí)現(xiàn)對隨機(jī)性現(xiàn)象的考察。

假設(shè)一：在函數(shù)運(yùn)行的某一狀態(tài)中，其遷移概率是平均分布的。

對于合約函數(shù)而言，只有選擇、循環(huán)等控制語句可能造成函數(shù)狀態(tài)的分支；其余情況下，合約語句都是順序執(zhí)行的。因此，在對合約函數(shù)建模的過程中，如下圖1所示，函數(shù)的大多數(shù)狀態(tài)都只有一個(gè)后繼狀態(tài)，因而其遷移概率先天為1，滿足設(shè)立的假設(shè)；對于由控制結(jié)構(gòu)生成的狀態(tài)遷移，如下圖2所示，由于可能產(chǎn)生若干N個(gè)后繼狀態(tài)，因而其遷移概率為1/N，這樣的假設(shè)固然十分簡陋，卻可以為研究提供很大的幫助，有能力驗(yàn)證合約函數(shù)的隨機(jī)性質(zhì)。而如何獲得更加接近現(xiàn)實(shí)的概率則有待于進(jìn)一步的研究。

圖1 非控制語句對應(yīng)產(chǎn)生的順序狀態(tài)遷移

圖2 控制語句生成的分支結(jié)構(gòu)狀態(tài)遷移

2.3.3 對調(diào)用函數(shù)語句的簡易支持

智能合約的函數(shù)同其它編程語言一樣，智能合約函數(shù)也可以實(shí)現(xiàn)對其它函數(shù)的調(diào)用。本文將合約函數(shù)中調(diào)用了函數(shù)的語句分為兩類處理：

1)調(diào)用的是public類型的函數(shù)，將其作為普通的順序語句處理。因?yàn)榭梢詫ublic函數(shù)單獨(dú)建模驗(yàn)證處理，因此為了簡化問題，這里不再將函數(shù)中調(diào)用的public函數(shù)展開建模；

2)調(diào)用了internal函數(shù)，對這類調(diào)用又可細(xì)分為兩種情況：

a)對于諸如用于if(condition)中條件判定語句的調(diào)用，不進(jìn)行展開；

b)其它情況則將進(jìn)行展開處理，即對internal函數(shù)的語句進(jìn)行建模；

通過這樣的處理，文中的方法實(shí)現(xiàn)了對合約函數(shù)中調(diào)用函數(shù)語句將的簡易支持。

2.3.4 控制語句的全面支持

智能合約Solidity語言的控制結(jié)構(gòu)共有if、else、while、do、for、break、continue、return等8種，Mavridou A[6]的工作未提供對do、break、continue語句的支持。文中的工作提供了對這三種控制結(jié)構(gòu)的支持，從而實(shí)現(xiàn)了對合約語言控制結(jié)構(gòu)的全面支持。

其中在處理do語句時(shí)，借鑒了文獻(xiàn)[6]對while語句的處理方法，這里不做贅述。

continue語句用于跳過本次循環(huán)體中余下尚未執(zhí)行的語句，立即進(jìn)行下一次的循環(huán)條件判定；break語句用于在循環(huán)結(jié)構(gòu)中結(jié)束本層循環(huán)體。設(shè)立了一個(gè)標(biāo)識符loop以確定函數(shù)執(zhí)行break或是continue語句時(shí)合約處于第幾層循環(huán)。在建模開始時(shí)，loop=0，其后隨著算法的運(yùn)行、建模過程的推進(jìn)，每進(jìn)入一層循環(huán)，置loop=loop+1；同樣的，沒處理完一層循環(huán)體的語句，便置loop=loop -1。通過這樣一個(gè)簡單的方式，可以明晰所處理的語句位于哪一層循環(huán)體，從而實(shí)現(xiàn)算法可以正確的建立對應(yīng)狀態(tài)的遷移、實(shí)現(xiàn)了對break語句和continue語句的支持。

2.3.5 require語句的處理

如前所述，大量智能合約的函數(shù)使用require語句以判定合約狀態(tài)是否可以觸發(fā)合約函數(shù)。對此本文將require語句作為一種特殊的語句進(jìn)行了處理的細(xì)化。

對于require(conditon)語句，若conditon語句為真，則合約函數(shù)將運(yùn)行下一語句；否則將回滾至合約函數(shù)運(yùn)行之前的狀態(tài)。因此將對require語句進(jìn)行了如下處理：

如下圖3，設(shè)函數(shù)的初始狀態(tài)為Sinit，當(dāng)前狀態(tài)為Sin，當(dāng)條件不滿足時(shí)，狀態(tài)回滾，則增加遷移Sin→Sinit，并記遷移概率為Prevert；當(dāng)條件滿足時(shí)，新增狀態(tài)S′，增加遷移Sin→S′，遷移概率為1-Prevert。本文中，在概率平均分布的假設(shè)之下，有Prevert=1-Prevert=0.5。

圖3 require語句建模效果圖

2.3.6 建模流程簡介

在介紹完本文所做工作后，介紹一下使用本文算法對合約函數(shù)的函數(shù)體語句建模流程。由于本文的工作是直接對合約函數(shù)建模，因而使用本文方法對函數(shù)建模的流程與原研究有所不同。具體的建模步驟總結(jié)如下：

1)按順序?qū)⒑霞s函數(shù)的修飾器語句加入到合約函數(shù)的函數(shù)體之中；

2)確定觸發(fā)、輸出狀態(tài)并調(diào)用算法：若函數(shù)不包含require語句或函數(shù)未改變其require中條件語句包含的變量值，則新增狀態(tài)S0，以p=1，loop=0調(diào)用算法functionAugment(S0，S0，S0，1，stmts)；否則新增狀態(tài)S0，S1，以p=1，loop=0調(diào)用算法functionAugment(S0，S0，S1，1，stmts)，其中stmts為函數(shù)體語句。

該算法將函數(shù)體語句分為12類，每類對應(yīng)相應(yīng)的轉(zhuǎn)換方式。這里限于篇幅將僅展示算法中的部分類別語句，完整的算法可以通過復(fù)制并訪問https:∥pan.baidu.com/s/11nQRSezd6ajQdJrcsztQDA，提取碼67p9獲得。

算法X.functionAugment(SINIT，SIN，SOUT，pIN，stmt)

1)if loop=0:

2)functionAugment(SINIT，SIN，SOUT，PIN，stmt，SIN，SOUT);

3): functionAugment(SINIT，SIN，SOUT，PIN，stmt，SIN，SOUT，S[loop]loopInit，S[loop]loopEnd);

算法X.functionAugment(SINIT，SIN，SOUT，PIN，stmt，SLOOPINIT，SLOOPEND)

1)if stmt is a require(condition)statement:{

2)add a transition SIN→ SINITwith probability P=PIN*(1-Prevert);

3)add a transition SIN→ SOUTwith probability P=PIN*Prevert;}

4)else if stmt is variable declaration statement ‖ event statement ‖expression statement:{…

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

為驗(yàn)證本文的提出的建模方法，首先將本文的算法應(yīng)用于部分智能合約的合約函數(shù)之中。囿于篇幅，這里只選取下節(jié)將用來驗(yàn)證性質(zhì)的3個(gè)函數(shù)進(jìn)行建模展示。

3.1 建模結(jié)果與分析

Mavridou A等人根據(jù)Solidity官方合約改編的blindAuction合約的withdraw函數(shù)與undid函數(shù)的代碼如下圖4、圖5所示，其生成DTMC的狀態(tài)遷移圖則如圖6、圖7所示。

需注意的是withdraw函數(shù)生成的DTMC中的三處遷移：S7→S8和S6→S8與unbid函數(shù)生成的DTMC中的S5→S6。這三處遷移對應(yīng)的是函數(shù)體中的transfer語句。正如Mavridou A等人在研究中的表述[6]，僅從生成的DTMC看，文獻(xiàn)的方法可以避免在執(zhí)行transfer等語句后對fallback函數(shù)的調(diào)用從而消除了“可重入性脆弱”。

圖4 文獻(xiàn)[6]中合約withdraw函數(shù)代碼

圖5 文獻(xiàn)[6]中合約unbid函數(shù)代碼

圖6 withdraw函數(shù)所生成DTMC

圖7 unbid函數(shù)所生成的DTMC

Solidity文檔中的blindAuction合約的withdraw函數(shù)的函數(shù)體語句代碼及函數(shù)體生成的DTMC分別如下圖8與圖9所示。由于這里的DTMC狀態(tài)相對較少，因此就很難看出是否存在“可重入性脆弱”。

圖8 blindAucion合約withdraw函數(shù)代碼

圖9 withdraw函數(shù)所生成的DTMC

3.2 驗(yàn)證生成的DTMC

對于智能合約函數(shù)而言，最易遭受的攻擊就是利用“可重入性”漏洞破壞函數(shù)原子性進(jìn)行的，對此，本文規(guī)約了一條PCTL公式以用于驗(yàn)證智能合約遭受利用“可重入性”漏洞的攻擊時(shí)是否安全：

對于智能合約而言，到達(dá)狀態(tài)r后，系統(tǒng)在到達(dá)狀態(tài)j之前不會到達(dá)狀態(tài)i：

(s=r)i，P-≤p.[(!(s=j))U(s=i)]

(1)

本文對此前生成的DTMC的最終得到驗(yàn)證結(jié)果如下表1所示。正如上一節(jié)所做的分析，文獻(xiàn)[6]中的兩個(gè)函數(shù)不存在可重入性漏洞，而Solidity文檔示例合約的函數(shù)也通過了驗(yàn)證。由于對以上合約函數(shù)進(jìn)行可重入性漏洞的安全性驗(yàn)證均得到了通過，為了驗(yàn)證方法的正確性，對Atzei N等人[3]提出的存在可重入性漏洞的實(shí)例合約SimpleDao進(jìn)行了建模驗(yàn)證，其未通過驗(yàn)證。該結(jié)果有力的證明了本文方法的正確性。

表1 函數(shù)“沒有可重入性漏洞”驗(yàn)證結(jié)果

4 結(jié)束語

本文基于已有研究，通過增加對隨機(jī)性的關(guān)注和合約控制語句的全覆蓋，提出了一種將智能合約的函數(shù)建模DTMC的方法。本方法首先通過向狀態(tài)遷移過程添加概率的方式實(shí)現(xiàn)了對隨機(jī)性現(xiàn)象的關(guān)注；其次，通過對函數(shù)類型的分類，提供了對函數(shù)調(diào)用語句的簡易支持；第三，增加了對break語句和continue語句的支持，實(shí)現(xiàn)了對智能合約所有控制語句的支持；最后，細(xì)化了前人研究的部分細(xì)節(jié)，對部分語句提供了差異化的處理方式，改進(jìn)了算法的處理效果。最終的實(shí)驗(yàn)結(jié)果表明，本文的方法可以實(shí)現(xiàn)將智能合約函數(shù)的函數(shù)體語句建模為DTMC、實(shí)現(xiàn)對智能合約全控制語句的支持等目標(biāo)。同時(shí)，本文對由智能合約所生成DTMC的性質(zhì)規(guī)約與驗(yàn)證的結(jié)果也表明了本文方法的正確性。