Study On Modeling And Verification Of Smart Contracts Based On Discrete-time Markov Chain

As an important bridge for the development of blockchain technology from the1.0 era to the 3.0 era,smart contracts have developed rapidly due to the rise of blockchain technology;as one of the most important smart contract application development platforms,the market value of Ethereum has exceeded 200 billion USD,completed more than 1 billion transactions.Ethereum smart contracts not only control a large number of digital assets,but also inherit the immutable properties of the blockchain.Therefore,it is extremely important to ensure that the properties of the Ethereum smart contract.As a classic formal verification method,model checking is used to verify whether a given system model satisfies the property formula to be verified.As a branch of model checking technology,stochastic model checking is used to verify whether the properties of stochastic systems are satisfied.In stochastic model checking,the reliability and performance of the system are often described by discrete-time Markov chains and discrete-time Markov chains with reward structures;the properties of the system are often specified by the probabilistic computation tree logic formulae.Due to the complexity of the operating environment,the smart contract will produce stochastic behaviors during operation,so it belongs to a stochastic system.Based on this,the stochastic model checking technology is used to model and verify the smart contract: by defining the state and transition of the contract,an algorithm for modeling the Ethereum smart contract or contract function as DTMC is proposed;According to the PCTL syntax,a protocol template that regulates the properties of the contract to the PCTL formula is proposed.The specific content of this paper is as follows:(1)Smart contract RDTMC modeling algorithm: By analyzing the trigger conditions of the contract function,the definition of the contract states and transitions,and the assumption of the function trigger probability are given;combined with the relationship between the bytecode of the Ethereum virtual machine and gas consumption,an algorithm for estimating the gas consumption that may be generated when the function is running is given.Finally,an algorithm for modeling smart contracts as RDTMC is given.Through the case studies of online contracts,it is found that by using the RDTMC modeling algorithm,the modeling work of most Ethereum smart contracts can be realized.(2)Contract function DTMC modeling algorithm: the contract function statements is abstracted into state transition according to categories such as loops and selection statements;by adding probabilities to state transition,the modeling of stochastic behaviors is realized;by adding identifiers,comprehensive support for smart contract control statements is realized;refined processing of calling functions;differentiated processing methods for require functions.Through experiments,it is found that the algorithm well supports all control statements of the contract,and the modeling of contract functions is more in line with the function statement logic.(3)Contract properties specification template: In order to more conveniently regulate the properties of the contract,a contract properties specification template is proposed based on PCTL syntax;at the same time,it is proved that the verification of the RDTMC generated by the smart contract satisfies the compositional verification framework.In the experiment,several properties of the modeled contract were stipulated using the protocol template and the verification work was carried out.The verification results strongly prove the validity and correctness of the modeling and specification methods.