區塊鏈拍賣退款交易智能合約DoS漏洞優化研究

摘 要：針對智能合約的DoS漏洞可能在拍賣退款交易中造成資源耗盡問題進行了研究，設計了拍賣退款交易中智能合約DoS漏洞優化方案。首先構造可能存在DoS漏洞的智能合約，然后采用增加映射以及壓棧出棧方法完成漏洞優化，最后通過形式化驗證運行優化后的智能合約，檢測其是否存在邏輯錯誤或不一致性。實驗結果表明，采用該方法優化的智能合約能夠避免因資源耗盡產生的拒絕服務，與帶有漏洞智能合約相比，優化后的智能合的等效內存使用量減少了約62.8%，運行時間也有縮短。

關鍵詞：智能合約；形式化驗證；拍賣退款；DoS漏洞

中圖分類號：TP393.08 文獻標志碼：A 文章編號：1001-3695（2023）02-004-0343-06

doi： 10.19734/j.issn.1001-3695.2022.07.0349

Research on DoS vulnerability optimization of blockchain auction refund transaction smart contract

Chen Hong， Wang Yinghui， Jin Haibo， Cao Yue

（College of Software， Liaoning Technical University， Huludao Liaoning 125105， China）

Abstract：Aiming at the problem that DoS vulnerabilities of smart contracts may cause resource exhaustion in auction refund transactions， this paper studied and designed an optimization scheme for DoS vulnerabilities of smart contracts in auction refund transactions. Firstly， it constructed a smart contract that might have DoS vulnerabilities， and then used the method of increasing mapping and pushing the stack out to complete vulnerability optimization. Finally， it ran the optimized smart contract through formal verification to detect whether there was logic errors or inconsistencies. The experimental results show that the smart contract optimized by this algorithm can avoid the denial of service caused by resource exhaustion. Compared with the smart contract with vulnerabilities， the equivalent memory usage of the optimized smart contract reduces about 62.8%， and the running time is shortened.

Key words：smart contract; formal verification; auction refund; DoS vulnerabilities

0 引言

1995年密碼學家尼科薩博提出了智能合約概念［1］，智能合約是能夠自動執行合約條款的計算機程序，由于其具有可信、去中心化特點被應用于區塊鏈中。智能合約能夠將合約參與者、合約協議以及參與者與協議之間復雜關系程序化。

智能合約漏洞分為語言、虛擬機以及區塊鏈三種層面漏洞［2，3］。DoS攻擊屬于智能合約語言層面的漏洞，該漏洞是一種網絡攻擊手法，其目的在于使目標的網絡或系統資源耗盡，使服務暫時中斷或停止，導致用戶無法訪問［4］。

智能合約和一般程序不同，因其不可竄改性，使得其無法通過打補丁方式來修復，一旦遭受攻擊，合約將無法被調用。如果在循環期間對另一個合約的調用或傳輸失敗，則使用for循環批量執行交易或更新的合約可能會被DoS攻擊。造成拒絕服務的原因很多，常見的如達到gas上限、意外自毀、通過制造大量無用數據使目的主機擁堵直至資源耗盡［5］。

從智能合約角度分析，該漏洞主要危害是雙重支付問題，雙重支付是指兩筆交易花費了同一筆資金。在拍賣退款交易中很容易因為DoS攻擊而使用戶交易費用被攻擊者轉移，產生金融詐騙，同時物理內存也全部被占用，造成交易終止或崩潰。

當智能合約的交易金額特別巨大，而同時發現合約上有較為明顯漏洞時，將導致巨額資產損失。近五年因智能合約安全問題引發了諸多攻擊事件。2016年6月，惡意攻擊者利用Solidity語言中的遞歸調用splitDAO漏洞，入侵以太坊公有鏈上作為智能合約執行的最大眾籌項目The DAO，導致超過6 000萬美元的以太幣被盜［6］；2017年，黑客利用Parity多重簽名錢包合約中的委托調用漏洞，獲取錢包地址的所有權并轉移內部資產，導致價值上億美元資金被凍結；2018年4月22日，BeautyChain出現安全漏洞，導致BEC損失64億人民幣［7］；同年4月28日，EOS被爆出可能存在BEC合約類似的安全漏洞，若此漏洞存在，則極大可能導致市場價值歸零，金融行業也因此蒙受較大損失；2020年8月，非法用戶利用存在漏洞的智能合約導致YAM項目暴跌致崩盤。

