软件学报  2019, Vol. 30 Issue (9): 2608-2619   PDF    
面向合同的智能合约的形式化定义及参考实现
王璞巍1,2 , 杨航天1 , 孟佶1 , 陈晋川1,2 , 杜小勇1,2     
1. 中国人民大学 信息学院, 北京 100872;
2. 数据工程与知识工程教育部重点实验室(中国人民大学), 北京 100872
摘要: 智能合约是区块链系统的核心组件,在现实中广泛应用.然而,目前没有关于智能合约的统一定义,在不同的区块链平台上,智能合约的实现也相差甚远.这样将影响公众对智能合约的认知,也对产业的发展造成障碍.回顾了智能合约的发展历史,梳理其概念的变化过程.归纳智能合约的本质,对现有智能合约的实现进行了分析和对比.给出了面向合同的智能合约的形式化定义,为智能合约的标准化奠定基础.提出了独立于区块链平台的、通用的智能合约实现方法.在目前广泛应用的联盟链区块链平台Hyperledger Fabric上面进行了具体实现.最后对未来工作进行了展望.
关键词: 区块链    智能合约    以太坊    超级账本    
Formal Definition for Classical Smart Contracts and Reference Implementation
WANG Pu-Wei1,2 , YANG Hang-Tian1 , MENG Ji1 , CHEN Jin-Chuan1,2 , DU Xiao-Yong1,2     
1. School of Information, Renmin University of China, Beijing 100872, China;
2. Key Laboratory of Data Engineering and Knowledge Engineering of Ministry of Education(Renmin University of China), Beijing 100872, China
Abstract: Smart contract is one of the key components of blockchain systems, and has been widely applied in practice. However, there are no uniform definitions for smart contract. Moreover, the implementations of smart contracts in different platforms have quite large differences. This situation will affect the public perception of smart contracts and will cause obstacles to the development of the blockchain industry. This study recalls the history of the development of smart contracts, combing out the changes of the concepts, summarizes the essence of smart contracts, and analyzes and compares existing smart contract implementations. The formal definition of classical smart contracts is proposed, which may lay the foundation for the standardization of smart contracts. A common implementation method independent of the blockchain platforms is also given. And a reference implementation based on Hyperledger Fabric is carried out as well. Finally, the conclusion is presented and the future work is listed.
Key words: blockchain    smart contract    Ethereum    hyperledger    

智能合约(smart contract)的概念由跨领域的学者Szabo于1994年提出[1].Szabo将智能合约定义为实现合同条款的计算机程序, 且在不需要可信第三方情况下, 能够确保合同的正确履行.在区块链技术出来之前, 智能合约并未在实际中应用, 因为很难在没有可信第三方情况下保证合同的正确执行.比特币系统是第一个区块链的应用系统, 也第一次实现了智能合约的理念.区块链网络所具备的去中心化、去信任以及不可篡改的特质, 使其成为智能合约天然的执行平台.伴随着区块链技术向多个传统行业的渗透, 智能合约也得到了广泛应用, 其理念和实现技术也有了迅速的发展.与此同时, 越来越多的学者认为, 智能合约就是运行在区块链上的程序, 不再与合同绑定.本文讨论的智能合约是指经典的定义, 即, 用程序定义的合同条款.

在实际应用中, 可以通过智能合约防范履约风险, 让合同履行实现自治, 无需法院等权威机构来督促合约的执行.随着区块链技术的不断发展, 智能合约被应用到不同领域.以农业保险为例, 农业保险品种小、覆盖范围低, 经常会出现骗保事件.将智能合约与农业保险结合之后, 一旦检测到农业灾害, 就会自动启动赔付流程, 这样赔付效率更高[2].此外, 在医疗数据共享领域, 通过智能合约来规范数据的产生者(病人)、数据的保管者(医院)以及数据的使用者(数据分析公司)三方的权责利, 促进医疗大数据的共享[3].

虽然智能合约已经得到了广泛应用, 但一直缺乏严格的定义.目前看到, 对智能合约的描述都是采用自然语言, 表达上不够精确, 且存在分歧.有些文献认为, 智能合约应该是数字化的商务合同.商务合同是指有关各方在进行商务合作的时候需要共同遵守的协议条款, 里面的协议常常涉及各种商业逻辑.例如, 我们摘取了航班延误保险合同的一部分协议:“被保险人持本人购买的有效机票以乘客身份乘坐航班时, 遭遇搭乘航班较预定起飞时间延误, 且延误时间达到保险单所载明的时间, 保险人按保险单所载明金额给付保险金”.这部分协议包含的商业逻辑是“只有当被保险人购买了机票, 以乘客身份乘坐航班, 且航班延误时间超过预定时间, 保险人才会支付保险金”.但是, 数字化商务合同的一个关键问题在于:如何形式化描述这些商业逻辑.

