智能合約函數(shù)的建模與驗證研究

葉昊榀，劉 陽

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

1 引言

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

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

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

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

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

2.1 概覽

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

2.2 智能合約與隨機性

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

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

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

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

2.3.2 遷移概率的假設

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

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

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

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

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

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

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

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

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

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

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

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

2.3.4 控制語句的全面支持

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

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

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

2.3.5 require語句的處理

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

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

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

圖3 require語句建模效果圖

2.3.6 建模流程簡介

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

1)按順序將合約函數(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類，每類對應相應的轉換方式。這里限于篇幅將僅展示算法中的部分類別語句，完整的算法可以通過復制并訪問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ù)之中。囿于篇幅，這里只選取下節(jié)將用來驗證性質的3個函數(shù)進行建模展示。

3.1 建模結果與分析

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。這三處遷移對應的是函數(shù)體中的transfer語句。正如Mavridou A等人在研究中的表述[6]，僅從生成的DTMC看，文獻的方法可以避免在執(zhí)行transfer等語句后對fallback函數(shù)的調(diào)用從而消除了“可重入性脆弱”。

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

圖5 文獻[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 驗證生成的DTMC

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

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

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

(1)

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

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

4 結束語

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