一種基于時間自動機的安全智能合約生成方法

劉 陽，張圣杰

（上海海事大學 物流科學與工程研究院，上海 201306）

0 概述

近年來，區塊鏈技術得到快速發展，其作為一種分布式計算技術，具有去中心化、匿名性、透明性等潛在特性。從最開始的比特幣到后來的以太坊，智能合約已經成為區塊鏈和應用領域之間的溝通橋梁。區塊鏈通過智能合約處理現實世界中的各種業務，在許多領域都具有良好的應用前景。智能合約本身并不是一個新概念，它最初是由計算機科學家SZABO 提出［1］，并被定義為“一套數字指定的承諾”。在區塊鏈中，智能合約是一個由相關各方均認可的程序代碼，這些程序代碼能夠以公開、透明、自動和確定性的方式規范某些業務流程或多方之間的交互［2］。與其他軟件相同，智能合約也容易出現錯誤，因為智能合約通常控制著大量的金融資產，所以它對安全性提出了更高的要求。由于區塊鏈本身所具備的特點，智能合約部署后的修改成本非常大，如DAO 事件［3-4］引起的以太坊硬分叉，因此一個安全的智能合約尤其重要，這也是基于區塊鏈的應用程序的執行關鍵。智能合約安全［5］已經成為區塊鏈應用執行過程中亟需解決的問題。

目前，大量的研究工作通過驗證技術來確保智能合約的安全，這些研究工作涵蓋了智能合約在設計、開發、運行等階段的安全問題［6］。文獻［7］開發一個智能合約驗證工具ContractLarva，用于監測應用運行時的違規情況。文獻［8］使用K 框架對智能合約進行驗證，檢測合約函數是否符合ERC20 代幣標準。文獻［9］介紹一個名為Manticore 的開源動態符號執行框架，該框架可用于分析二進制文件和以太坊智能合約。文獻［10-12］也都通過符號執行技術來分析智能合約代碼的漏洞。在模型檢測方面，文獻［13］不僅建立智能合約的時間自動機（Timed Automata，TA）模型，還構建簡單的區塊鏈機制并模擬用戶行為。文獻［14］將Solidity 智能合約建模為彩色Petri 網（Color Petri Net，CPN），并使用CPN 工具驗證智能合約的相關屬性。以上方法大多針對由智能合約工作機制以及合約代碼的缺陷或錯誤所導致的安全問題，然而在實踐過程中，根據一個邏輯不嚴謹、不完善甚至錯誤的業務流程所設計的智能合約，不但會導致整個業務無法正常進行，還可能使現實世界遭受巨大的經濟損失。

文獻［15］提出一種將業務流程建模符號（Business Process Modeling Notation，BPMN）流程模型編譯成Solidity 智能合約的方法，文獻［16］提出一種類似的方法，使用BPMN 對組織間的業務流程進行建模，經過一系列的轉換和優化后為Hyperledger Fabric 生成Go 語言鏈碼。文獻［17］將離散事件建模與有限狀態機（Finite State Machine，FSM）建模相結合，以表示交易領域的應用邏輯，并將模型自動轉換為智能合約。文獻［18］使用文件模板和受控自然語言（Controlled Natural Language，CNL）創建人類可理解的合約文件，并將其自動映射為正式模型，然后將該正式模型翻譯為可執行的Hyperledger Fabric 智能合約。文獻［19］設計一種SPESC 到目標程序語言（Solidity）的轉換規則。文獻［20］為自動生成智能合約提供了一個新的框架，該框架使用本體和語義規則來編碼特定領域的知識，然后利用抽象語法樹的結構來納入所需的約束。文獻［21］提出一個用于建模和開發智能合約的聊天機器人，其可以進行模型到文本的轉換以生成智能合約代碼。

