带时间约束的智能合约验证

doi:10.3969/j.issn.0255-8297.2021.01.001

Abstract

Abstract: In real life, a type of smart contract is closely related to time constraint, and whether the contract meets its time property will directly affect the correctness of its applications. In order to avoid serious problems after its deployment, this paper focuses on smart contracts of Ethereum, gives a timed automata semantics for smart contracts, after the smart contract is converted into a time automata model, and uses model checking tool UPPAAL to check whether the smart contract meets timed properties expressed by temporal logic formulas. Finally, we study two cases, an auction contract and a flight insurance contract. Experimental results indicate whether the real-time property is satisfied. If not, counter examples can be used to locate the problem points in the smart contract, showing the effectiveness of the work.

Key words: blockchain, smart contract, Solidity, time constraint, model checking

CLC Number:

TP311

ZHAO Yingqi, ZHU Xueyang, LI Guangyuan, GAO Ya, BAO Yulong. Verification of Smart Contracts with Time Constraints[J]. Journal of Applied Sciences, 2021, 39(1): 1-16.

References

[1] 贺海武, 延安, 陈泽华. 基于区块链的智能合约技术与应用综述[J]. 计算机研究与发展, 2018, 55(11):2452-2466. He H W, Yan A, Chen Z H. Survey of smart contract technology and application based on blockchain[J]. Journal of Computer Research and Development, 2018, 55(11):2452-2466. (in Chinese)
[2] Szabo N. Smart contracts in essays on smart contracts, commercial controls and security[EB/OL]. 1994[2020-09-25]. http://www.fon.hum.uva.nl/rob/Courses/InformationInSpeech/CDROM/Literature/LOTwinterschool2006/szabo.best.vwh.net/smart.contracts.html.
[3] Buterin V. A next-generation smart contract and decentralized application platform[EB/OL]. 2014[2020-09-26]. https://www.zybuluo.com/Gebitang/note/1039458.
[4] 邱欣欣, 马兆丰, 徐明昆. 以太坊智能合约安全漏洞分析及对策[J]. 信息安全与通信保密, 2019(2):44-53. Qiu X X, Ma Z F, Xu M K. Ethereum smart contract security vulnerability scenario analysis[J]. Information Security and Communications Privacy, 2019(2):44-53. (in Chinese).
[5] 赵延红, 原宝华, 梁军. 区块链技术在医疗领域中的应用探讨[J]. 中国医学教育技术, 2018, 32(1):1-7. Zhao Y H, Yuan B H, Liang J. Application of blockchain technology in medical field[J]. China Medical Education Technology, 2018, 32(1):1-7. (in Chinese)
[6] 何源源. 数字版权保护中的区块链智能合约法律规制研究[D]. 开封:河南大学, 2019:1-35.
[7] DuPont Q. Experiments in algorithmic governance:a history and ethnography of "The DAO", a failed decentralized autonomous organization[M]. Bitcoin and Beyond, 2017:157-177.
[8] Bai X, Cheng Z, Duan Z, et al. Formal modeling and verification of smart contracts[C]//Proceedings of 20187th International Conference on Software and Computer Applications, 2018:322-326.
[9] Alt L, Reitwießner C. SMT-based verification of solidity smart contracts[C]//International Symposium on Leveraging Applications of Formal Methods. Cham:Springer, 2018:376-388.
[10] 王璞巍, 杨航天, 孟佶, 等. 面向合同的智能合约的形式化定义及参考实现[J]. 软件学报, 2019, 30(9):2608-2619. Wang P W, Yang H T, Meng J, et al. Formal definition for classical smart contracts and reference implementation[J]. Journal of Software, 2019, 30(9):2608-2619. (in Chinese).
[11] Solidity-the official documentation of Solidity 0.7.0 documentation[EB/OL]. 2019[2020-9-25]. https://solidity.readthedocs.io/en/v0.7.1/.
[12] Bengtsson J, Larsen K, Larsson F, et al. UPPAAL-a tool suite for automatic verification of real-time systems[C]//International Hybrid Systems Workshop. Berlin, Heidelberg:Springer, 1995:232-243.
[13] 郭华, 庄雷, 张习勇. UPPAAL——一种适合自动验证实时系统的工具[J]. 微计算机信息, 2006(5X):52-54. Guo H, Zhuang L, Zhang X Y. UPPAAL-a tool suit for automatic verification of real-time systems[J]. Control & Automation, 2006(5X):52-54. (in Chinese).
[14] 欧阳丽炜, 王帅, 袁勇, 等. 智能合约:架构及进展[J]. 自动化学报, 2019, 45(3):445-457. Ouyang L W, Wang S, Yuan Y, et al. Smart contracts:architecture and research progresses[J]. Acta Automatica Sinica, 2019, 45(3):445-457. (in Chinese).
[15] Liu J, Liu Z. A survey on security verification of blockchain smart contracts[J]. IEEE Access, 2019, 7:77894-77904.
[16] 倪远东, 张超, 殷婷婷. 智能合约安全漏洞研究综述[J]. 信息安全学报, 2020, 5(3):78-99. Ni Y D, Zhang C, Yin T T. A survey of smart contract vulnerability research[J]. Journal of Cyber Security, 2020, 5(3):78-99. (in Chinese).
[17] Dannen C. Introducing Ethereum and Solidity[M]. Berkeley:Apress, 2017:69-88.
[18] Luu L, Chu D H, Olickel H, et al. Making smart contracts smarter[C]//Proceedings of 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016:254-269.
[19] 陈伟, 薛云志, 赵琛, 等. 一种基于时间自动机的实时系统测试方法[J]. 软件学报, 2007, 18(1):62-73. Chen W, Xue Y Z, Zhao C, et al. A method for testing real-time system based on timed automata[J]. Journal of Software, 2007, 18(1):62-73. (in Chinese)
[20] 李力行, 金芝, 李戈. 基于时间自动机的物联网服务建模和验证[J]. 计算机学报, 2011, 34(8):1365-1377. Li L X, Jin Z, Li G. Modeling and verifying services of Internet of things based on timed automata[J]. Chinese Journal of Computers, 2011, 34(8):1365-1377. (in Chinese).
[21] Bengtsson J, Yi W. Timed automata:semantics, algorithms and tools[C]//Advanced Course on Petri Nets. Berlin, Heidelberg:Springer, 2003:87-124.
[22] Zhu X Y, Yan R, Gu Y L, et al. Static optimal scheduling for synchronous data flow graphs with model checking[C]//International Symposium on Formal Methods. Cham:Springer, 2015:551-569.
[23] Pnueli A. The temporal logic of programs[C]//The 18th Annual Symposium on Foundations of Computer Science, IEEE, 1977:46-57.
[24] Novy D. Python-solidity-parser[EB/OL]. 2019[2020-07-15]. https://github.com/ConsenSys/python-solidity-parser.
[25] Zuo H B. The example of auction[EB/OL]. 2019[2020-08-03]. https://soliditycn.readthedocs.io/zh/develop/solidity-by-example.html.
[26] Stewart-Frantz K. FlightSurety-DApp[EB/OL]. 2019[2020-09-12]. https://github.com/jeroat-github/FlightSurety-DApp/tree/master/contracts.

