智能合约的时间约束模式及其形式化验证  

Time Constraint Patterns of Smart Contracts and Their Formal Verification

作　　者：赵颖琪 朱雪阳[1,2] 李广元 包玉龙[1] ZHAO Ying-Qi;ZHU Xue-Yang;LI Guang-Yuan;BAO Yu-Long(State Key Laboratory of Computer Science(Institute of Software,Chinese Academy of Sciences),Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China)

机构地区：[1]计算机科学国家重点实验室(中国科学院软件研究所),北京100190 [2]中国科学院大学,北京100049

出　　处：《软件学报》2022年第8期2875-2895,共21页Journal of Software

基　　金：国家自然科学基金(62072443)。

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

关 键 词：智能合约 时间约束模式 模型检测 SOLIDITY 形式化方法 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]