上述研究重點關注智能合約代碼的自動生成而忽略了其安全性。文獻［22］提出一種VeriSolid 框架，它可以對使用過渡系統模型和嚴格操作語義時指定的智能合約進行驗證，并從驗證過的模型中生成Solidity 代碼。文獻［23］將智能合約創建為FSM，并且實現一個用于設計合約FSM 的用戶界面以及一個自動代碼生成器，其所包含的鎖定和轉換計數可以防止可重入、不可預測狀態等常見的安全問題。文獻［24］使用Petri Nets 對智能合約工作流進行建模，并通過引入驗證引擎對模型進行驗證，驗證為安全的模型會自動轉換為可執行的智能合約代碼。

本文提出一種基于時間自動機的安全智能合約生成方法，目的是在智能合約生成之前避免錯誤，即設計正確的合約模型，并從模型中生成可執行的智能合約代碼。相較現有的方法框架，時間自動機具有豐富的時間語義，更能滿足區塊鏈應用在多樣化、復雜化的背景下對智能合約建模的需求。同時，基于建模、模擬和驗證進行一體化設計，從而提高生成方法的執行效率。

1 背景知識

時間自動機［25］本質上是用實值變量擴展的有限狀態機，該實值變量也叫時鐘。設Т是非負實數或自然實數的時域，時鐘x是一個來自時域的變量，可以用來測量時間的流逝。對于一個時鐘x，時鐘解釋v表示對時鐘的賦值，定義為x→ ?≥0，v（x）=0 意味著將時鐘x重置為0。Φ（x）是時鐘x上的一組時鐘約束，它是一個不等式的結合物，其中，單個時鐘的值與一個整數進行比較。一個時鐘約束Φ的定義為：

其中：True 表示邏輯正確；x是一個時鐘；c是有理數集中的一個常量。

時間自動機是一個六元組A=（Σ，L，l0，X，I，E），其中：Σ是一個有限的符號集，稱為字母表；L是有限位置的集合；l0∈L是初始位置；X是有限時鐘的集合；I是一個不變量映射，它為L中的每一個位置l指定一個時鐘約束；E?L×Σ×Φ（X）×2X×L是位置轉換關系的集合。令g∈Φ（X）是時鐘X上的一個具體的時鐘約束，r為轉換過程中被重置的時鐘，那么一條具體的轉換可以形式化表示為e=（1，σ，r，g，l′）∈E，即當輸入為σ時，如果滿足時鐘約束g，那么自動機的位置將從l 轉換到l′，并且對于任意的時鐘x∈r，有v（x）=0。

2 方法論

在以太坊中，智能合約被看作是一個狀態機，智能合約執行一次則狀態發生改變，這為將智能合約建模為狀態轉換系統提供了先決條件。智能合約可以被外部賬戶和合約賬戶調用，當滿足預先設定的條件時自動執行。智能合約本質上是由眾多函數和狀態變量組成的，本節詳細闡述如何為一個指定的文本合同建立時間自動機模型以及如何從模型中自動生成可執行代碼。

圖1 所示為安全智能合約生成的工作流框架，共分為3 個部分：

圖1 安全智能合約生成的工作流框架Fig.1 Workflow framework for secure smart contract generation

1）從文本合同到時間自動機的準確性建模。對于一個給定的文本合同（如法律文書、業務活動方案等），通過UPPAAL 建模工具將其建模為時間自動機。為了避免建模過程中由人為因素導致的錯誤，文本合約中所描述的工作流被抽象為計算樹邏輯（Computation Tree Logic，CTL）公式并通過驗證器進行驗證，驗證通過則說明所建立的模型和文本合約的工作流保持一致，否則根據驗證不通過的反例修正模型直到通過為止。

2）基于時間自動機的智能合約安全性驗證。被驗證為正確的時間自動機模型可通過模擬器進行模擬，以便于更直觀地了解合約的工作流。在此基礎上，驗證器通過相關性質驗證該時間自動機模型的可達性、安全性以及活性，以保證文本合約所描述的工作流本身是安全可靠的。其中，相關性質可以來自于行業的既定標準，也可以是從工作流中高度概括而來的性質規約，它們都被抽象為CTL 公式以支持驗證器輸出結果，若結果為yes，則代表相關性質被滿足。

