智能合约的形式化验证方法

被引：61

作者：

胡凯 ^{[1
]}

白晓敏 ^{[1
]}

高灵超 ^{[2
]}

董爱强 ^{[2
]}

机构：

[1] 北京航空航天大学计算机学院

[2] 北京中电普华信息技术有限公司

来源：

信息安全研究 | 2016年 / 2卷 / 12期

关键词：

智能合约; 形式化方法; 建模; 验证; SPIN模型检测工具;

D O I：

暂无

中图分类号：

TP309 [安全保密];

学科分类号：

081201 ; 0839 ; 1402 ;

摘要：

智能合约是一种代码合约和算法合同,将成为未来数字社会的基础技术,它利用协议和用户接口,完成合约过程的所有步骤.总结了智能合约主要技术特点和现存的可信、安全等问题,提出将形式化方法应用于智能合约的建模、模型检测和模型验证过程,以支持规模化智能合约的生成.研究提出了一个应用于智能合约生命周期的形式化验证框架和验证方法,针对一个智能购物场景,采用Promela建模语言对智能购物合约进行建模,用SPIN进行了模型检测,验证了形式化方法对智能合约的作用.

引用

页码：1080 / 1089

页数：10

共 4 条

[1] LDP协议一致性测试研究与实现[D]. 张颖蓓.国防科学技术大学. 2003
[2] Model-Driven Engineering of Reliable Fault-Tolerant Systems—A State-of-the-Art Survey[J] . Vidar Sl?tten,Peter Herrmann,Frank Alexander Kraemer.Advances In Computers . 2013
[3] Symmetry and model checking[J] . E. Allen Emerson,A. Prasad Sistla.Formal Methods in System Design . 1996 (1)
[4] Decentralized autonomous organization:The DAO .2 https://en.wikipedia.org/wiki/Decemralizedautonomousorganization . 2016

← 1 →