在实际应用中, 几乎所有的区块链平台都宣称支持智能合约, 但实现的方式差别较大.比特币的智能合约类似Forth语言[4], 是基于堆栈的脚本, 不支持循环, 不是图灵完备.加上大小的限制, 使得比特币的智能合约只能支持有限的逻辑, 通常只作为账户拥有者的身份识别.以太坊的智能合约采用图灵完备的solidity语言来编写, 合约具有状态.超级账本旗下的Fabric(Hyperledger Fabric)平台采用Go语言编写智能合约, 功能强大, 但本身并不支持状态.对智能合约模糊的、不一致的描述, 以及不同的实现, 妨碍了公众对智能合约的认知, 影响统一标准的制定, 并阻碍行业的健康发展.

在很多应用场景中, 智能合约担负商务合同的作用.此时, 智能合约将面临两个问题.

1) 如何准确地描述商务合同?

2) 如何让程序员之外的人员理解?

商务合同和智能合约的鸿沟在于:前者采用自然语言, 后者是计算机程序.未受过专业训练的人员, 比如企业的法律顾问, 无法理解程序, 只能在计算机专家的帮助下对比智能合约和商务合同, 这里面的难度和风险显而易见.

本文将提出面向合同的智能合约的形式化定义.该定义将基于合同的基本元素(承诺), 用统一的形式化模型来描述商务合同和智能合约.这样做的优点在于:首先, 给智能合约严格的、统一的定义; 其次, 领域专家和程序员将可以在双方都能理解的统一模型下交流, 就像数据库中的概念模型.智能合约的形式化定义可以看成是面向智能合约的建模语言, 方便非计算机专业的一般用户来描述他们的承诺, 再从这些承诺自动地(或半自动地)转换到智能合约具体的实现语言(例如solidity和go).

本文第1节将概述目前智能合约在学术界和工业界的进展, 对比分析不同的智能合约实现.第2节将给出智能合约的形式化定义.第3节提出了通用的实现算法.第4节介绍我们在区块链平台Hyperledger Fabric中的参考实现.最后, 第5节总结全文并展望未来工作.

1 智能合约概览 1.1 智能合约的定义

在最早的定义中, 智能合约被描述为执行合同条款的计算机程序[1], 或者是数字化的一组承诺[5], 要求智能合约的执行无须可信的第三方.需注意, 承诺是合同的基本要素.在Wikipedia的定义中, 智能合约是一种旨在以信息化方式传播, 验证或执行合同的计算机协议, 允许在没有第三方的情况下进行可信交易, 且这些交易可追踪且不可逆转[6].不难看出, 上述对智能合约的定义, 均要求合约能够实现现实中商务合同, 且要求合约的执行在一个无须可信第三方的环境.我们将其称为“狭义的”或“经典的”智能合约, 这也是本文讨论重点.

随着区块链的问世, 人们终于找到了无中介的可信计算环境.只要网络中多数节点是正常的, 那么整个网络最终的运行结果(共识)也就值得信赖.在这之后, 智能合约得到了迅速发展, 其概念也在发生变化.很多学者认为, 智能合约就是运行在区块链上的程序.在文献[7]中, 智能合约被定义为运行在区块链上的脚本, 实现了多步骤过程的自动化.在文献[8]中, 区块链就是可以被一个网络正确执行的计算机程序, 该网络由互不信任的节点构成.Luu等人[9]则认为:智能合约就是运行在区块链上的程序, 由共识协议保证其正确执行.类似的观点还出现在文献[10-12]中.我们将这类智能合约称为“广义的”智能合约.

此外, 文献[13, 14]强调了智能合约是一个状态机.特别是以太坊中, 智能合约的每次执行都可以看做是从一个状态转移到另一个状态[14].值得注意的是, 商务合同的执行过程也可以被看做是一个状态机.一份合同的执行, 正是按照预先规定的逻辑在不同状态之间转移的过程.

通过上面对智能合约的分析, 我们认为智能合约是具备以下几个性质的一段程序.

1) 支持复杂的商业逻辑;

2) 支持状态机;

3) 可以自动执行;

4) 执行的结果能被参与各方认可;

5) 无须可信第三方.

1.2 智能合约的实现

比特币系统是第1个区块链的应用, 在比特币系统中, 区块链的作用仅仅是记录比特币在各个账户之间的转移.每一笔交易的输出(output)中, 都需要写入一段脚本, 作为该笔输出在未来被使用的条件.大多数情况下, 脚本被用来检验output账户拥有者的身份.脚本也可以用来实现简单的逻辑, 比如指定某个输出只有在区块高度达到某个阈值之后才能使用.但总的来说, 比特币脚本所使用的语言较为简单, 难以实现复杂的商业逻辑.此外, 每个输出只能被使用一次, 也不能表达状态机.