3）在模型被判定為安全的基礎上基于時間自動機的Solidity 代碼生成。首先根據映射規則從時間自動機模型中獲取對應的Solidity 智能合約信息，然后通過提前定義好的智能合約模板自動生成可執行的Solidity 代碼。

2.1 基于UPPAAL 的時間自動機建模與驗證

UPPAAL 是一個用于驗證實時系統的工具箱，旨在驗證可以建模為時間自動機網絡的系統，該網絡擴展了整數變量、結構化數據類型和信道同步。UPPAAL 已成功應用于智能合約系統的建模過程［26-27］，其能提供友好的圖形化界面，可以通過編輯器、模擬器和驗證器引擎實現系統建模和驗證可視化。

UPPAAL 的建模語言為時間自動機網絡，表示多個時間自動機的并發。從文本合約到時間自動機的建模過程具有嚴格的流程，基于UPPAAL 的時間自動機建模流程如圖2 所示。對于一個給定的文本合約，根據其所描述的工作流提取出對應的事件，隨后為每一個事件聲明其所需要涉及的變量，包括事件的名稱等。同時，根據合約所描述的工作流分析狀態間的轉移關系進而確定事件觸發的條件以及產生的結果。接著，在模型編輯器中繪制狀態轉移圖從而得到文本合約的時間自動機模型。在繪制過程中，使用事件的名稱進行并發模型之間的交互，事件的具體操作表示為自動機邊上的更新（update），事件觸發的條件表示為邊上的守衛（guard）。最后，UPPAAL 驗證器用于驗證合約工作流的相關性質，確保所建立的時間自動機模型正確，驗證結果若為no，則重新執行整個建模流程，直到驗證結果為yes，流程結束。

圖2 基于UPPAAL 的時間自動機建模流程Fig.2 UPPAAL-based timed automata modeling process

圖3 中描述了一個跑馬燈系統，該跑馬燈擁有關閉（off）、常亮（bright）和閃爍（blink）3 個狀態，其中，off 為初始狀態，通過按壓指令Press 可以實現3 個狀態的任意轉換。該系統被建模為一個由跑馬燈自動機（lamp）和開關自動機（switch）組成的時間自動機網絡，2 個自動機之間通過Press 指令進行通信，唯一的時鐘x測量每個事件之間的時間。當按下開關時，lamp接收Press指令，狀態從off 轉移到bright。若Press 在一個時間單位內發生2 次，lamp 則轉移到blink 狀態。若lamp 在bright 狀態持續3 個時間單位之后再次接收到Press 指令，則回到off 狀態。當lamp 已經到達blink 狀態，無論Press 何時發生，它都將再次轉換到off 狀態。

圖3 時間自動機網絡Fig.3 Timed automata network

UPPAAL 查詢語言是一個簡化版的計算樹邏輯，它由路徑公式和狀態公式組成，用于指定相關屬性。狀態公式描述單個狀態，而路徑公式量化了模型的過量或痕跡。狀態公式φ是一種表達式，可以在不考慮模型行為的情況下對狀態進行評估。路徑公式可分為可達性、安全性和有效性。可達性意味著是否存在一條從初始狀態開始的路徑，沿著該路徑最終滿足φ，本文用路徑公式E＜＞φ表示滿足φ的某個狀態是可到達的。安全性要求壞的事情永遠不會發生。對于一個給定的狀態公式φ，本文用A［］φ表示在所有可達狀態下φ都應該為真，而E［］φ則表示應該存在一條最大路徑使得φ為真。活性意味著好的事情總會發生，其中，A＜＞φ表示狀態公式φ最終會滿足，φ→ψ表示只要φ滿足，那么ψ最終也會滿足。

2.2 基于時間自動機的智能合約代碼生成

以太坊Solidity 智能合約是一個狀態機，函數的每一次執行都會引起狀態的變化，其中，函數在執行過程中處理智能合約的狀態變量，從而引起狀態的遷移。將智能合約表述為一個狀態轉換系統，如定義1 所示。

