软件学报ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac Journal of Software,2019,30(9):2608−2619 [doi: 10.13328/jki.jos.005773] ©中国科学院软件研究所版权所有. Tel: +86-10-62562563
面向合同的智能合约的形式化定义及参考实现∗
王璞巍1,2, 杨航天1, 孟佶1, 陈晋川1,2, 杜小勇1,2
1(中国人民大学信息学院，北京 100872)
2(数据工程与知识工程教育部重点实验室(中国人民大学)，北京 100872)
通讯作者: 陈晋川, E-mail:jcchen@ruc.edu
摘要: 智能合约是区块链系统的核心组件，在现实中广泛应用.然而，目前没有关于智能合约的统一定义，在不同的区块链平台上，智能合约的实现也相差甚远.这样将影响公众对智能合约的认知，也对产业的发展造成障碍.回顾了智能合约的发展历史，梳理其概念的变化过程.归纳智能合约的本质，对现有智能合约的实现进行了分析和对比.给出了面向合同的智能合约的形式化定义，为智能合约的标准化奠定基础.提出了独立于区块链平台的、通用的智能合约实现方法.在目前广泛应用的联盟链区块链平台Hyperledger Fabric上面进行了具体实现.最后对未来工作进行了展望.
关键词: 区块链；智能合约；以太坊；超级账本
中图法分类号: TP311
中文引用格式: 王璞巍，杨航天，孟佶，陈晋川，杜小勇.面向合同的智能合约的形式化定义及参考实现.软件学报,2019, 30(9):2608−2619./1000-9825/5773.htm
英文引用格式: Wang PW, Yang HT, Meng J, Chen JC, Du XY. Formal definition for classical smart contracts and a reference implementation. Ruan Jian Xue Bao/Journal of Software, 2019,30(9):2608−2619 (in Chinese)./1000-9825/ 5773.htm
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
∗基金项目: 国家重点研发计划(2016YFB1000702); 贵州财经大学与商务部国际贸易经济合作研究院联合基金(2017 SWBZD08)
Foundation item: National Key Research and Development Plan Task of China (2016YFB1000702); Guizhou University of Finance and Economics and the Ministry of Commerce International Trade and Economic Cooperation Research Institute Joint Fund (2017SWBDZ08)
本文由“区块链数据管理”专题特约编辑于戈教授、牛保宁教授、金澈清教授推荐.
收稿时间:2018-06-09; 修改时间: 2018-08-28; 采用时间: 2018-12-14; jos在线出版时间: 2019-04-10
CNKI网络优先出版: 2019-04-09 17:32:20, knski/kcms/detail/11.2560.TP.20190409.1732.003.html
王璞巍等：面向合同的智能合约的形式化定义及参考实现2609
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)如何准确地描述商务合同?
solidity2)如何让程序员之外的人员理解?
商务合同和智能合约的鸿沟在于：前者采用自然语言，后者是计算机程序.未受过专业训练的人员，比如
企业的法律顾问，无法理解程序，只能在计算机专家的帮助下对比智能合约和商务合同，这里面的难度和风险显而易见.
本文将提出面向合同的智能合约的形式化定义.该定义将基于合同的基本元素(承诺)，用统一的形式化模型来描述商务合同和智能合约.这样做的优点在于：首先，给智能合约严格的、统一的定义；其次，领域专家和程序员将可以在双方都能理解的统一模型下交流，就像数据库中的概念模型.智能合约的形式化定义可以看成是面向智能合约的建模语言，方便非计算机专业的一般用户来描述他们的承诺，再从这些承诺自动地(或半自动地)转换到智能合约具体的实现语言(例如solidity和go).
本文第1节将概述目前智能合约在学术界和工业界的进展，对比分析不同的智能合约实现.第2节将给出智能合约的形式化定义.第3节提出了通用的实现算法.第4节介绍我们在区块链平台Hyperledger Fabric中的参考实现.最后，第5节总结全文并展望未来工作.
2610 Journal of Software软件学报 V ol.30, No.9, September 2019 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由微众银行、万向
王璞巍等：面向合同的智能合约的形式化定义及参考实现2611
区块链和矩阵元三方开发，为分布式商业提供区块链技术基础设施及服务，并于2017年7月31日完全开源.其智能合约主要使用solidity语言开发，智能合约设计理念与以太坊类似.
在表1中，对比分析了上述的智能合约系统.可以看出以太坊,EOS,BCOS对智能合约的实现较为完善.而比特币和Fabric则存在不足.在第4节中，我们将基于Fabric系统实现一个带有状态的智能合约.
Table 1 Comparison of major smart contracts
表1目前主流的智能合约对比分析
支持复杂的商业逻辑支持状态机可以自动执行结果被各方认可无须权威第三方
√√√
比特币× ×
以太坊√√√√√
Fabric √ ×
√√√
EOS √√√√√
BCOS √√√√√
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已达成
2612
Journal of Software 软件学报 V ol.30, No.9, September 2019
了前提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元钱)，而结果是寄货物的动作(a 给b 寄出购买的货物).本文中，我们将动作(action)定义如下.
定义3(动作). 一个动作表示为action :=actname (executor ,object ,input ,output )，其中:
•
actname 是动作的名称,executor 是动作的执行者,object 是动作的作用对象,input 是输入参数,output 是输出参数(act ,exectuor 是必需的(required)，而object ,input 和output 都是可选的(optional)); • 动作的值是一个布尔值,action =fasle 表示没有完成该动作,action =true 表示该动作已完成.动作的默认
值为false.
例如,transfer (a ,b ,10,receipt )表示a 向b 转账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 ),(24,24)).
这是一个有条件承诺，其含义是：如果客户b 在承诺激活的24h 内达成前提deposit (b ,s ,100)=true，那么商家a 就会在承诺就绪后的24h 内完成结果send (a ,b ,goods )=true.但是假设有这样一种情况：如果客户b 在承诺C 1进入过期状态之后才在系统s 上预存100元钱，这时候承诺C 1已失效(可能是商家a 的优惠购买活动已经结束)，系统s 如何处理这一笔预存款呢?此时，系统s 往往需要做出一个关于“承诺C 1过期之后如何处理客户预存款”
版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。
发表评论