智能合約中的部分函數執行是依賴于外部調用結果，該情況下又沒有對外部返回的結果進行嚴格控制，比如返回結果非預期的處理，可能會引發一些安全事故［8，9］。例如DoS攻擊導致的KotET安全漏洞事件［10］。KotET是一款區塊鏈游戲的簡稱，該游戲通過用戶間抬高ether的方式互相競爭，最后決出優勝用戶。該智能合約中存在bid方法，該方法首先判斷了金額的大小，滿足條件后先將上一個用戶退位，再賦值新的優勝用戶。如果上一個用戶一直不退位，那么一直沒有新的用戶當選，就會造成系統拒絕服務，系統資源很可能會耗盡。

Fomo3D是一款運行在區塊鏈上的龐氏騙局游戲［11］。玩家通過花費ether來購買游戲中的key，這些花費的ether會被記入獎池，后面加入的玩家需要支付高出前一次購買的價格來購買key，而當沒有人繼續購買key時，游戲也隨之結束。最后一個購買key的玩家會獲得獎池中48%的獎金額，也就是獎池中的大部分ether。攻擊者通過DoS攻擊的手段，讓自己有很大概率成為最后的勝利者，造成財產損失。

案例表明，智能合約若自身存在漏洞隱患，會嚴重威脅用戶信息和財產安全，甚至造成難以預估的損失。面對智能合約存在的安全問題，研究高效的合約漏洞優化方法具有重要意義。

能夠對智能合約漏洞進行完備性和安全性分析的方法目前仍未被提出，當前對于智能合約的安全保障主要依靠專家審計和人工復查，而該類方式不能保證代碼的絕對安全［11～13］。

目前針對智能合約漏洞研究主要以智能合約部署后檢測是否存在漏洞為主［14～16］，而在智能合約部署前進行檢測及優化的較少，尤其是針對拒絕服務（DoS）漏洞優化改進的研究也是進展緩慢。

本文以拍賣退款交易模型為背景，擬解決區塊鏈中智能合約因DoS漏洞引發的資金財產安全問題和響應速度問題，對含有DoS漏洞的智能合約進行分析、優化，構建安全智能合約，并對優化后的智能合約進行安全性分析，通過形式化驗證進行正確性和效率分析。實驗結果表明，在安全性方面，優化后的智能合約能夠有效避免因資源耗盡產生的拒絕服務；在正確性和效率方面，與帶有漏洞智能合約相比，優化后的智能合約的等效內存使用量減少了約62.8%，本文方案在部署至區塊鏈前進行DoS漏洞優化，可有效避免因DoS漏洞而造成的巨大經濟損失。

1 相關理論

1.1 智能合約

在真實以太坊區塊鏈中存在無數個智能合約，每分鐘都有數以萬計的合約和交易被創建以解決實際問題。智能合約是在區塊鏈上運行的程序，合約代碼和運行狀態存儲在鏈中，它們可以產生交易并發送接收資金，一經啟動將自動運行且不可更改。

以太坊智能合約交易中定義了交易費用，用gas表示，其目的是為了防止用戶在鏈中發送太多無意義交易，因此每一筆交易均需付出一定代價，即用戶發送一筆交易時需支付一定的gas用于該筆交易執行。執行一筆交易計算步驟越復雜，這筆交易消耗的gas越多。交易執行完成后，若支付的gas沒有被消耗完，則會返還給發起該筆交易的賬戶［5］，同時產生相應合約地址。

1.2 形式化驗證

形式化驗證可以對智能合約的源碼和字節碼進行安全驗證，最大程度地保證智能合約在代碼層面的安全。形式化方法是基于數學描述和推理計算機系統性質的技術，常用于軟件規范化、開發和驗證。其中，模型檢測（也稱為屬性檢查）是一種基于狀態遷移系統的自動驗證技術，它以窮盡搜索為基礎［17］，檢查系統的給定有限狀態模型是否符合其形式規范或正確性屬性。該方法采用Promela（process meta-language）建模語言對智能合約進行建模，用SPIN進行模型檢測以驗證形式化方法對智能合約的作用［18］。

Promela是一種驗證建模語言，用于對協議（或一般的分布式系統）進行抽象，以抑制與進程無關細節［11］。Promela程序由進程、消息通道和變量組成。進程是全局對象，消息通道和變量可以在進程內全局或本地聲明。進程指定行為、通道和全局變量定義進程運行環境。