相对于比特币, 以太坊平台可以支持各类智能合约.以太坊采用的语言是图灵完备的, 可以支持复杂的商业逻辑.智能合约以字节码形式存储于区块中, 可以被各个节点执行.合约在发布之后可以被多次调用, 每次调用均需从之前的区块中读取合约的状态和代码, 而调用执行的结果也会存入新的区块中.因此, 智能合约在以太坊上的执行就是一个状态机, 只不过这个状态机是运行在区块链这个去中心的分布式计算平台上.

超级账本是目前影响最为广泛的联盟链项目, 其中最重要的系统是Fabric.与以太坊和比特币不同的是:在Fabric中, 智能合约(即Fabric中的链码, ChainCode)并不存储于区块, 而是一直运行在联盟节点之上.链码采用Go语言, 图灵完备, 可以实现各种复杂的商业逻辑.但是链码没有状态.在比特币或以太坊上运行的智能合约可以看做是某个合约模板的多个实例, 但是在Fabric中没有合约的实例, 所有对区块链上数据的读写都必须经过链码来执行, 类似于MVC模型中的M(model).

EOS(enterprise operation system)是一款为商用分布式应用设计的区块链操作系统, 旨在实现分布式应用的性能扩展.其与比特币、以太坊不同的是:EOS采用了DPOS(delegated proof of stake, 委托权益证明)的共识机制, 同时对智能合约系统进行优化, 并支持多种语言编写合约, 为使用者提供一个没有手续费的智能合约使用平台.

BCOS(BlockChain OpenSource)是聚焦于企业级应用服务的区块链技术开源平台.BCOS由微众银行、万向区块链和矩阵元三方开发, 为分布式商业提供区块链技术基础设施及服务, 并于2017年7月31日完全开源.其智能合约主要使用solidity语言开发, 智能合约设计理念与以太坊类似.

表 1中, 对比分析了上述的智能合约系统.可以看出以太坊, EOS, BCOS对智能合约的实现较为完善.而比特币和Fabric则存在不足.在第4节中, 我们将基于Fabric系统实现一个带有状态的智能合约.

Table 1 Comparison of major smart contracts 表 1 目前主流的智能合约对比分析

1.3 智能合约的安全性

智能合约的安全性一直是人们关心的问题, 而由智能合约的漏洞暴露出来的安全性事件层出不穷, 例如2017年6月的TheDAO事件[15].TheDAO是搭建在以太坊网络上的智能合约, 黑客利用递归函数的漏洞将面向公众筹集的350万个以太坊代币转向自己的地址, 造成了巨大的经济损失.2018年4月, 黑客再次利用BEC代币的智能合约漏洞向BEC代币发起攻击[16], 通过计算溢出, 凭空产生5.7896×1058个代币, 同时, 黑客将这些代币转移到交易平台进行抛售, 导致BEC代币市值几乎归零.

目前有多个公司从事与智能合约的安全性验证工作, 如链安、慢雾等.传统的安全公司也在开始进军智能合约安全领域, 比如360公司最近发现了EOS平台的重大漏洞, 在文献[17]中, 提出了一种智能合约的形式化验证方法.

2 智能合约的形式化定义

基于以上认识, 我们以承诺(commitment)作为基本元素来构建智能合约.承诺是商务合同的基本单位[18], 表示一方对另一方的义务.一份合同通常由一组相互关联的承诺组成.在人工智能领域, 有不少关于形式化描述商业承诺的工作[19, 20].本文将承诺用于描述智能合约, 根据智能合约的特点对承诺进行了重新定义, 并在此基础上完成了智能合约的形式化定义.

2.1 承诺

定义1(承诺).承诺是一个五元组C(x, y, p, r, tc), 含义是承诺人x(promisor)向被承诺人y (promisee)做出承诺, 如果前提p(premise)达成, 就产生结果r(result).其中,

●  前提p和结果r的值是布尔值.值为true表示前提已达成(或结果已完成), 值为false表示前提未达成(或结果未完成);

●  tc(time-constraints)表示该承诺的有效期, tc为true, 承诺才会有效.

一个承诺的生命周期内可能有5种不同的状态.

1)   激活(act):前提p和结果r都为false, 时间未超出承诺的有效期.表示承诺有效, 在等待前提p的达成和结果r的完成;

2)   就绪(bas):前提p为true, 结果r为false, 时间未超出承诺的有效期.表示承诺已生效且前提p已经达成, 在等待结果r的完成;