定義1一個智能合約可以表示為一個四元組SSC=（S，s0，vvar，TTrans），其中：S表示合約的有限狀態集合；s0是合約的初始狀態；vvar是合約變量的集合，包括合約數據變量（C）、函數輸入變量（I）和輸出變量（O）；TTrans?S×AAct×G×S是函數 的集合，AAct=Operation（C，I，O）表示動作，其本質是對變量的操作，G是布爾值，它是函數的執行條件，條件滿足則執行，不滿足則終止執行，其本質是合約數據與函數輸入數據的比較，定義為G：：=True|C>I|C≥I|C

由時間自動機的定義可知，時間自動機的語義可以表示為一個帶有時間約束的狀態轉換系統（Q，q0，Σ，λ），其中，Q=（L，v），q0=（l，0），λ?Q×（Σ∪T）×Q是系統轉換關系。該系統的離散轉換可以表示為：當a∈Σ時，有（l，v）通過a遷移到（l′，v′），這意味著在時間自動機中存在一個轉換（l，a，g，r，l′）∈E，使時鐘賦值v滿足時鐘約束g。

從模型到可執行代碼的過程中，代表智能合約工作流的時間自動機通過狀態轉換系統和Solidity智能合約在語義上建立等價關系。UPPAAL 時間自動機的每一個轉換被翻譯成具體的Solidity 函數，轉換中的守衛表示函數執行的條件，更新則表示函數的具體操作。一個由UPPAAL 編輯的代表智能合約工作流的時間自動機模型到Solidity 智能合約的具體映射規則如下：

1）時間自動機的位置與智能合約的狀態S是一一對應的關系，且時間自動機的初始位置l0對應合約的初始狀態s0。

2）時間自動機的變量（不包括通道等特有變量）等價于智能合約的變量vvar。

3）時間自動機中的轉換等價于智能合約中的TTrans，即函數。

4）時間自動機轉換上的通道（channel）變量等價于智能合約中對應函數的名稱，即。

5）時間自動機轉換上的守衛條件對應智能合約中的函數執行條件，即。

6）時間自動機轉換上的輸入和輸出分別等價于智能合約中對應函數的參數和返回值。

7）時間自動機轉換上的更新等價于智能合約中對應函數對變量的操作，即。

根據以上映射規則，代表智能合約工作流的時間自動機模型通過智能合約模板很容易被翻譯為可執行Solidity 代碼。智能合約模板包含4 個主要的語句，分別為合約定義ContractDefinition、狀態定義StateDefinition、變量定義VariablesDefinition 以及函數定義FunctionDefinition，對于每一個語句的表示分別如下（加粗字體表示模板語句中固有的輸出，斜體表示等待填入或修改的語句）：

ContractDefinition：：=contractname｛

StateDefinition

VariablesDefinition

FunctionDefinition

...

｝，

該語句的作用是根據contract 關鍵字定義一個具體的合約結構，其中，name是需要填入的合約名稱，即時間自動機的名稱。一個完整的智能合約結構包含智能合約的狀態、變量以及函數。

StateDefinition ：：=｛enum States｛

S0，S1，S2，…

｝

States private state=States.S0；｝，

該語句表示通過enum關鍵字枚舉智能合約的狀態，并定義一個States枚舉類型的State變量指向S0。根據映射規則可知，智能合約的狀態等價于時間自動機的狀態，因此，S0、S1、S2是代碼生成過程中需要填入的時間自動機狀態。

VariablesDefinition：：=｛type（C）Visibility C；uint startTime=block.timestamp；

｝，

該部分語句表示聲明合約變量C用來存儲相應的合約數據，其中，type可以是值類型也可以是引用類型。對于一些復雜的類型（如mapping），需要在轉換之前人為指定。Visibility=｛public，internal，private｝表示該變量的可見性，在翻譯過程中全部默認為public，在翻譯結束后可根據要求手動進行更改。startTime 為模板固定輸出，用于記錄合約的時間戳。