SPIN可驗證通信協議的正確性。一個進程被定義為proctypes，雖然在執行時可以動態產生新進程，但是存在一個指定某些初始指令和產生一個或多個進程臨界區。也可以在每個proctype關鍵字之前增加active關鍵字來使進程在一開始時便自動執行。SPIN模型的執行是多個語義的交叉執行，其單個表達式是原子類型，即每個表達式獨立執行。為了能使某段代碼能夠自動執行或成段執行，可以添加atomic和d_step關鍵字來使單一語句成為代碼段［19］。

1.3 智能合約通用形式化描述

智能合約的運行可以看做是狀態之間的相互轉移與轉換［20］。2019年，王璞巍等人［20］提出以多個有限狀態機組合形式來形式化描述面向合約的智能合約，以承諾作為基本單元來構建智能合約，一份合同通常由一組相互關聯的承諾組成。

定義1 承諾。它是一個五元組C（x，y，p，r，tc），五元組C含義為承諾人x向被承諾人y作出承諾，如果前提p達成，就產生結果r［20］。其中：

a）前提p和結果r是布爾值，即值為true表示前提已達成或結果已完成，值為1表示前提未達成或結果未完成；

b）tc表示該承諾的有效期，只有當tc為true，承諾才會有效。

一個承諾的生命周期可能有五種不同的狀態，分別是激活（act）、就緒（bas）、滿足（sat）、過期（exp）、違約（vio）。

a）激活。前提p和結果r都為1，時間未超出承諾的有效期，表示承諾有效，在等待前提p的達成和結果r的完成。

b）就緒。前提p為true，結果r為1，時間未超出承諾的有效期，表示承諾已生效且前提p已經達成，在等待結果r的完成。

c）滿足。前提p和結果r都為true，表示前提p已達成，結果r也已完成，承諾已被履行。

d）過期。前提p和結果r都為1，時間已超出承諾的有效期，表示在承諾失效時，前提p未能達成而結果r也未能完成。

e） 違約。前提p為true，但結果r為1，時間已超出承諾的有效期，表示當承諾失效時，盡管b已達成了前提p，但a仍然未履行其承諾完成結果r，已經違約。

定義2 承諾有效期。它是一個二元組tc：=（pdact，pdbas），其中，pdact表示承諾進入激活狀態之后，對前提p的完成時間限制；pdbas表示承諾進入就緒狀態之后，對結果r的完成時間限制。若這兩個限制滿足，tc為true；否則，tc為1［20］。

例如，tc=（12，12）表示前提p需要在承諾進入激活狀態12 h（默認單位為h）之內達成（即pdac=12），否則承諾將進入過期狀態；結果r需要在承諾進入到就緒狀態之后12 h之內完成（即pdbas=12），否則承諾進入違約狀態。

在承諾中，前提或結果可能是預期的動作。例如，商家a向客戶b作出一個承諾，如果b在系統上預存100元貨物錢，a就給b寄出相應貨物。這里，前提是預存錢的動作（b在系統上預存100元錢），結果是寄貨物的動作（a給b寄出購買的貨物）。本文中，動作（action）定義如下。

定義3 動作。一個動作表示為action：=actname（executor，object，input，output）［20］，其中：

a）actname是動作的名稱，executor是動作的執行者，object是動作的作用對象，input是輸入參數，output是輸出參數。act、exectuor是必需的（required），而objectinput和output都是可選的（optional）。

b）動作的值是一個布爾值，action=1表示沒有完成該動作，action=true表示已完成該動作，動作的默認值為1。

2 本文方案

在本文的拍賣退款交易應用場景中惡意合約利用DoS漏洞可使拍賣出現以下問題：

a）主動終止拍賣。若無用戶出價，攻擊者成為此時的最高出價者（又稱領先者），則此時拍賣終止，將執行拍賣合同中的退款操作。退款操作中將遍歷數組為各用戶退款，攻擊者可利用DoS漏洞阻止退款操作，使得交易款留在合約賬戶中，未能退到各用戶的地址賬戶，此時攻擊者可非法獲得各交易用戶的交易款。如其中某一賬戶退款失敗，則所有后續退款操作都將終止。

b）被動終止拍賣。攻擊者循環遍歷數組操作可導致gas耗盡，使交易狀態回退至原始狀態，此次燃料費gas被無端消耗。如此無限循環，誘使交易賬戶多次支付燃料費gas。

該安全問題產生原因是合約在執行下一步操作時需依賴上一步的退款結果，導致攻擊者惡意攻擊使回退函數執行失敗，一個用戶退款失敗，導致下一個用戶無法進行操作。

