智能合约函数的建模与验证研究

Study on Modeling and Verification of Functions of Smart Contracts

针对智能合约对安全性方面的相关性质的极高要求,有必要改进已有的建模算法,提出将智能合约函数的函数体语句建模为DTMC的算法,并对生成的DTMC进行验证。通过为状态迁移添加概率,实现了对随机现象的关注。通过对调用函数的分类处理,精细化了对函数调用函数情况的处理。通过添加标识符,实现了对智能合约所有控制语句的支持。对常被用于判定函数是否可以被触发的require语句,提供了差异化的处理方式从而改善算法的处理能力。同时对智能合约应保障的部分性质进行规约以验证模型效果。实验结果表明,建模方法可以实现对智能合约所有控制结构语句建模的支持,能够实现对合约函数的建模并完成验证。

Because of the extremely high requirements of the security and other correlative properties of smart contracts,it is necessary to improve the existing modeling algorithms,propose an algorithm to model the statements of the functions of smart contracts as DTMC,and verify the generated DTMC.At first,the random phenomena should be paid attention to through adding probabilities to state transition.Secondly,the handling of function calling functions was refined through classifying the called functions.Thirdly,all the control statements of smart contracts can be supported through adding identifiers.Finally,the differentiated processing method was proposed to determine whether the function can be triggered by the require statement,which can improve the processing capacity of the algorithm.Meanwhile,partial properties of smart contracts were regulated for verification.The experimental results show that the modeling method can provide supports to model all the control structures of smart contracts and help to completely verify the feasibility and effectiveness of the modeling of contract function.