一种基于时间自动机的安全智能合约生成方法

刘 阳，张圣杰

（上海海事大学 物流科学与工程研究院，上海 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 代码，该代码通过以太坊测试网络被证明具有有效性。下一步将规范并扩展从模型到代码的映射规则，同时从语义层面给出严格的证明，从模型中获取更全面的智能合约信息，减少代码自动生成过程中的人为干预。此外，利用模型学习技术从输入、输出中自动推断智能合约的运行时模型也是今后的研究方向。