本文涉及智能合約運行的兩個重要變量：a）領先者currentFrontrunner，表示當前出價最高者；

b）當前金額currentBid，用來存放領先者所出金額。

2.1 優化方案

針對該智能合約實例中因受到DoS攻擊而使賬戶地址gas耗盡問題進行如下改進：

a）為被優化的合約（contract SecureAuction）添加refunds，refunds為mapping類型（建立地址到整型間的映射），每個用戶將退還的金額存儲在refunds中，由用戶自己主動去請求合約來實現金額的退回，這樣就避免revert函數被觸發。

b）對于交易bid函數。send方法的實現內容是revert函數，檢查是否存在領先者（currentFrontrunner！=0），若不存在，則退回；若存在（條件為真），則進行交易，之后發生退款：用局部變量refund存儲當前賬戶的交易額，當交易額歸零（refunds［msg.sender］=0）時，退款發生。

針對拍賣退款智能合約運行中出現的安全問題，設計本文DoS漏洞優化及驗證方案，如圖1所示。

a）拍賣退款智能合約文件。含有DoS漏洞的合約（contract DosAuction）及被優化的合約（contract SecureAuction）作為兩份合約共同存儲在auction.sol文件中。

b）合約建模。使用Promela語言形成DosAuction.pml和SecureAuction.pml兩份形式化代碼文件。

c）驗證。將待驗證模型通過SPIN自動化驗證工具實驗運行。

d）驗證結果。驗證優化后的智能合約的安全性及效率。

2.2 拍賣退款智能合約

2.2.1 拍賣退款智能合約算法

拍賣過程中，拍賣退款智能合約貫穿拍賣全程。首先由某一用戶出價，其后有意競爭用戶相繼出價（報價持續升高），直至無人出價。智能合約用于競爭用戶出價時，將前一用戶的競價退回，并將本次交易存儲在相應合約地址中。

根據1.3節中有限狀態機組合形式，有漏洞智能合約算法形式化描述如下：

C1=C（msg.sender，currentFrontrunner，true，

refund（msg.sender，currentFrontrunner），（∞，h））

承諾C1的含義為：當前調用者msg.sender向當前領先者currentFrontrunner承諾，如果currentFrontrunner在競價低于原始競價則發生refund（msg.sender，currentFrontrunner）行為，系統將會在h時間內執行。

根據設計流程思路得出帶有漏洞智能合約算法如下所示。

算法1 帶有漏洞的智能合約（contract DosAuction）算法

輸入：當前領先者currentFrontrunner；當前金額currentBid。

輸出：若保存到合約中金額大于當前最高價，則繼續執行支付函數bid（）；否則，則中止支付函數bid（），等待下一次交易開始。

支付函數bid（）：

if msg.valuegt;currentBid：

if currentFrontrunner！=0：

currentFrontrunner.sender.send（currentBid）;

else

currentFrontrunner=msg.sender;

currentBid=msg.value;

else

end;

其中：bid（）函數是帶有關鍵字“payable”帶有支付性質函數，在運行過程中，會判斷參與保存到合約中金額與領先者賬戶的金額大小關系，若不高于，DoS攻擊不會發生；否則，則會無限次發生DoS攻擊，使交易無法進行。

2.2.2 優化方案算法

根據本文1.3節中有限狀態機組合形式，優化后拍賣退款智能合約算法形式化描述如下：

C2=C（msg.sender，currentFrontrunner，true，

refund（msg.sender，currentFrontrunner），（x，h））

承諾C2的含義為：當前調用者msg.sender向當前領先者currentFrontrunner承諾，如果currentFrontrunner在競價低于原始競價則發生refund（msg.sender，currentFrontrunner）行為，系統將會在h時間內執行。

針對DoS漏洞優化后的拍賣退款智能合約算法如下。

算法2 優化后的智能合約（contract SecureAuction）算法

輸入：當前領先者currentFrontrunner；當前金額currentBid；存儲退款映射refunds；退款數組refund。

輸出：若保存到合約中金額大于當前最高價，則繼續執行支付函數bid（）及退款函數withdraw（）；否則，則中止支付函數bid（），執行退款函數withdraw（）。

映射refunds：

address→uint;

支付函數bid（）：

if msg.valuegt;currentBid：

if currentFrontrunner！=0：

currentBid++;

else break;

else end;

if msg.valuegt;currentBid：

if currentFrontrunner！=0：

mapping+currentBid;

退款函數withdraw（）：

refunds［msg.sender］=0;

msg.sender.send（refund）;

