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

发布时间：2017-12-09 04:19

  本文关键词：智能合约的形式化验证方法

  更多相关文章： 智能合约 形式化方法 建模 验证 SPIN模型检测工具

【摘要】：智能合约是一种代码合约和算法合同,将成为未来数字社会的基础技术,它利用协议和用户接口,完成合约过程的所有步骤.总结了智能合约主要技术特点和现存的可信、安全等问题,提出将形式化方法应用于智能合约的建模、模型检测和模型验证过程,以支持规模化智能合约的生成.研究提出了一个应用于智能合约生命周期的形式化验证框架和验证方法,针对一个智能购物场景,采用Promela建模语言对智能购物合约进行建模,用SPIN进行了模型检测,验证了形式化方法对智能合约的作用.
【作者单位】： 北京航空航天大学计算机学院;北京中电普华信息技术有限公司;
【基金】：国家自然科学基金项目(91538202)
【分类号】：TP309
【正文快照】： 2016年6月17日,运行在以太坊公有链上的The DA0W」智能合约遭遇攻击,该合约筹集的公众款项不断被一个函数的递归调用转向它的子合约,涉及总额300多万以太币,这是一起严重的智能合约被攻击事件.The DAO本质上是个VC(风险投资基金),通过以太坊筹集到的资金会锁定在智能合约中,

【相似文献】

中国期刊全文数据库 前10条

1 古天龙;董荣胜;;欧洲高校计算机专业的形式化方法课程教学[J];计算机教育;2008年10期

2 柴振荣;《编程中的形式化方法及其应用》会议[J];管理科学文摘;1995年06期

3 郑士贵;智能服务网络形式化方法的模拟和实质[J];管理科学文摘;1997年01期

4 姜利;孙永强;;形式化方法的发展及展望[J];计算机科学;1998年02期

5 张广泉;关于软件形式化方法[J];重庆师范学院学报(自然科学版);2002年02期

6 鹿蕾;;形式化方法B的证明技术[J];现代电子技术;2005年23期

7 陈澎;设计模式形式化方法分析和初步比较[J];计算机工程;2005年02期

8 李建华;李红革;;形式化及其历史发展[J];自然辩证法研究;2008年08期

9 曹源;唐涛;徐田华;穆建成;;形式化方法在列车运行控制系统中的应用[J];交通运输工程学报;2010年01期

10 ;《软件学报》形式化方法和工具专刊征文通知[J];软件学报;2010年07期

中国重要会议论文全文数据库 前7条

1 李文健;;形式化的涵义及其认识论本质[A];1993年逻辑研究专辑[C];1993年

2 吴允曾;;关于形式化的几个问题[A];金岳霖学术思想研究——金岳霖学术思想研讨会论文集[C];1985年

3 郑宇军;石海鹤;薛锦云;;Spec#语言中的形式化特性[A];2005年全国理论计算机科学学术年会论文集[C];2005年

4 雷敏;雷友殉;;一种UML到SDL转换方法的研究与应用[A];2006通信理论与技术新进展——第十一届全国青年通信学术会议论文集[C];2006年

5 苗洁君;王克;;密码模块的形式化设计和验证研究[A];第二十一次全国计算机安全学术交流会论文集[C];2006年

6 缪道期;;评审计算机安全等级[A];第二次计算机安全技术交流会论文集[C];1987年

7 赵晓峰;;城市轨道交通自主化信号系统全面创新实践[A];中国系统工程学会第十八届学术年会论文集——A12系统科学与系统工程理论在各个领域中的应用研究[C];2014年

中国重要报纸全文数据库 前1条

1 殷杰 安军 山西大学科学技术哲学研究中心;21世纪科学哲学的关键词:语境、科学理性与形式化[N];中国社会科学报;2011年

中国博士学位论文全文数据库 前8条

1 刘艳;互联网内容分级服务技术标准体系的形式化设计与验证[D];华中师范大学;2015年

2 钱振江;安全操作系统形式化设计与验证方法研究[D];南京大学;2013年

3 刘强;设计模式的形式化研究及其EMF实现[D];华东师范大学;2011年

4 张鹏;形式化方法在云计算中的应用研究[D];吉林大学;2014年

5 刘洋;网络式软件需求验证的形式化方法研究[D];电子科技大学;2013年

6 王迈;语言形式化原理[D];上海外国语大学;2011年

7 胡静;基于Pi-演算的Web服务形式化描述模型[D];天津大学;2013年

8 周宁;代数化符号模拟验证的应用研究[D];北京交通大学;2015年

中国硕士学位论文全文数据库 前10条

1 王春晓;MDF连续平压质量控制形式化建模及优化研究[D];东北林业大学;2015年

2 王亚丽;面向机器人规划的形式化研究[D];北京化工大学;2015年

3 韩佳芮;基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究[D];兰州交通大学;2015年

4 徐世泽;基于Timed RAISE的RBC切换建模与分析[D];兰州交通大学;2015年

5 郭叶芳;电网控制系统软件可靠性分析的形式化方法研究[D];华北电力大学;2015年

6 黄峰;系统演化的形式化与具体化研究[D];南京邮电大学;2014年

7 Hamza I.Bangura;基于Z规格的软件缺陷形式化方法[D];天津大学;2010年

8 钟琪;软件分析模式的形式化研究[D];西南师范大学;2004年

9 王祥兵;形式化方法的理论及其影响[D];贵州大学;2009年

10 郭忠伟;神经内分泌复杂系统的形式化研究[D];扬州大学;2009年

，

本文编号：1269056