北航分布式实验室:一文了解智能合约的形式化验证案例

区块链资讯牛市来了2019-11-28 22:03:46  阅读 -评论 0

北京航空航天大学分布式实验室 北京航空航天大学云南创新研究院 白晓敏,周楚涵

本文将介绍基于模型检测形式化方法应用于智能合约辅助生成和验证的一个案例,便于大家了解相关的技术路线。作为形式化方法的工程实践,模型驱动工程(MDE)旨在提高程序规范中的抽象级别,从而提高程序规范中的抽象级别,通过使用可执行模型转换来增加程序开发中的自动化,较高级别的模型被转换为较低级别的模型,直到该模型可以使用代码生成或模型解释来执行。

1. MDE方法工程框架

MDE可以支持智能合约的整个生命周期,从建模、验证、代码生成到一致性测试,应用于智能合约的形式化方法流程如图 1所示。

北航分布式实验室:一文了解智能合约的形式化验证案例

图1 智能合约的MDE方法流程

在模型驱动框架下,由于体系结构模型包含的系统特征和信息较多,一般不直接对体系结构模型进行验证和分析,而主要采用模型转换的方式,即将体系结构模型(或子集)转换到另一个形式模型,或者直接转换到模型检测工具或定理证明器,目的是为了重用这些已有的验证和分析能力。我们提出智能合约的模型检测工程化形式化方法框架如图 2所示。一个合约的生成包括:首先,用户提出需求,根据用户需求制定合约文本。然后对合约文本进行形式化描述,并选择合适的建模语言和建模工具对形式化规格说明文档进行建模和性质验证。其中,模型验证包括理论证明和模型检测,在模型检测中,我们通常使用模型转换来验证更多的性质。最后是一致性测试。为了证明合约代码与合约文本在性质和执行力是保持一致的,因此,需要对合约文本和合约代码进行一致性测试。这就是将形式化方法应用于智能合约完整生命周期的框架。

北航分布式实验室:一文了解智能合约的形式化验证案例

图 2 MDA形式化方法应用框架

2. 智能合约的验证案例

我们使用Promela建模语言和检测工具SPIN来建立和验证一个互联网智能购物合约SSC(Smart Shopping Contract)的模型。

SPIN是一个通用的形式化验证工具,以严格的和大多数自动化的方式验证分布式软件模型的正确性。是一种著名的分析验证并发系统逻辑一致性的工具,以其简洁明了和自动化程度高而备受注目。SPIN已成功应用在安全协议验证、控制系统验证、软件验证及最优化规划等领域。作为一种形式化自动验证工具,SPIN可以提供:1)系统建模语言Promela(Process Meta Language),用于直观、明确地描述系统Promela模型规约,而不考虑具体实现细节;2)功能强大而简明的描述系统应满足性质(属性要求)的逻辑表示法;3)提供一套验证系统建模逻辑一致性及系统是否满足所要验证性质的方法。除模型检测之外,SPIN还可以作为模拟器操作,遵循系统的一个可能的执行路径并且向用户呈现所产生的执行轨迹。

基本合约包括商品订货、分销和售后服务,合约可以组合和定制。

合约1: 货物订购与分配:

北航分布式实验室:一文了解智能合约的形式化验证案例

合约2: 售后服务合约:

北航分布式实验室:一文了解智能合约的形式化验证案例

SSC应在用户订单之后触发,并且它具有两个参与者,即用户和商店。

智能购物合约的描述如下:当用户下订单时,他需要将购物所需的资金提交给智能购物合约,智能购物合约暂时持有资金。同时SSC启动两个子进程,用户进程和商店进程。用户进程:如果商家在七天内没有交货,用户将取消交易,SSC会将资金退还给用户,用户进程定时、周期地检测交货状态;商店进程:商家收到订单后,系统判断订单是否结束,如果订单没有超时,则商店发货。SSC需要确保资金的安全性和交易过程中各个状态的可达性。

我们可以简单建立SSC的Promela模型如下:

北航分布式实验室:一文了解智能合约的形式化验证案例

然后我们可以使用模型检测工具SPIN检测SSC模型,模型的模拟结果如4所示。从图4的模型仿真结果可以看出,一旦超时(day= 8),SSC将钱退还给用户。

北航分布式实验室:一文了解智能合约的形式化验证案例

图 4 模型模拟结果(超时退款)

如图 5结果所示,当商店在第二天送货时,SSC将钱转给商店。由于SSC是有限状态模型,通过对SSC的建模和验证,SPIN可以随机生成合约的所有状态,实验结果与合约的预期结果一致。

北航分布式实验室:一文了解智能合约的形式化验证案例

图5 模型模拟结果(交易完成)

基于这个案例,本文针对智能合约存在的可信与安全问题,将形式化方法应用于智能合约的生命周期验证,从形式化描述和形式化验证方法方面进行了详细的阐述。一个好的模型检测工具有助于检查和验证智能合约的各项属性。通过实例可以看出,智能合约可以在合约的不同节段获得不同的状态,当智能合约验证时,SPIN可以随机产生若干种不同的结果,形式化方法可以在智能合约的建立、验证和代码生成中得到重要应用,是智能合约可信和安全性的发展方向。