bid（）函數是帶有關鍵字“payable”帶有支付性質的函數，在運行過程中：

a）定義映射，定義由地址到短整型映射來存儲退款。

b）價格累加，競拍價格依次累加，避免中途回滾。

c）退款函數，將需要退款的地址借助變量refund來存儲，依次退款。

2.3 合約建模

2.3.1 形式化驗證定義

首先將Solidity代碼翻譯成等效Promela代碼，一部分Solidity代碼去除，其他部分直接或間接換成Promela代碼語句。建模時主要對合約控制語句進行抽象，對控制語句進行形式化定義如下所示［4］。

（B，σB，σM）→true：

（if（B）{O}，σB，σM）→（O，σB，σM）（1）

（B，σB，σM）→1：

（if（B）{O}，σB，σM）→（//，σB，σM）（2）

式（1）（2）為if語句。其中，B表示判斷條件，判斷條件分為true和1，若判斷條件為真時，執行操作O，∥表示若判斷條件為假，不執行任何操作。

（B，σB，σM）→true：

（while（B）{O}，σB，σM）→（O，while（B）{O}，σB，σM）（3）

（B，σB，σM）→1：

（while（B）{O}，σB，σM）→（//，σB，σM）±（4）

式（3）（4）為while語句。其中，B表示判斷條件，判斷條件分為true和1，若判斷條件為真時，執行操作O再進行判斷，∥表示若判斷條件為假，不執行任何操作。

在使用Promela建模時，需要將Solidity中的控制語句轉換為Promela語句。定義轉換規則如下：

Solidity：（if（B），{O}） | →

Promela：

if

：：（B） →{O}

：：else →skip

fi

Solidity：（while（B），{O}） | →

Promela：

do

：：（B） →{O}

：：else →skip

od

2.3.2 形式化驗證算法

合約建模步驟如下：

a）變量初始化。定義msg_sender，msg_value類型以及初始值；定義refunds（整型數組）用于存放退款；定義currentFrontrunner（出價最高者）以及currentBid（出具金額）。

b）定義sendCoin（付款函數）。用于貨幣傳輸；定義兩個參數，分別是amount和receiver， amount參數用于存儲賬戶金額，receiver參數用于存儲收款人（參與競價的地址）。

c）定義bid（交易函數）。包含通道變量currentstate，用于存儲當前參與競價地址以及競價金額。

d）定義withdraw（退款函數）。用于進行地址的退款，同時避免重入攻擊。

e）激活形式化驗證進程。上述提及所有函數是三個不同的進程名，使用關鍵字run來激活進程。

形式化驗證算法如下：

算法3 優化前形式化代碼文件（DosAuction.pml）

輸入：當前領先者currentFrontrunner；當前金額currentBid；參與拍賣總人數NUMBER；存儲參與人的退款balances［NUMBER］。

輸出：執行sendCoin（）函數，用于交易（貨幣流通），支付函數bid（）中，若保存到合約中金額大于當前最高價，則繼續執行；否則，則中止支付函數bid（），等待下一次交易開始。同時輸出運行結果：冗余校驗結果、內存占用效率、壓縮率、運行時間。

交易函數sendCoin（）：

int amount;//定義一個賬戶用于存儲交易額

if amount lt; high_sendCoin_account：

amount++;

assert（balances［msg_sender］ gt; amount）

支付函數bid（）：

chan currentstate=［2］ of {byte，int};

assert（msg_valuegt;currentBid）;

msg_value=current _msg_value;

currentFrontrunner=msg_sender;

算法4 優化后形式化代碼文件（SecureAuction.pml）

輸入：當前領先者currentFrontrunner；當前金額currentBid；參與拍賣總人數NUMBER；存儲參與人的退款balances［NUMBER］。

輸出：執行sendCoin（）函數，用于交易（貨幣流通），支付函數bid（）中，若保存到合約中金額大于當前最高價，則繼續執行；否則，則中止支付函數bid（），執行退款函數withdraw（）。同時輸出運行結果。

交易函數sendCoin（）：

int amount;//定義一個賬戶用于存儲交易額

if amount lt; high_sendCoin_account：

amount++;

assert（balances［msg_sender］ gt; amount）

支付函數bid（）：

chan currentstate=［2］ of {byte，int};

assert（msg_value gt; currentBid）;

msg_value=currentBid+msg_value;

currentFrontrunner=msg_sender;

退款函數withdraw（）：

chan refund=［2］ of {byte，int};

currentFrontrunner=msg_sender;