3)   满足(sat):前提p和结果r都为true.表示前提p已达成, 结果r也已完成, 承诺已被履行;

4)   过期(exp):前提p和结果r都为false, 时间已超出承诺的有效期.表示在承诺失效时, 前提p未能达成而结果r也未能完成;

5)   违约(vio):前提p为true, 但结果r为false, 时间已超出承诺的有效期.表示当承诺失效时, 尽管b已达成了前提p, 但a仍然未履行其承诺完成结果r, 已经违约.

图 1所示:如果在创建承诺时, 前提p和结果r都为false, 承诺进入激活状态, 我们将这样的承诺成为有条件承诺, 也就是承诺人履行该承诺存在前提条件; 如果前提p为true, 结果r为false, 承诺进入就绪状态, 我们将这样的承诺成为无条件承诺, 也就是承诺人将无条件履行该承诺; 在激活状态下, 如果时间超出了承诺的有效期, 前提p和结果r都未能达成(完成), 承诺进入了过期状态, 此时承诺已经失效; 在激活状态下, 如果前提p达成(也就是使得p=true), 该承诺变成无条件承诺, 进入就绪状态; 在就绪状态下, 如果时间超出了承诺的有效期, 结果r依然未能完成, 承诺进入违约状态, 表示承诺人已违约.在就绪状态下, 在有效期内, 承诺人完成了结果r(也就是使得r=true), 进入满足状态, 表示承诺人履行了其承诺.

Fig. 1 The lifecycle of a commitment 图 1 承诺的生命周期图

从承诺生命周期图中我们可以看到, 承诺的有效期与激活状态和就绪状态有关.本文中, 我们将承诺有效期(time constraints)定义如下.

定义2(承诺有效期).承诺有效期是一个二元组tc:=(pdact, pdbas), 其中:pdact表示承诺进入激活(act)状态之后, 对前提p的完成时间限制; pdbas表示承诺进入就绪(bas)状态之后, 对结果r的完成时间限制.若这两个限制满足, tc为true; 否则, tc为false.

例如, tc=(24, 24)表示前提p需要在承诺进入激活状态24h(默认单位为h)之内达成(即pdact=24), 否则承诺将进入过期状态; 结果r需要在承诺进入到就绪状态之后24h之内完成(即pdbas=24), 否则承诺进入违约状态.

在承诺中, 前提或结果可能是预期的动作.例如, 商家a向客户b做出一个承诺, 如果b在系统上预存100元货物钱, a就给b寄出相应货物.这里, 前提是预存钱的动作(b在系统上预存100元钱), 而结果是寄货物的动作(ab寄出购买的货物).本文中, 我们将动作(action)定义如下.

定义3(动作).一个动作表示为action:=actname(executor, object, input, output), 其中:

●  actname是动作的名称, executor是动作的执行者, object是动作的作用对象, input是输入参数, output是输出参数(act, exectuor是必需的(required), 而object, inputoutput都是可选的(optional));

●  动作的值是一个布尔值, action=fasle表示没有完成该动作, action=true表示该动作已完成.动作的默认值为false.

例如, transfer(a, b, 10, receipt)表示ab转账10元的动作, 其中, transfer是动作名, a是动作的执行者, b是动作的作用对象, 10是输入参数, receipt(收据)是输出参数.transfer(a, b, 10, receipt)的默认值是false, 表示b还没有收到a转过来的10元钱, 也就是动作还未完成.如果transfer(a, b, 10, receipt)=true, 则表示该动作已经完成(a收到b转账过来的10元钱).

此时, 前面提到的那个承诺就可以写为

$ {C_1} = C(a, b, deposit(b, s, 100), send(a, b, goods), \left( {24, 24} \right)). $

这是一个有条件承诺, 其含义是:如果客户b在承诺激活的24h内达成前提deposit(b, s, 100)=true, 那么商家a就会在承诺就绪后的24h内完成结果send(a, b, goods)=true.但是假设有这样一种情况:如果客户b在承诺C1进入过期状态之后才在系统s上预存100元钱, 这时候承诺C1已失效(可能是商家a的优惠购买活动已经结束), 系统s如何处理这一笔预存款呢?此时, 系统s往往需要做出一个关于“承诺C1过期之后如何处理客户预存款”的承诺.可以看到, 承诺的前提可能与另一个承诺的状态有关系.系统s可以做出如下承诺:

$ {C_2} = C(s, b, {C_1}\_exp, deposit(b, s, x), refund(s, b, x), \left( {\infty , 24} \right)). $

其中,

●  C1_exp是一个布尔变量:如果承诺C1处于过期(exp)状态, 值为true; 否则, 值为false;