FunctionDefinition：：=function（uint x，type（i1）i1，…，type（in）in）Visibility Return（TTrans）｛

Require（state==States.）；

x=block.timestamp-startTime；

｝，

該部分表示根據function 關鍵字定義一個具體的智能 合約函 數，其中：i1，i2，…，；Visibility=｛public，internal，private，external｝表示該函數的可見性，在翻譯過程中全部默認為public，在翻譯結束后可根據要求手動進行更改。分別表示時間自動機中對應轉換的上一個和下一個狀態。Return（TTrans）：：=returns（type（o1）o1，…，type（on）on），其中，o1，o2，…，。如果，那么代表該函數沒有返回值。在模板中，為每一個函數固定設置一個輸入參數x，用于記錄合約流程開始到函數執行的時間差。

3 案例實現

本文考慮一個“雙十一”購物狂歡節期間的商品預售合約，有如下要求：1）買家在商品的預售時間內支付押金，并可以在其間索還押金；2）買家在預售期結束后、“雙十一”活動結束前向商家支付尾款；3）若買家沒有在規定時間內支付尾款，其支付的押金應作為對商家的賠償。本節將利用所提方法對該合約進行建模、模擬、驗證以及自動生成Solidity 代碼。

3.1 工作流建模

由預售合約要求可知，該合約應具有支付押金（Submit）、索還押金（Withdraw）、支付尾款（Transfer）以及扣除押金（Deduct）4 個事件。如圖4 所示，在UPPAAL 中，上述4 個事件在全局范圍內被聲明為通道，其他聲明是該合約中所涉及的相關參數，如showTime 表示規定的預售時間，endTime 是活動截止時間，price 是商品的售賣價格，lowDeposit 是需要支付的最低押金。buyerAccount 和sellerAccount 用來模擬買賣雙方的賬戶，N的初始值為0，用于記錄交易的次數，x是唯一時鐘變量，用于記錄事件發生的時間。

圖4 模型參數的全局聲明Fig.4 Global declaration of model parameters

圖5 是該預售合約的時間自動機網絡，并行的2 個自動機通過上文定義的通道進行同步。圖5（a）是用戶自動機（users），用于表示用戶的行為，其本質是外部賬戶對合約的調用；圖5（b）則是預售合約自動機（PreSale），表示合約對外部調用的響應以及合約自身的調用。users 自動機的初始狀態是start，它通過Submit 向PreSale 自動機發送存入押金的同步消息，而PreSale 只在規定的時間內接收該消息，當x>showTime，users 在start 狀態自循環。PreSale擁有3 個狀態，分別為deposit、wait 和end。當PreSale 處于deposit狀態時，它允許接收來自users 的Submit信號，從而實現支付押金的操作，同時PreSale遷移到wait狀態。當PreSale處于wait狀態時，則可以根據不同的信號以及條件回到deposit狀態或遷移到end狀態。

圖5 預售合約的時間自動機模型Fig.5 Timed automata model for pre-sale contract

3.2 工作流模擬

令endTime 為7，showTime 為3，lowDeposit 為60，price 為200，buyerAccount 為500，sellerAccount 為500，depositBalance 為0，通過隨機模擬觀察隨著時間自動機狀態的遷移而引起的以上參數量變化，有助于了解模型的工作流，同時也有利于合約功能的完整性設計。表1 記錄了 buyerAccount、sellerAccount 和depositBalance 的變化情況。從表1可以看出：當時間自動機網絡處于（deposit，start）時，3 個參數保持不變；當狀態通過由users 發送到PreSale 的Submit 信號遷移到（wait，select）時，buyerAccount 為440，sellerAccount 為500，depositBalance為60；當狀態通過由PreSale 發送到users 的Transfer信號遷移到（end，start）時，buyerAccount 為440，sellerAccount 為560，depositBalance 為0。以上結果 表示，買家參與了預售活動并支付了押金，但是沒有在規定時間內補交尾款，因此，買家支付的押金作為賠償轉移到了賣家賬戶。