3 實驗結果及分析

本文實驗分為智能合約和形式化驗證兩個部分，分別驗證優化后系統資源是否耗盡、內存占用效率及運行效率是否提高。

3.1 實驗環境

操作系統為基于VMware Workstation 16 Pro搭載的Ubuntu 16.04.7 LTS鏡像；

處理器為Intel CoreTM i5-10300H CPU @ 2.50 GHz × 4；

內存為虛擬內存4.0 GB （3.8 GB 可用）；

編程環境為Remix在線編輯器，Ispin形式化驗證工具圖形界面；

編程語言為Solidity 0.4.15，Promela形式化驗證語言。

3.2 智能合約文件運行安全性分析

對優化后的智能合約（contract SecureAuction）在資源耗盡方面進行分析，驗證優化后的智能合約運行安全性。

a）運行帶有DoS漏洞智能合約（contract DosAuction）支付10 ether。帶有DoS漏洞的智能合約交易輸出的詳細信息如表1所示。

其中：參數Status表示本次交易狀態；參數from表示賬戶地址；參數to表示合約地址；參數gas表示花費燃料；參數Transaction cost表示交易燃料；參數hash表示交易加密；參數value表示交易10 ether。

b）運行優化后智能合約（contract SecureAuction）支付10 ether。

優化DoS漏洞的智能合約交易輸出的詳細信息如表2所示。

對比兩份合約（contract DosAuction和contract Secure-Auction）的運行日志（表1和2）：

contract DosAuction中，gas=transaction cost（燃料費與交易費是相等），即花費了全部燃料費來支撐交易，造成了資源耗盡；

contract SecureAuction中，gasgt;gt; transaction cost（燃料費與交易費不等），并未花費全部資源來支撐本次交易。

針對2.1節中闡述的問題，優化DoS漏洞的智能合約解決了以下情況：

優化DoS漏洞的智能合約用refunds（地址映射）存儲退款，借助refund依次退款，不會造成遍歷數組時中途被攻擊者終止；

根據優化DoS漏洞的智能合約運行結果可以看出，因為燃料費與交易費不等，不會造成系統資源消耗殆盡（gas耗盡），故拍賣不會因gas耗盡而終止。

c）withdraw退款函數運行結果分析。

優化DoS漏洞的智能合約執行withdraw退款函數后結果如表3所示。

表3中，參數status表示本次交易狀態；參數from表示賬戶地址；參數to表示合約地址；參數gas表示花費燃料；參數transaction cost表示交易燃料；參數hash表示交易加密；參數value表示交易0 ether。

本次拍賣完成后不存在資源耗盡問題，同時在運行withdraw退款函數后系統資源由表2的65651 gas變為表3的23804 gas，參數value由表2的10 ether變為表3的0 ether，表明退款成功。

3.3 形式化驗證步驟及結果分析

利用自動化工具SPIN運行兩份形式化文件產生運行日志，完成語法校驗、冗余校驗、內存使用數據及運行時間數據。

1）形式化驗證步驟

利用Remix在線編輯器編寫智能合約并編譯運行，采用SPIN進行形式化驗證，包含語法校驗、冗余校驗、狀態列表、隨機種子數與循環步數調整、輸出參數結果等步驟。

a）編寫智能合約。編寫auction.sol文件，文件中包含Dos-Auction和SecureAuction兩份合約，其中DosAuction合約是包含DoS漏洞的智能合約，SecureAuction合約是針對DoS攻擊經過一定程度改進后的智能合約。

b）形成形式化驗證文件。將該auction.sol文件按照Promela語法規則轉換成DosAuction.pml和SecureAuction.pml兩份形式化驗證文件。

c）分別導入源文件。導入“ispin DoSAuction.pml”和“ispin SecureAuction.pml”文件。

d）校驗。對DosAuction.pml和SecureAuction.pml進行語法校驗和冗余校驗，生成如圖2～5所示運行結果。

e）模擬運行。設置隨機種子random seeds=150、循環步數loop steps=10 000，運行DosAuction.pml和SecureAuction.pml文件。

f）形式化驗證。將DosAuction.pml和SecureAuction.pml文件進行形式化驗證，獲得運行日志。

2）結果分析

a）上述步驟d）得到的校驗結果，如圖2～5所示。

結果分析：通過語法校驗和冗余校驗結果（如圖2～5紅框所示）可知，DosAuction.pml和SecureAuction.pml兩份形式化文件不存在語法錯誤和冗余。

