在现实生活中有一类智能合约与时间紧密相关，而合约是否满足这类时间性质将直接影响应用的正确性。为了避免合约部署后出现严重的问题，将以太坊上的智能合约为研究对象定义智能合约的时间自动机语义，再将智能合约转换为时间自动机模型，接着用模型检测工具UPPAAL检测智能合约是否满足以时序逻辑公式表示的实时性质。最后对竞拍合约以及飞机保险购买合约进行了实例研究，其结果可以展示合约的实时性质是否得以满足。若不满足则可以根据反例定位合约出现的问题点，显示了该工作的有效性。
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.
[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.