表1 相關變量在狀態遷移時的變化情況 Table 1 The change of related variables during state transition

3.3 驗證結果

根據預售合約的文本描述，部分性質如下：

1）最終會達到“end”狀態：A<>PreSale.end。

2）“end”是可達狀態：E<>PreSale.end。

3）預售時間結束后才能支付尾款：A［］PreSale.end implyx>3。

4）不能發起重復交易，不能既支付尾款又扣除押金：A［］not（N==2）。

5）只有在預售期內才能支付押金或索還押金：A［］ PreSale.deposit implyx≤3。

6）不會死鎖：A ［］ not deadlock。

圖6 展示了以上性質的驗證結果以及時間和內存消耗。從圖6 可以看出，A<>PreSale.end 驗證不通過，這是因為合約規定了買家可以選擇在預售期內的任何時間索還押金從而退出預售活動。

圖6 驗證結果Fig.6 Verification results

3.4 Solidity 代碼生成

本文提供了模塊化代碼的生成方法，根據前文定義的轉換規則依次將時間自動機的各個部分轉換為對應的Solidity 代碼。首先，從時間自動機中提取與智能合約形成映射關系的相關信息，如自動機名稱、轉換條件等，更新變量，轉換輸入、輸出等。接下來，本文展示從PreSale 時間自動機生成的完整代碼，其已在https：//remix.ethereum.org/上進行了編譯并部署。PreSale 代碼如下：

contract PreSale ｛

//枚舉狀態

enum States ｛

deposit，wait，end

｝

States private state=States.deposit；

//變量定義

uint public endTime=7；

uint public price=200；

uint public showTime=3；

uint public lowDeposit=60；

mapping（address=>uint）public depositBalance；

mapping（address=>uint）public buyerAccount；

mapping（address=>uint）public sellerAccount；

uint startTime=block.timestamp；

//Submit 轉換

function Submit（uint x）public ｛

require（state==States.deposit）；

require（buyerAccount［msg.sender］>=price）；

x=block.timestamp-startTime；

require（x <=showTime）；

buyerAccount［msg.sender］-=lowDeposit；

depositBalance［msg.sender］+=lowDeposit；

state=States.wait；

｝

//Withdraw 轉換

function Withdraw（uint x）public ｛

require（state==States.wait）；

x=startTime-block.timestamp；

require（x <=showTime）；

buyerAccount［msg.sender］+=lowDeposit；

depositBalance［msg.sender］=0；

state=States.deposit；

｝

//Transfer 轉換

function Transfer（uint x，address add）public ｛

require（state==States.wait）；

x=startTime-block.timestamp；

require（x >=showTime&&x<=endTime）；

buyerAccount［msg.sender］-=price-lowDeposit；

sellerAccount［add］+=price；

depositBalance［msg.sender］-=lowDeposit；

state=States.end；

｝

//Deduct 轉換

function Deduct（uint x，address add）public ｛

require（state==States.wait）；

x=startTime-block.timestamp；

require（x >=endTime）；

sellerAccount［add］+=lowDeposit；

depositBalance［msg.sender］-=lowDeposit；

state=States.end；

｝

｝

4 結束語

本文提出一種基于時間自動機的安全智能合約生成方法。通過對人類可理解的文本合約進行形式化建模、模擬和驗證，有效解決智能合約在設計、開發階段的安全性問題。根據嚴格的映射規則將時間自動機轉換為可執行的智能合約代碼，提高合約編寫的效率并避免人為因素所造成的錯誤。基于該方法設計并生成商品預售合約的Solidity 代碼，該代碼通過以太坊測試網絡被證明具有有效性。下一步將規范并擴展從模型到代碼的映射規則，同時從語義層面給出嚴格的證明，從模型中獲取更全面的智能合約信息，減少代碼自動生成過程中的人為干預。此外，利用模型學習技術從輸入、輸出中自動推斷智能合約的運行時模型也是今后的研究方向。