b）上述步驟f）針對DosAuction.pml和SecureAuction.pml產生的驗證記錄分別如圖6和7所示。形式化驗證記錄對比如表4所示。

結果分析：通過運行日志找到兩份文件的內存使用數據和運行時間數據，對比觀察效率得到提高。優化方案中為contract SecureAuction合約添加映射類型變量，用于存儲每個用戶退款的金額，可由用戶主動請求退款，避免退款函數使用send方法調用revert函數被動完成；對于交易bid函數，檢查是否存在領先者，若不存在，則退回；若存在，則進行交易，及時產生退款。由于主動退款發生后，系統資源被釋放，使運行時間縮短，內存占用減少，同時也可避免惡意用戶利用DoS漏洞非法占用資金。

運行日志表明，優化后智能合約與帶有漏洞智能合約的總存儲空間占用基本相同，但在等效內存使用量方面，優化后的智能合約減少了約62.8%，說明優化后的智能合約空間利用率更高，運行時間也減少了44.9%。

4 結束語

區塊鏈上的智能合約一直面臨著漏洞問題，其中許多漏洞已經造成了重大經濟損失。本文以拍賣合約為背景，以拍賣退款為例提出一種針對DoS攻擊智能合約的優化方法，采用SPIN形式化驗證算法分別對優化前后合約進行驗證，得到輸出日志。通過這種將智能合約和形式化驗證相結合的方式來對DoS漏洞加以改進優化，不斷地增強智能合約在現實中的應用效果。然而該模型還存在一些不足之處，雖然針對拍賣退款智能合約模型中因依賴外部數據而產生的DoS漏洞問題做了優化改進，對于由其他因素而產生的DoS漏洞問題如何優化問題及設計DoS漏洞通用的優化方案是下一步研究方向。

新的智能合約漏洞還會出現，需要區塊鏈領域、密碼學領域、網絡安全領域以及形式化驗證領域的不斷合作與創新。

參考文獻：

［1］單康康，袁書宏，張紫徽，等. 區塊鏈技術及應用研究綜述 ［J］. 電信快報，2020 （11）： 17-20. （Shan Kangkang，Yuan Shuhong，Zhang Ziwei，et al. Overview of blockchain technology and application research ［J］ Telecom Express，2020 （11）： 17-20.）

［2］劉志勇，朱峰，吳東升，等. 區塊鏈智能合約安全漏洞問題研究 ［C］//第九屆中國指揮控制大會論文集. 2021： 6. （Liu Zhiyong，Zhu Feng，Wu Dongsheng，et al. Research on security vulnerabilities of blockchain smart contract ［C］ // Proc of the 9th China Command and Control Conference. 2021： 6.）

［3］肖美華，周浩洋，朱志亮，等. 基于模型檢測的區塊鏈智能合約公平性形式化驗證 ［J］. 華東交通大學學報，2021，38（3）： 52-60. （Xiao Meihua，Zhou Haoyang，Zhu Zhiliang，et al. Formal verification of fairness of blockchain smart contract based on model detection ［J］. Journal of East China Jiaotong University，2021，38（3）： 52-60.）

［4］朱颮凱，李穎，張志強，等. 基于動態模糊測試和機器學習的智能合約漏洞檢測方法 ［J］. 警察技術，2021（6）： 56-60. （Zhu Baokai，Li Ying，Zhang Zhiqiang，et al. Intelligent contract vulnerability detection method based on dynamic fuzzy testing and machine learning ［J］. Police Technology，2021（6）： 56-60.）

［5］Luu L，Chu D H，Olickel H，et al. Making smart contracts smarter ［C］// Proc of ACM SIGSAC Conference on Computer and Com-munications Security. New York ：ACM Press，2016： 254-269.

［6］付夢琳，吳禮發，洪征，等. 智能合約安全漏洞挖掘技術研究 ［J］. 計算機應用，2019，39（7）： 1959-1966. （Fu Menglin，Wu Lifa，Hong Zheng，et al. Research on security vulnerability mining technology of smart contract ［J］. Journal of Computer Applications，2019，39（7）： 1959-1966.）

［7］趙波，上官晨晗，彭小燕，等. 基于語義感知圖神經網絡的智能合約字節碼漏洞檢測方法 ［J］. 工程科學與技術，2022，54（2）： 49-55. （Zhao Bo，Shangguan Chenhan，Peng Xiaoyan，et al. Smart contract bytecode vulnerability detection method based on semantic perception graph neural network ［J］. Engineering Science and Technology，2022，54（2）： 49-55.

