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

Study on Modeling and Verification of Functions of Smart Contracts

作　　者：叶昊榀 刘阳 YE Hao-pin;LIU Yang(College of Information Engineering,Nanjing University of Finance&Economics,Nanjing Jiangsu 210023,China)

机构地区：[1]南京财经大学信息工程学院,江苏南京210023

出　　处：《计算机仿真》2021年第3期201-205,共5页Computer Simulation

基　　金：江苏省“六大人才高峰”高层次人才(RJFW-014);江苏省高等学校自然科学研究重大项目(17KJA520002)。

摘　　要：针对智能合约对安全性方面的相关性质的极高要求,有必要改进已有的建模算法,提出将智能合约函数的函数体语句建模为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.

关 键 词：智能合约 形式化方法 离散时间马尔可夫链 概率计算树逻辑 随机模型检验 

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