智能合约形式化验证文章作者:北航云南数字经济研究中心 我要纠错

声明:本文由入驻金色财经的作者撰写,观点仅代表作者本人,绝不代表金色财经赞同其观点或证实其描述。

声明:链世界登载此文仅出于分享区块链知识,并不意味着赞同其观点或证实其描述。文章内容仅供参考,不构成投资建议。投资者据此操作,风险自担。此文如侵犯到您的合法权益,请联系我们kefu@lianshijie.com

参与讨论 (0 人参与讨论)

相关推荐

NEST Protocol:一种分布式价格预言机网络

6)价格序列与波动率以太坊网络的每个区块对应一个 NEST 价格,从而形成价格序列。

中钞区块链技术研究院:四大分布式数字身份架构的对比及研究

中钞区块链技术研究院:四大分布式数字身份架构的对比及研究

原文标题:《巴比特首发 | 中钞区块链技术研究院:四大分布式数字身份架构的对比及研究》原文来源:巴比特概述 数字身份伴随着计算机科学的应用而发展。

Video Blog(VB)基于区块链技术的分布式短视频服务系统

Video Blog 简称 VB,是由一家在新加坡建立的基金会所建立。Video Blog 的关键点是数据分布。为了解决上述问题,Video Blog 提出了 BFT-BPoS/PoC 的共识机制。

​POC挖矿项目众多,SIP超级智能合约如何脱颖而出!

​POC挖矿项目众多,SIP超级智能合约如何脱颖而出!

随着比特币为首的数字货币经济价值不断提升显现,越来越多的人把关注的焦点转移到数字货币上来。那么,数字货币的投资项目众多,如何选择有价值投资的项目呢?目前,数字货币中价值最为突出的就是比特币。比特币是基于POW工作量证的矿币,在经历了第三次产量减半后,很大部分矿工受挫流失,比特币网络的安全性与分散性大幅度降低,挖矿生态陷入恶性循环,这已经不利于矿工继续挖矿了。然而,矿工都是逐利的,哪里能够投入更少而

中信银行打造“区块链”信用证结算!

中信银行打造“区块链”信用证结算!

科技不会改变金融的实质,但却能让金融服务更高效,能让资金供、需方信息不对称的问题更好地解决。近期,中信银行首个区块链项目——基于区块链的国内信用证信息传输系统(简称BCLC)(一期)成功上线,这是国内银行业第一次将区块链技术应用于信用证结算领域。 据中信银行国际业务部总经理助理张栩青介绍,将现在流行的区块链技术应用在国内信用证中,改变了银行传统信用证业务模式,信用证的开立、通知、交单、承兑报文

中国信息技术部门成立区块链研究实验室

中国信息技术部门成立区块链研究实验室

暴走时评:本月初,中国政府对国内的ICO和数字货币交易所的打击在世界范围内引起了强大反响,但政府已经多次声明不会将区块链与数字货币划等号,依然非常重视区块链技术在中国的发展。鉴于中国工业和信息化部成立了一个专门研究区块链的实验室,这一论调也得到了进一步的证实。 虽然中国政府最近在大力打击比特币交易所和ICO,但仍然致力于开发区块链在其他领域的潜力。 据财新网报道,中国工业和信息化部已经成立了一

 分布式账本中的生命科学

分布式账本中的生命科学

生物科学是医学领域涉及遗传研究,疾病预防和生活方式治疗(lifestyle treatments)的学科。它已经存在了很长时间,但区块链技术的基础设施应用给该学科提供了重大进步的可能性。 根据Pistoia Alliance进行的2016年6月份高级制药和生命科学领袖调查,83%的受访者表示,他们预计在五年内将全面采用区块链技术。 Pistoia Alliance是一个全球性的非营利组织,致

区块链vs.核能:日本最大电力公司东京电力(TEPCO)寻求使用区块链减轻对核电的依赖

区块链vs.核能:日本最大电力公司东京电力(TEPCO)寻求使用区块链减轻对核电的依赖

东京电力公司 (TEPCO) 对于能源过度中心化的风险可以说绝不陌生。 也许最著名的就是2011年发生的福岛核电站事故,这个日本最大的能源公司如今正在寻求区块链技术来防止这种灾难再次发生。 然而,从使用微型风车的分布式风力发电到用于存储在电力成本低时购买的电力的智能电池,可替代能源项目一直以来都属于个人慈善事业。 然而,TEPCO风险投资部门主管Jeffrey Char认为区块链能够帮助为这

麦妖榜
更新日期 2019-09-03
排名用户贡献值
1牛市来了30910
2BitettFan24187
3等待的宿命23810
4区块大康20369
5六叶树20310
6linjm122719429
7天下无双16192
8lizhen00215280
9让时间淡忘14586
10yelanyi050511349
返回顶部 ↑