智能合约的时间约束模式及其形式化验证
作者:
作者单位:

作者简介:

赵颖琪(1994-),女,硕士,主要研究领域为智能合约,形式化方法;
李广元(1962-),男,博士,研究员,CCF专业会员,主要研究领域形式化方法,实时系统模型检测;
朱雪阳(1971-),女,博士,副研究员,CCF高级会员,主要研究领域为形式化方法,嵌入式系统设计;
包玉龙(1995-),男,硕士,主要研究领域为形式化方法,智能合约.

通讯作者:

朱雪阳,E-mail:zxy@ios.ac.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(62072443)


Time Constraint Patterns of Smart Contracts and Their Formal Verification
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    智能合约是一套以数字形式定义的承诺.通过智能合约,可以大大减少协议制定的中间环节,提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入,智能合约的作用必然越来越突出,智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视,但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.通过分析典型智能合约,对智能合约时间约束的不同表现形式进行梳理,提炼出相应的时间约束模式并对其进行形式化;定义Solidity智能合约到时间自动机的转换规则,并实现其到实时模型检测工具UPPAAL入口模型的自动转换;再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究,结果表明了所提炼模式的普遍性以及所提出形式化验证方案的可行性和有效性.

    Abstract:

    Smart contract consists of a set of commitments defined in digital form. Smart contracts can greatly reduce the intermediate links in agreement formulation and improve the efficiency of agreement formulation. Blockchain technology provides a trusted platform for the execution of smart contracts. As the application of blockchain technology expands and deepens, the role of smart contracts will become more and more important, and the potential reliability problems, however, may cause huge lose to participants. The reliability of smart contracts has received more and more attention, but there is no systematic research on problems caused by the time properties of smart contracts. This study analyzes typical smart contracts, sorts out the different manifestations of time constraints, summarizes several time constraint patterns of smart contracts and formalizes them; defines transform rules from Solidity smart contracts to the timed automata. The translation from smart contracts to the model of model checker UPPAAL is then implemented and UPPAAL is used to verify the time properties of smart contracts. Case study is carried out on two practical smart contracts. The results show that the patterns extracted are general and the formal verification solution proposed is feasible and efficient.

    参考文献
    相似文献
    引证文献
引用本文

赵颖琪,朱雪阳,李广元,包玉龙.智能合约的时间约束模式及其形式化验证.软件学报,2022,33(8):2875-2895

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号