微信服务号

微信订阅号

2025年7月20日 7:46 星期日
首页 > 过刊浏览>2022年第33卷第8期 >2875-2895. DOI:10.13328/j.cnki.jos.006603
PDF HTML阅读 XML下载 导出引用 引用提醒
智能合约的时间约束模式及其形式化验证
作者:
作者简介:

赵颖琪(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:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [58]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    智能合约是一套以数字形式定义的承诺.通过智能合约,可以大大减少协议制定的中间环节,提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入,智能合约的作用必然越来越突出,智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视,但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.通过分析典型智能合约,对智能合约时间约束的不同表现形式进行梳理,提炼出相应的时间约束模式并对其进行形式化;定义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.

    参考文献
    [1] He HW, Yan A, Chen ZH.Survey of smart contract technology and application based on blockchain.Journal of Computer Research and Development, 2018, 55(11):2452-2466(in Chinese with English abstract).
    [2] Zhu XY.Formal analysis of the DAO exploit.Information Technology and Network Security, 2021, 40(5):13-19(in Chinese with English abstract).
    [3] Zhou Y.Research on promising blockchain smart Contract[MS.Thesis].Shanghai:Shanghai Jiao Tong University, 2018(in Chinese).
    [4] Dannen C.Introducing Ethereum and Solidity.New York:Berkeley Press, 2017.69-88.
    [5] Liu DL.Research and application status, problems and suggestions of blockchain smart contract technology in the financial field.Hainan Finance, 2016(10):27-31(in Chinese with English abstract).
    [6] Zhao YH, Yuan BH, Liang J.Application of blockchain technology in medical field.China Medical Education Technology, 2018, 32(1):1-7(in Chinese with English abstract).[doi:10.13566/j.cnki.cmet.cn61-1317/g4.201801001]
    [7] Cai YB.On the conformity of smart contract to the private law system.Oriental Law, 2019, 68(2):68-81(in Chinese with English abstract).[doi:10.19404/j.cnki.dffx.20190304.002]
    [8] Zhao YQ, Zhu XY, Li GY, et al.Verification of smart contracts with time constraints.Journal of Applied Sciences, 2021, 39(1):1-16(in Chinese with English abstract).
    [9] Gao F.The difficult on fix vulnerabilities of blockchain smart contracts.Computer and Network, 2018, 44(12):50-51(in Chinese with English abstract).
    [10] Ni YD, Zhang C, Yin TT.A survey of smart contract vulnerability research.Journal of Cyber Security, 2020, 5(3):78-99(in Chinese with English abstract).
    [11] Qiu XX, Ma ZF, Xu MK.Ethereum smart contract security vulnerability scenario analysis.Information Security And Communications Privacy, 2019(2):46-55(in Chinese with English abstract).
    [12] Eric.FlightDelay smart contract.2018.https://github.com/causztic/archwing/blob/master/contracts/UserInfo.sol
    [13] Ethereum, HiBlock.Auction.2021.https://learnblockchain.cn/docs/solidity/solidity-by-example.html#index-1
    [14] Behrmann G, David A, Larsen KG, et al.Uppaal 4.0.In:Proc.of the Int'l Conf.on the Quantitative Evaluaiton of Systems (QEST).IEEE Computer Society, 2016.125-126.
    [15] Luu L, Chu DH, Olickel H, et al.Making smart contracts smarter.In:Proc.of the 2016 ACM SIGSAC Conf.on Computer and Communications Security.2016.254-269.
    [16] Mainticore.https://github.com/trailofbits/manticore
    [17] Mossberg M, Manzano F, Hennenfent E, et al.Manticore:A user-friendly symbolic execution framework for binaries and smart contracts.In:Proc.of the 34th IEEE/ACM Int'l Conf.on Automated Software Engineering (ASE).IEEE, 2019.1186-1189.
    [18] Mythril.https://github.com/ConsenSys/mythril
    [19] Mythril:Smashing Ethereum smart contracts for fun and real profit.2018.https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf
    [20] Tsankov P, Dan A, Drachsler-Cohen D, et al.Securify:Practical security analysis of smart contracts.In:Proc.of the 2018 ACM SIGSAC Conf.on Computer and Communications Security.2018.67-82.
    [21] Ahrendt W, Bubel R, Ellul J, et al.Verification of smart contract business logic.In:Proc.of the Int'l Conf.on Fundamentals of Software Engineering.Cham:Springer, 2019.228-243.
    [22] Alt L, Reitwiessner C.SMT-based verification of solidity smart contracts.In:Proc.of the Int'l Symp.on Leveraging Applications of Formal Methods.Cham:Springer, 2018.376-388.
    [23] Amani S, Bégel M, Bortin M, et al.Towards verifying ethereum smart contract bytecode in Isabelle/HOL.In:Proc.of the 7th ACM SIGPLAN Int'l Conf.on Certified Programs and Proofs.2018.66-77.
    [24] Bhargavan K, Delignat-Lavaud A, Fournet C, et al.Short paper:Formal verification of smart contracts.In:Proc.of the 11th ACM Workshop on Programming Languages and Analysis for Security (PLAS), in conjunction with ACM CCS.2016.91-96.
    [25] Ma FC, Fu Y, Ren M, et al.EVM*:From offline detection to online reinforcement for ethereum virtual machine.In:Proc.of the 26th IEEE Int'l Conf.on Software Analysis, Evolution and Reengineering (SANER).IEEE, 2019.554-558.
    [26] Bai XM, Cheng ZJ, Duan ZB, et al.Formal modeling and verification of smart contracts.In:Proc.of the 7th Int'l Conf.on Software and Computer Applications.2018.322-326.
    [27] Holzmann GJ.The model checker SPIN.IEEE Trans.on Software Engineering, 1997, 23(5):279-298.
    [28] Cimatti A, Clarke E, Giunchiglia F, et al.NUSMV:A new symbolic model checker.Int'l Journal on Software Tools for Technology Transfer, 2000, 2(4):410-425.
    [29] Abdellatif T, Brousmiche KL.Formal verification of smart contracts based on users and blockchain behaviors models.In:Proc.of the 9th IFIP Int'l Conf.on New Technologies, Mobility and Security (NTMS).IEEE, 2018.1-5.
    [30] Kalra S, Goel S, Dhawan M, et al.Zeus:Analyzing safety of smart contracts.In:Proc.of the NDSS.2018.1-12.
    [31] Permenev A, Dimitrov D, Tsankov P, et al.Verx:Safety verification of smart contracts.In:Proc.of the IEEE Symp.on Security and Privacy (SP).2020.1661-1677.
    [32] Shishkin E.Debugging smart contract's business logic using symbolic model checking.Programming and Computer Software, 2019, 45(8):590-599.
    [33] Zhu WJ.PPTL model checking for blockchains.In:Proc.of the 5th IEEE Information Technology and Mechatronics Engineering Conf.(ITOEC).IEEE, 2020.792-795.
    [34] Li SX, Wang GQ, Zhuang L.Reverse real-time model detection method for blockchain smart contract security.Journal of Chinese Computer Systems, 2020, 41(10):2030-2035(in Chinese with English abstract).
    [35] Sun TY, Yu WS.A formal verification framework for security issues of blockchain smart contracts.Electronics, 2020, 9(2):255.
    [36] Ouyang LW, Wang S, Yuan Y, et al.Smart contracts:Architecture and research progresses.Acta Automatica Sinica, 2019, 45(3):445-457(in Chinese with English abstract).
    [37] Wang PW, Yang HT, Meng J, et al.Formal definition for classical smart contracts and reference implementation.Ruan Jian Xue Bao/Journal of Software, 2019, 30(9):2608-2619(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5773.htm[doi:10.13328/j.cnki.jos.005773]
    [38] Bengtsson J, Larsen K, Larsson F, et al.UPPAAL-A tool suite for automatic verification of real-time systems.In:Proc.of the Int'l Hybrid Systems Workshop.Berlin, Heidelberg:Springer, 1995.232-243.
    [39] Larsen KG, Pettersson P, Yi W.UPPAAL in a nutshell.Int'l Journal on Software Tools for Technology Transfer, 1997, 1(1-2):134-152.
    [40] Pnueli A.The temporal logic of programs.In:Proc.of the 18th Annual Symp.on Foundations of Computer Science (SFCS'77).IEEE, 1977.46-57.
    [41] TrackingSystem.2019.https://github.com/Omprakash143/provenance_tracking_SmartContract/tree/master/provenance_tracking_smartContract
    [42] Auction smart contract.2018.https://github.com/astralship/eos/blob/master/contracts/Auction.sol
    [43] TimeLock smart contract.2016.https://github.com/SCBuergel/timeLock-smartContract/blob/master/TimeLock.sol
    [44] Shopping smrt contract.2018.https://github.com/asutosh05/SmartContracts/blob/master/ShoppingApp.sol
    附中文参考文献:
    [1] 贺海武,延安,陈泽华.基于区块链的智能合约技术与应用综述.计算机研究与发展, 2018, 55(11):2452-2466.
    [2] 朱雪阳.The DAO事件的形式化分析.信息技术与网络安全, 2021, 40(5):13-19.
    [3] 周匀.基于承诺的区块链智能合约研究[硕士学位论文].上海:上海交通大学, 2018.
    [5] 刘德林.区块链智能合约技术在金融领域的研发应用现状、问题及建议.海南金融, 2016(10):27-31.
    [6] 赵延红,原宝华,梁军.区块链技术在医疗领域中的应用探讨.中国医学教育技术, 2018, 32(1):1-7.[doi:10.13566/j.cnki.cmet.cn61-1317/g4.201801001]
    [7] 蔡一博.智能合约与私法体系契合问题研究.东方法学, 2019, 68(2):68-81.[doi:10.19404/j.cnki.dffx.20190304.002]
    [8] 赵颖琪,朱雪阳,李广元,高雅,包玉龙.带时间约束的智能合约验证.应用科学学报, 2021, 39(1):1-16.
    [9] 高枫.区块链智能合约漏洞修复困难.计算机与网络, 2018, 44(12):50-51.
    [10] 倪远东,张超,殷婷婷.智能合约安全漏洞研究综述.信息安全学报, 2020, 5(3):78-99.
    [11] 邱欣欣,马兆丰,徐明昆.以太坊智能合约安全漏洞分析及对策.信息安全与通信保密, 2019(2):46-55.
    [34] 李书霞,王国卿,庄雷.区块链智能合约安全的逆向实时模型检测方法.小型微型计算机系统, 2020, 41(10):2030-2035.
    [36] 欧阳丽炜,王帅,袁勇,倪晓春,王飞跃.智能合约:架构及进展.自动化学报, 2019, 45(3):445-457.
    [37] 王璞巍,杨航天,孟佶,陈晋川,杜小勇.面向合同的智能合约的形式化定义及参考实现.软件学报, 2019, 30(9):2608-2619.http://www.jos.org.cn/1000-9825/5773.htm[doi:10.13328/j.cnki.jos.005773]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:1783
  • 下载次数: 4964
  • HTML阅读次数: 4738
  • 引用次数: 0
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第20269777位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号