●  有效期tc=(∞, 24)表示承诺在激活状态不会过期, 但如果在就绪状态下超过24h还未完成结果, 系统s将会违约.这个承诺的具体含义是:系统s向客户b承诺, 如果b在承诺C1过期之后还在系统上预存钱, 系统将会在24h内退钱给b.

这里, 我们通过一个机票延误险的案例来说明我们定义的承诺.在机票延误险场景中, 乘机人购买机票之后在系统上预存10元保费; 保险公司再在系统上预存相应的赔偿金1000元; 如果保险公司没有按时预存赔偿金, 系统就直接将保费退还给用户; 如果保险公司预存了赔偿金, 若航班没有延误, 或者延误时间少于4h, 系统就将乘机人预存的保费转账给保险公司, 同时退还保险公司预存的赔偿金.如果航班延误超过4h, 系统也会将保费转账给保险公司, 但是会将保险公司预存的赔偿金赔偿给乘机人.假设a表示保险公司, b表示乘机人, c表示航空公司, s表示系统, MAX-T表示保险最大有效期, 他们的承诺如下.

●  C3=C(b, s, true, buy_ticket(b, c, flightno), (∞, 24)).含义是乘机人向系统承诺:将会向航空公司c购买航班号为flightno的机票(buy_ticket(b, c, 5210)).这个承诺是无条件承诺, 没有前提条件, 承诺初始为就绪状态.承诺有效期是(∞, 24), 即乘机人将在24h购买机票;

●  C4=C(b, s, C3_sat, deposit(b, s, 10), (24, 0.5)).含义是乘机人向系统承诺:如果承诺C3进入满足状态(也就是按时购买了机票), 他就在系统上预存10元保费(deposit(b, s, 10)).承诺有效期是(24, 0.5), 即乘机人需要在24h内购买机票, 以及乘机人将在购买机票后0.5h内在系统上预存保费;

●  C5=C(a, s, C3_sat, C4_sat, deposit(a, s, 1000), (72, 1)).含义是保险公司向系统承诺:如果承诺C3C4都进入了满足状态(也就是乘机人按时购买了机票并且在系统上按时预存了10元保费), 它将在系统上预存1000元赔偿金(deposit(a, s, 1000)).承诺有效期是(72, 1), 即保险公司只在72h内接受乘机人预存保费, 且将在乘机人购买机票和预存保费之后1h内在系统上预存赔偿金;

●  C6=C(s, b, C5_vio, refund(s, b, 10), (MAX-T, 2)).含义是系统向乘机人承诺:如果承诺C5进入违约状态(也就是保险公司未能按时预存保险金), 系统将向用户退还预存保费(refund(s, b, 10)).承诺有效期是(MAX-T, 2), 即, 系统将在保险公司违约之后2h内退还保险金;

●  C7=C(s, b, C5_satflight_delay(c, flightno, 4.0), transfer(s, a, 10), compensate(s, b, 1000), (MAX-T, 24)).含义是系统向乘机人承诺:如果承诺C5进入满足状态(也就是保险公司预存了赔偿金), 并且航空公司c航班号为flightno的飞机延误4h以上(flight_delay(c, flightno, 4.0)), 系统将把10元保费转账给保险公司(transfer(s, a, 10)), 同时向乘机人赔偿1000元(compensate(s, b, 1000)); 承诺有效期是(MAX-T, 24), 即, 系统将在完成投保且航班延误后24h内, 将保费转账给保险公司和支付用户赔偿金;

●  C8=C(s, a, C5_sat¬flight_delay(c, flightno, 4.0), transfer(s, a, 10), refund(s, a, 1000), (MAX-T, 24)).含义是系统向保险公司承诺:如果承诺C5进入满足状态(也就是保险公司预存了赔偿金), 并且航空公司c航班号为flightno的飞机没有延误, 或延误在4h内(¬flight_delay(c, flightno, 4.0)), 系统将把10元保费转账给保险公司(transfer(s, a, 10)), 同时向保险公司退还1000预存赔偿金(refund(s, a, 1000)).

2.2 智能合约:有限自动机

定义4(智能合约). 智能合约就是定义在一组承诺之上的有限自动机SC:=(CC, A, S, s0, δ, F), 其中,

●  CC={C1, C2, …, Cn}是一个有限的承诺集合;

●  A是这些承诺涉及到的动作的集合(包括超时动作, 也就是时间超出了承诺的有效期);

●  S={s0, s1, s2, …, sm}是一个有限的状态集合.状态siCC中所有承诺的状态共同决定:

$ {s_i} = \{ {C_1}:state, {C_2}:state, \ldots , {C_n}:state\} (state \in \{ act, sat, bas, exp, vio\} ); $

●  s0是初始状态, 其中, CC中所有承诺或者处于激活状态(有条件承诺), 或者就绪状态(无条件承诺);

