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

区块链资讯牛市来了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 人参与讨论)

相关推荐

云算宝 iExec 发布新版本 V4,提高分布式云计算可扩展性

区块律动 BlockBeats 消息,分布式云计算项目 iExec 发布了其新版本 V4,该版本解决了区块链应用程序的可扩展性问题,并引入了零费用交易。据悉,iExec 已将 GPU 计算集成到其云市场中。

百度超级链突破智能合约性能极限

超级链的智能合约会设置资源的上限,一旦合约的执行超过上限会自动停止,杜绝死循环的情况发生。

Coinbase Pro 将于 12 月 14 日上线分布式 v\/p\/n 网络兰花协议 Orchid

区块律动 BlockBeats 消息,据 Coinbase 官方信息,太平洋时间12月13日早10点后,即北京时间 12 月 14 日凌晨两点之后,分布式v/p/n网络 Orchid Protocol数字资产 OXT 将上线 Coinbase Pro。

以太坊智能合约版本升级的核心方法

以太坊智能合约版本升级的核心方法

本文主要说明以太坊的注册表合约、代理合约、继承的存储可升级性,以及更多的可升级性方法。 在软件工程中,当发现新的bug和安全风险时,通常会对它们进行修补,并实时推送更新的版本。在智能合约开发中,可升级性并不是那么简单。因此,我们必须采取不同的做法。 以太坊仍处于起步阶段,关于如何升级智能合约版本的争议很多,但我们将介绍一些当今最好的选择。 注意:智能合约版本的可升级性仍然是研究的活跃领域。以下任何

DeFi 中的智能合约风险

DeFi 中的智能合约风险

对于 ERC token 和 DeFi,智能合约中的漏洞是最受关注的,因为 DeFi 作为一个系统,是由来自世界各地的不同的开发者们创建的无数智能合约交织在一起的复杂网络。我们把由智能合约漏洞引起的风险称为智能合约风险。

Bakkt 计划明年推出类似布伦特原油期货合约的数字货币产品

区块律动 BlockBeats 消息,Bakkt 似乎已经制定了明年的产品路线图,该交易所正寻求效仿其母公司洲际交易所 ICE 的模式。

Bakkt 现金结算比特币期货合约首日成交量已突破1000份

Bakkt 现金结算比特币期货合约首日成交量已突破1000份

区块律动 BlockBeats 消息,据 Bakkt 今日官方推特发文称,其于昨日推出的 Bakkt 现金结算比特币期货合约成交量已突破 1000 份,截止发稿时官方最新数据显示,过去 24 小时已成交 1440 份比特币期货合约。

币安实验室投资孵化组合一览:涵盖 11 大类,超 30 个初创项目

币安实验室投资孵化组合一览:涵盖 11 大类,超 30 个初创项目

据区块律动 BlockBeats 了解,币安实验室孵化项目于 2018 年年中启动,重点是「清晰的产品市场契合度」和「为全球区块链生态系统提供可持续增长的切实解决方案」。目前,币安实验室第三季孵化筛选已经于今年 8 月 31 日结束。

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