［8］Wood G. Ethereum： a secure decentralised generalised transaction ledger ［J］. Ethereum Project Yellow Paper，2014，151： 1-32.

［9］Osterland T，Rose T. Model checking smart contracts for Ethereum ［J］. Pervasive and Mobile Computing，2020，63： 101129.

［10］趙偉，張問銀，王九如，等. 基于符號執行的智能合約漏洞檢測方案 ［J］. 計算機應用，2020，40（4）： 947-953. （Zhao Wei，Zhang Wenyin，Wang Jiuru，et al. Smart contract vulnerability detection scheme based on symbolic execution ［J］. Journal of Computer App-lications，2020，40（4）： 947-953.）

［11］李宗鴻，胡大裟，蔣玉明. 面向智能合約漏洞檢測的改進符號執行研究 ［J］. 計算機應用研究，2021，38（7）： 1943-1946. （Li Zonghong，Hu Dasha，Jiang Yuming. Research on improved symbolic execution for smart contract vulnerability detection ［J］.Application Research of Computers，2021，38（7）： 1943-1946.）

［12］Buterin V. A next-generation smart contract and decentralized application platform ［EB/OL］. （2016）. https：//github.com/ethereum/wiki/wiki/White-Paper.

［13］Bogner A，Chanson M，Meeuw A. A decentralised sharing App running a smart contract on the Ethereum block chain ［C］// Proc of the 6th International Conference on the Internet of Things. New York： ACM Press，2016： 177-178.

［14］印桂生，高樂，莊園，等. 基于字節碼關鍵路徑的智能合約漏洞檢測 ［J］. 哈爾濱工程大學學報，2022，43（2）：255-261. （Yin Guisheng，Gao Le，Zhuang Yuan，et al. Smart contract vulnerability detection based on bytecode critical path ［J］. Journal of Harbin Engineering University，2022，43（2）：255-261.）

［15］祝超群，張永川. 拒絕服務攻擊下網絡化控制系統的安全研究 ［J］. 控制工程，2021，28（10）： 2070-2077. （Zhu Chaoqun，Zhang Yongchuan. Research on security of networked control system under denial of service attack ［J］. Control Engineering，2021，28（10）： 2070-2077.）

［16］Omohundro S. Cryptocurrencies，smart contracts，and artificial intel-ligence ［J］. AI Matters，2014，1（2）： 19-21.

［17］Nehai Z，Piriou P Y，Daumas F. Model-checking of smart contracts ［C］// Proc of IEEE International Conference on Internet of Things and IEEE Green Computing and Communications and IEEE Cyber，Physical and Social Computing and EEE Smart Data. Piscataway，NJ： IEEE Press，2018： 980-987.

［18］張瀠藜，馬佳利，劉子昂，等. 以太坊Solidity智能合約漏洞檢測方法綜述 ［J］. 計算機科學，2022，49（3）： 52-61. （Zhang Yingli，Ma Jiali，Liu Ziang，et al. Overview of Ethereum solidity smart contract vulnerability detection methods ［J］. Computer Science，2022，49（3）： 52-61.）

［19］朱健，胡凱，張伯鈞. 智能合約的形式化驗證方法研究綜述 ［J］. 電子學報，2021，49（4）： 792-804. （Zhu Jian，Hu Kai，Zhang Bojun. Review on formal verification methods of smart contract ［J］. Acta Electronica Sinica，2021，49（4）： 792-804.）

［20］王璞巍，楊航天，孟佶，等. 面向合同的智能合約的形式化定義及參考實現 ［J］. 軟件學報，2019，30（9）： 2608-2619. （Wang Puwei，Yang Hangtian，Meng Jie，et al. Formal definition for classical smart contracts and reference implementation ［J］.Journal of Software，2019，30（9）： 2608-2619.）

收稿日期：2022-07-27；修回日期：2022-09-20 基金項目：國家自然科學基金資助項目（62173171）

作者簡介：陳虹（1967-），女，遼寧阜新人，副教授，碩導，碩士，主要研究方向為信息安全、網絡安全；王穎輝（1998-），男（通信作者），遼寧沈陽人，碩士研究生，主要研究方向為網絡安全、區塊鏈（15998203039@163.com）；金海波（1983-），男，遼寧沈陽人，副教授，碩導，博士，主要研究方向為復雜系統可靠性分析、異常檢測、優化維修策略制定；曹玥（1997-），女，江蘇常州人，碩士研究生，主要研究方向為網絡安全、密碼學.