●  δ:S×AS是状态变迁函数.A中的动作会促使CC中承诺的状态发生变化, 从而引起智能合约的状态发生变化;

●  FS是一个有限的终止状态集合.

智能合约由一组承诺构成, 例如第2.1节给出了机票延误险场景中的6个承诺CC={C3, C4, …, C8}, 这些承诺里涉及的动作有:buy_ticket(b, c, 5210)乘机人购买机票, deposit(b, s, 10)乘机人预存延误险保费, deposit(a, s, 1000)保险公司预存赔偿金, refund(s, b, 10)系统退还乘机人保费, refund(s, a, 1000)系统退还保险公司预存赔偿金, flight_delay(c, flightno, 4.0)航空公司航班延误超过4h, transfer(s, a, 10)系统将乘机人保费转账给保险公司, compensate(s, b, 1000)系统向乘机人支付赔偿金, timeout时间超过承诺有效期.

承诺是有状态的, 对于智能合约的调用, 会触发承诺的状态发生改变.因而, 智能合约又是指定义在一组承诺之上的有限自动机.如图 2所示, 可以在这些承诺之上生成一个智能合约(有限自动机), 其初始状态为s0={C3: bas, C4:act, C5:act, C6:act, C7:act, C8:act}, 也就是除了承诺C3是就绪状态之外, 其他的承诺都是激活状态.在初始状态s0上, 乘机人在承诺C3的有效期内执行购买机票的动作buy_ticket(b, c, flightno)之后, 智能合约的状态就会变化为s2={C3:sat, C4:bas, C5:act, C6:act, C7:act, C8:act}.也就是承诺C3的状态从就绪(bas)变为满足(sat), 承诺C4的状态从激活(act)变为就绪(bas), 其余承诺的状态没有变化.

Fig. 2 An example of smart contract 图 2 智能合约:有限自动机

为了简便, 我们用发生了变化的那些承诺状态来表示智能合约的新状态.例如, 图 2就将s2表示为C3:sat, C4: bas, 因为从s0变化到s2, 只有承诺C3C4的状态发生变化.在s2状态下, 若乘机人执行预存保费的动作(deposit(b, s, 10)), 智能合约的状态就会变化为s4=C4:sat, C5:bas.紧接着, 如果保险公司执行预存赔偿金的动作(deposit(a, s, 1000)), 智能合约的状态会变化为s6=C5:sat.紧接着, 如果航班真的发生了延误(flight_delay(c, flightno, 4)), 智能合约进入状态s8=C7:bas.系统再将保费转账给保险公司, 但将保险公司1000元的预存金赔偿给客户, 智能合约的状态最终进入终止状态s10=C7:sat.这就是从智能合约从初始状态到终止状态的一条路径:s0s2s4s6s8s10.根据初始状态s0和这条路经, 可以得出终止状态s10的完整表示{C3:sat, C4:sat, C5:sat, C6:act, C7:sat, C8:act}, 也就是承诺C3~C5C7最终进入满足状态.此外, 从图 2可以看出, 这个智能合约还有多条执行路径.

3 智能合约的通用实现方法

本节讨论如何在区块链平台上实现智能合约.考虑到合约内容的多样性, 要求区块链平台能够运行图灵完备的程序.本节先介绍智能合约在区块链平台的执行过程, 然后提出一种通用的算法.

3.1 智能合约在区块链平台的运行过程

图 3所示, 合约发布到链上, 有一个初始状态.每次调用(包括指令和参数)都需要读取合约的逻辑和上一个状态, 执行之后将新的状态存入区块.智能合约就是运行在区块链上的状态机.

Fig. 3 The process of executing smart contracts on blockchain platforms 图 3 智能合约在区块链平台上执行的通用过程描述

3.2 通用算法

智能合约是一个状态机, 因此必然包含状态机和一系列接口函数.对智能合约的每次调用, 都通过接口函数来完成, 相当于对状态机施加的动作.状态机将实现合约所包含的一系列承诺, 以及承诺之间的约束.算法1介绍了对智能合约的调用过程.

算法1. invokeContract.

Input:

   contractID; //合约的ID;

   invokerID; //调用者ID, 即公钥;

   operation; //操作, 包括参数;

   sig; //调用者对操作的签名;

Output:

   布尔值; //表示调用是否成功.

contractInfoloadContract(contractID); //contractInfo包含合约的状态以及各属性的值

If (!verifySig(invokerID, operation, sig)) //检验签名是否正确

   Return false;

If (!verifyOperation(contractInfo, invokerID, operation))

   //检查在合约当前的状况下, 调用者是否可以执行这个操作

   Return false;