Verification of Smart Contracts with Time Constraints

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments

[1]	FANG Junjie, LEI Kai. Blockchain for Edge AI Computing: A Survey [J]. Journal of Applied Sciences, 2020, 38(1): 1-21.
[2]	HE Zhengyuan, DUAN Tiantian, ZHANG Ying, ZHANG Hanwen, SUN Yi. Blockchain in Internet of Things: Application and Challenges [J]. Journal of Applied Sciences, 2020, 38(1): 22-33.
[3]	BAO Zhenshan, WANG Kaixuan, ZHANG Wenbo. A Practical Byzantine Fault Tolerance Consensus Algorithm Based on Tree Topological Network [J]. Journal of Applied Sciences, 2020, 38(1): 34-50.
[4]	LI Zhongcheng, HUANG Jianhua, TANG Ruicong, HU Qingchun, XIA Xu. A Scalable Consensus Protocol Based on Equity Representation [J]. Journal of Applied Sciences, 2020, 38(1): 51-64.
[5]	ZOU Xiuqing, LUO Decun, LIN Ping, SHEN Shiping, XIE Zhenping, WANG Yujue, DING Yong. System of River Chief-Oriented Water Quality Information Certification Based on Blockchain [J]. Journal of Applied Sciences, 2020, 38(1): 65-80.
[6]	YUAN Chenjuan, SUN Guozi, LI Huakang, WANG Jitao. Credible Depository Chain System of Card Games [J]. Journal of Applied Sciences, 2020, 38(1): 81-92.
[7]	JIANG Yunchao, HE Xiaowei, CUI Yiju. Blockchain Node Storage Optimization Scheme [J]. Journal of Applied Sciences, 2020, 38(1): 119-126.
[8]	PAN Heng, PAN Lei, YAO Zhongyuan, SI Xueming. A Patient-Controlled Security Access Mechanism for Electronic Health Records [J]. Journal of Applied Sciences, 2020, 38(1): 127-138.
[9]	SHE Wei, CHEN Jiansen, GU Zhihao, TIAN Zhao, XU Li, LIU Wei. Location Information Protection Model for IoT Nodes Based on Blockchain [J]. Journal of Applied Sciences, 2020, 38(1): 139-151.
[10]	LEI Kai, HUANG Shuokang, FANG Junjie, HUANG Jiyue, XIE Yingying, PENG Bo. Intelligent Eco Networking (IEN): Knowledge-Driven and Value-Oriented Future Internet Infrastructure [J]. Journal of Applied Sciences, 2020, 38(1): 152-172.
[11]	ZHANG Lihua, HU Fangzhou, HUANG Yang, WAN Yuanhua, LI Jingjing. Identity Authentication Protocol of Micro-grid Power Based on Consortium Blockchain [J]. Journal of Applied Sciences, 2020, 38(1): 173-183.
[12]	ZHANG Yifei, CAO Shaozhong, QI Deli, WANG Liang, YANG Yanhong. Book Infringement Record Depositing Platform Based on Blockchain [J]. Journal of Applied Sciences, 2020, 38(1): 184-196.
[13]	REN Peng, XU Jingjing, WANG Yi, MA Xiaofeng. Research and Implementation of Car Rental Alliance Based on Blockchain and Internet of Vehicles [J]. Journal of Applied Sciences, 2019, 37(6): 851-858.
[14]	FAN Xian-li, FAN Chun-xiao, WU Yue-xin. Realization of Privacy Protection of Food Supply Chain Based on Blockchain and IPFS [J]. Journal of Applied Sciences, 2019, 37(2): 179-190.
[15]	LI Bo, ZHENG Bo, GUO Zi-yang, WANG Hong-zhi. The State-of-the-Art Blockchain Applications in Finance: Progress and Trends [J]. Journal of Applied Sciences, 2019, 37(2): 151-163.