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

劉 陽，張圣杰

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

0 概述

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

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

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

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

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

1 背景知識

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

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

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

2 方法論

在以太坊中，智能合約被看作是一個狀態(tài)機(jī)，智能合約執(zhí)行一次則狀態(tài)發(fā)生改變，這為將智能合約建模為狀態(tài)轉(zhuǎn)換系統(tǒng)提供了先決條件。智能合約可以被外部賬戶和合約賬戶調(diào)用，當(dāng)滿足預(yù)先設(shè)定的條件時自動執(zhí)行。智能合約本質(zhì)上是由眾多函數(shù)和狀態(tài)變量組成的，本節(jié)詳細(xì)闡述如何為一個指定的文本合同建立時間自動機(jī)模型以及如何從模型中自動生成可執(zhí)行代碼。

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

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

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

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

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

2.1 基于UPPAAL 的時間自動機(jī)建模與驗證

UPPAAL 是一個用于驗證實(shí)時系統(tǒng)的工具箱，旨在驗證可以建模為時間自動機(jī)網(wǎng)絡(luò)的系統(tǒng)，該網(wǎng)絡(luò)擴(kuò)展了整數(shù)變量、結(jié)構(gòu)化數(shù)據(jù)類型和信道同步。UPPAAL 已成功應(yīng)用于智能合約系統(tǒng)的建模過程［26-27］，其能提供友好的圖形化界面，可以通過編輯器、模擬器和驗證器引擎實(shí)現(xiàn)系統(tǒng)建模和驗證可視化。

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

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

圖3 中描述了一個跑馬燈系統(tǒng)，該跑馬燈擁有關(guān)閉（off）、常亮（bright）和閃爍（blink）3 個狀態(tài)，其中，off 為初始狀態(tài)，通過按壓指令Press 可以實(shí)現(xiàn)3 個狀態(tài)的任意轉(zhuǎn)換。該系統(tǒng)被建模為一個由跑馬燈自動機(jī)（lamp）和開關(guān)自動機(jī)（switch）組成的時間自動機(jī)網(wǎng)絡(luò)，2 個自動機(jī)之間通過Press 指令進(jìn)行通信，唯一的時鐘x測量每個事件之間的時間。當(dāng)按下開關(guān)時，lamp接收Press指令，狀態(tài)從off 轉(zhuǎn)移到bright。若Press 在一個時間單位內(nèi)發(fā)生2 次，lamp 則轉(zhuǎn)移到blink 狀態(tài)。若lamp 在bright 狀態(tài)持續(xù)3 個時間單位之后再次接收到Press 指令，則回到off 狀態(tài)。當(dāng)lamp 已經(jīng)到達(dá)blink 狀態(tài)，無論P(yáng)ress 何時發(fā)生，它都將再次轉(zhuǎn)換到off 狀態(tài)。

圖3 時間自動機(jī)網(wǎng)絡(luò)Fig.3 Timed automata network

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

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

以太坊Solidity 智能合約是一個狀態(tài)機(jī)，函數(shù)的每一次執(zhí)行都會引起狀態(tài)的變化，其中，函數(shù)在執(zhí)行過程中處理智能合約的狀態(tài)變量，從而引起狀態(tài)的遷移。將智能合約表述為一個狀態(tài)轉(zhuǎn)換系統(tǒng)，如定義1 所示。

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

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

從模型到可執(zhí)行代碼的過程中，代表智能合約工作流的時間自動機(jī)通過狀態(tài)轉(zhuǎn)換系統(tǒng)和Solidity智能合約在語義上建立等價關(guān)系。UPPAAL 時間自動機(jī)的每一個轉(zhuǎn)換被翻譯成具體的Solidity 函數(shù)，轉(zhuǎn)換中的守衛(wèi)表示函數(shù)執(zhí)行的條件，更新則表示函數(shù)的具體操作。一個由UPPAAL 編輯的代表智能合約工作流的時間自動機(jī)模型到Solidity 智能合約的具體映射規(guī)則如下：

1）時間自動機(jī)的位置與智能合約的狀態(tài)S是一一對應(yīng)的關(guān)系，且時間自動機(jī)的初始位置l0對應(yīng)合約的初始狀態(tài)s0。

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

3）時間自動機(jī)中的轉(zhuǎn)換等價于智能合約中的TTrans，即函數(shù)。

4）時間自動機(jī)轉(zhuǎn)換上的通道（channel）變量等價于智能合約中對應(yīng)函數(shù)的名稱，即。

5）時間自動機(jī)轉(zhuǎn)換上的守衛(wèi)條件對應(yīng)智能合約中的函數(shù)執(zhí)行條件，即。

6）時間自動機(jī)轉(zhuǎn)換上的輸入和輸出分別等價于智能合約中對應(yīng)函數(shù)的參數(shù)和返回值。

7）時間自動機(jī)轉(zhuǎn)換上的更新等價于智能合約中對應(yīng)函數(shù)對變量的操作，即。

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

ContractDefinition：：=contractname｛

StateDefinition

VariablesDefinition

FunctionDefinition

...

｝，

該語句的作用是根據(jù)contract 關(guān)鍵字定義一個具體的合約結(jié)構(gòu)，其中，name是需要填入的合約名稱，即時間自動機(jī)的名稱。一個完整的智能合約結(jié)構(gòu)包含智能合約的狀態(tài)、變量以及函數(shù)。

StateDefinition ：：=｛enum States｛

S0，S1，S2，…

｝

States private state=States.S0；｝，

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

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

｝，

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

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

Require（state==States.）；

x=block.timestamp-startTime；

｝，

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

3 案例實(shí)現(xiàn)

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

3.1 工作流建模

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

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

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

圖5 預(yù)售合約的時間自動機(jī)模型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，通過隨機(jī)模擬觀察隨著時間自動機(jī)狀態(tài)的遷移而引起的以上參數(shù)量變化，有助于了解模型的工作流，同時也有利于合約功能的完整性設(shè)計。表1 記錄了 buyerAccount、sellerAccount 和depositBalance 的變化情況。從表1可以看出：當(dāng)時間自動機(jī)網(wǎng)絡(luò)處于（deposit，start）時，3 個參數(shù)保持不變；當(dāng)狀態(tài)通過由users 發(fā)送到PreSale 的Submit 信號遷移到（wait，select）時，buyerAccount 為440，sellerAccount 為500，depositBalance為60；當(dāng)狀態(tài)通過由PreSale 發(fā)送到users 的Transfer信號遷移到（end，start）時，buyerAccount 為440，sellerAccount 為560，depositBalance 為0。以上結(jié)果 表示，買家參與了預(yù)售活動并支付了押金，但是沒有在規(guī)定時間內(nèi)補(bǔ)交尾款，因此，買家支付的押金作為賠償轉(zhuǎn)移到了賣家賬戶。

表1 相關(guān)變量在狀態(tài)遷移時的變化情況 Table 1 The change of related variables during state transition

3.3 驗證結(jié)果

根據(jù)預(yù)售合約的文本描述，部分性質(zhì)如下：

1）最終會達(dá)到“end”狀態(tài)：A<>PreSale.end。

2）“end”是可達(dá)狀態(tài)：E<>PreSale.end。

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

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

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

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

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

圖6 驗證結(jié)果Fig.6 Verification results

3.4 Solidity 代碼生成

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

contract PreSale ｛

//枚舉狀態(tài)

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 轉(zhuǎn)換

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 轉(zhuǎn)換

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 轉(zhuǎn)換

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 轉(zhuǎn)換

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 結(jié)束語

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