contractInfoexecuteContract(contractInfo, invokerID, operation, sig);

   //执行合约, 修改相应属性的值, 并根据合约的预制规则得到新的合约状态

   //本次操作记录及签名也会保存到contractInfo

If (saveContract(contractInfo))

   Return true;

Else

   Return false;

注意输入参数sig, 对合约的每次调用操作均必须由调用者签名.

●  算法第1步, 从区块链上读取指定的合约信息, 存储到结构体contractInfo中;

●  第2步将检验签名的有效性, operation相当于明文, sig为对应密文, verifySig函数将尝试使用调用者公钥(invokerID)去验证签名;

●  第3步是检查操作的有效性, 根据合约的逻辑, 判断当前状态下该调用者是否可以执行相应操作.这里, 合约的逻辑实现了所有的承诺以及承诺之间的约束;

●  第4步将执行操作, 根据状态转移矩阵修改合约的状态, 并修改合约的属性值.注意, 本次操作和签名也会保存作为合约的操作日志;

●  最后一步是将新的合约信息保存到区块链上.

下面, 从两方面对算法1进行分析, 我们将讨论其性能及其在执行过程中如何与外界可信地交互.

算法1只是一个框架, 在具体执行时会调用不同的智能合约, 因此整体执行性能取决于智能合约的复杂程度.因此, 我们在这里只能讨论在区块链环境中执行一些基本操作的时间开销.算法1所涉及的基本操作主要是从区块链上读取合约的状态, 以及向区块链上写入更新后的合约状态.通常, 读取操作可以基于节点的本地状态数据库完成, 时间开销很小.而写入操作需要和网络中其他节点保持一致, 其时间开销主要取决于所采用的共识协议类型以及网络的规模.一般而言, 公链的写入耗时较长, 如比特币网络在1h左右(即6次确认), 以太坊则在10s左右.联盟链的网络规模较小, 单次写入耗时可以在亚秒级.本文在实验中采用的是Hyperledger Fabric, 在单机上虚拟多个节点, 实验中平均每次写入耗时约数百毫秒;

算法1中对智能合约进行调用时, 有时会涉及与外部的交互问题, 比如确认航班是否延误.目前采用的办法是利用类似oraclize这样的预测机, 保证各个节点拿到可信的相同的外部数据.Oraclize依赖于TLS公证(TLSnotary)来提供诚实地从互联网页面安全获取信息的能力.

4 参考实现

本节将介绍基于Hyperledger Fabric系统对航空延误保险例子的实现.在第4.1节简述基于Fabric平台搭建的区块链网络; 第4.2节介绍程序模块.我们的代码可以从https://github.com/RucBlockchain/SmartContract链接下载.

4.1 平台介绍及系统部署

在Hyperledger Fabric 1.0中有两种类型节点.一类是peer节点, 负责存储区块链.Chaincode(链码)部署在peer节点上, 可以对区块链进行读写.多个peer节点构成一个组织(organization), 每个组织有一个CA认证中心, 负责分发公钥和私钥.多个组织构成一个通道(channel), 只有通道内的peer节点才能参与交易(也就是一个联盟链); 另一类是orderer(排序)节点, 不负责存储区块链, 只负责对peer节点提交的交易进行排序, 批量打包后生成新的区块, 再发送到peer节点加入到区块链之中.

我们的实验构建了一个Hyperledger Fabric网络, 其中有一个通道, 包含了两个组织(org1和org2), 每个组织里有两个peer节点, 另外有3个orderer节点提供共识服务.Chaincode是一段由go语言编写的代码, 可以对区块链进行读写操作.如图 4所示, Hyperledger Fabric 1.0上, chaincode的执行过程如下.

Fig. 4 The process of executing chaincodes on hyperledger fabric 1.0 图 4 Hyperledger Fabric 1.0上, chaincode的执行过程

1)   用户向某个peer节点(称为提交节点)发出调用chaincode的请求;

2)   提交节点执行chaincode代码.当需要进行交易(就是往区块链写入交易)的时候, 向channel中的几个peer节点(称之为背书节点)发出背书请求;

3)   背书节点模拟执行交易(只是模拟, 此时并不会真正将交易写入区块链), 得到模拟执行的结果;

4)   提交节点收集背书节点返回的模拟结果;

5)   提交节点向某一个排序节点提交交易请求(包括背书结果);

6)   排序节点是对收到的交易进行批量打包生成新的区块;

7)   排序节点将新生成的区块发送到提交节点所在channel中的每个peer节点;

8)   最后, peer节点验证区块中每个交易的背书结果是否符合事先设定好的要求, 只会将符合要求的交易写入到区块链之中.

在这个执行过程中, 我们发现:1)通过chaincode写入区块链的交易都是被背书点验证的, 且通过排序服务在每个节点上都保证了数据的一致性, 不需要权威第三方再进行验证; 但是, 2) chaincode实际上只提供了访问区块链的接口(API), 不会记录chaincode的状态以及实现状态转移.在我们的实验中, 在chaincode基础上实现了一种支持状态机的通用智能合约.

4.2 基于chaincode的智能合约实现思路

我们基于chaincode实现了一个状态机, 可以在区块链存储智能合约的状态以及实现状态转移.如图 5所示, 外部调用通过入口函数进行转发.状态机包括初始化模块、事件响应模块、事件注册模块及具体的action函数.

Fig. 5 The architecture of smart contract program 图 5 智能合约程序架构

●  初始化模块负责构造一个合约实例以及注册合约的参与各方;

●  事件注册模块将建立状态机的状态转移矩阵, 即:接收到某个事件时, 状态应如何转变;

●  事件响应模块将根据状态转移矩阵和输入的事件对状态机的状态进行修改;

●  最后, action函数实现具体的动作(action), 如buy_ticket, deposit等等.

在航空延迟险的例子中, 智能合约需根据航班的信息来决定是否赔付.在实际系统中, 可以由多家保险公司或其他机构主动获取航班信息, 并写入区块链.智能合约将根据这些数据来自动判定航班是否延误.多家公司数据相互印证, 提高了结果的可信性.此外, 由于写入区块链的数据将不可更改, 客观上也会约束保险公司的行为.

5 总结和展望

本文总结了目前智能合约的发展状况, 提出了对智能合约的形式化定义, 以及通用的实现算法.在目前广泛使用的联盟链平台Hyperledger Fabric上实现了上述算法, 检验了形式化定义和算法的有效性.之后的工作将致力于开发一种可视化的智能合约的建模工具, 使得用户可以轻松实现合同向智能合约的转换, 并研究智能合约建模语言向程序语言(如go, solidity, Java等)的映射方法.

参考文献
[1]
[2]
[3]
[4]
[5]
[6]
[7]
Christidis K, Devetsikiotis M. Blockchains and smart contracts for the Internet of things. IEEE Access, 2016, 4: 2292-2303. [doi:10.1109/ACCESS.2016.2566339]
[8]
Atzei N, Bartoletti M, Cimoli T. A survey of attacks on Ethereum smart contracts SoK. In: Maffei M, Ryan M, eds. Proc. of the 6th Int'l Conf. on Principles of Security and Trust. Vol.10204. New York: Springer-Verlag, 2017. 164-186.[doi: 10.1007/978-3-662-54455-6_8]
[9]
Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In: Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security (CCS 2016). New York: ACM Press, 2016. 254-269.[doi: 10.1145/2976749.2978309]
[10]
Zhang F, Cecchetti E, Croman K, Juels A, Shi E. Town crier: An authenticated data feed for smart contracts. In: Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security (CCS 2016). New York: ACM Press, 2016. 270-282.[doi: 10.1145/2976749.2978326]
[11]
Fairfield J. Smart contracts, Bitcoin bots, and consumer protection. Washington and Lee Law Review Online, 2014, 71(2): 35-50.
[12]
Seijas PL, Thompson S, McAdams D. Scripting smart contracts for distributed ledger technology. Report 2016/1156. Cryptology ePrint Archive, 2016.
[13]
Mavridou A, Laszka A. Designing secure Ethereum smart contracts: A finite state machine based approach. arXiv.1711.09327. 2017.
[14]
[15]
[16]
[17]
Hu K, Bai XM, Gao LC, Dong AQ. Formal verification method of smart contract. Journal of Information Security Research, 2016, 2(12): 1080-1089(in Chinese with English abstract). [doi:10.3969/j.issn.2096-1057.2016.12.003]
[18]
Desai N, Chopra AK, Singh MP. Representing and reasoning about commitments in business processes. In: Proc. of the 22nd Conf. on Artificial Intelligence. AAAI, 2007. 1328-1333.
[19]
Chesani F, Mello P, Montali M, Torroni P. Representing and monitoring social commitments using the event calculus. Autonomous Agents and Multi-Agent Systems, 2013, 27(1): 85-130. [doi:10.1007/s10458-012-9202-0]
[20]
Desai N, Chopra AK, Singh MP. Amoeba:A methodology for modeling and evolving cross-organizational business processes. ACM Trans. on Software Engineering Methodology, 2009, 19(2): Article 6. [doi:10.1145/1571629.1571632]
[17]
胡凯, 白晓敏, 高灵超, 董爱强. 智能合约的形式化验证方法. 信息安全研究, 2016, 2(12): 1080-1089. [doi:10.3969/j.issn.2096-1057.2016.12.003]