Research On Model Checking Method Of Blockchain Smart Contract Security

With the rapid development of blockchain,smart contracts have received widespread attention as the core technology of blockchain.However,the frequent incidents of smart contract vulnerabilities have caused huge economic losses and also plunged smart contracts into a trust crisis.How to ensure the security of the contract has become a problem that needs to be studied urgently.The process of smart contract from demand analysis to code implementation needs to go through rigorous mathematical reasoning verification.The process of smart contract from demand analysis to code implementation needs to go through rigorous mathematical reasoning and verification,and the use of model checking methods can ensure the security of contract requirements;In order to check whether the smart contract source code on Ethereum is safe and reliable when executed,it can also be used to detect security vulnerabilities in reverse with the help of model checking methods.Therefore,this article is based on the model checking method,starting from two different perspectives of contract requirements and contract source code,focusing on the forward and reverse model checking methods of blockchain smart contract security.The main work content is as follows:1)In order to detect loopholes in contract requirements,a forward model checking method for blockchain smart contract security is proposed.Establish a forward analysis framework,and use it as a basis for detailed analysis in combination with role-based access control(RBAC)cases.By analyzing the requirements of the contract case,abstracting the logical roles and operation operators of the contract,deriving the contract roles and the information interaction between the systems,and formalizing them;Introduce model checking technology to build Organization,Thirdparty,Schoolperson,and System models,use sequential logic formulas to express the reliability,functional properties,timeliness and uniqueness of contract cases,and use UPPAAL tools to verify the characterised properties.The verification results show that the use of forward checking methods can detect the security properties that the contract needs meet,and can avoid the emergence of contract code programming loopholes.2)Most of the smart contracts on Ethereum only have the contract source code,and the forward detection method cannot achieve analysis and modeling.Therefore,a reverse model detection method for smart contract security is proposed.Establish a reverse analysis framework,effectively improve detection methods and procedures,and be more suitable for the general situation of smart contracts,and conduct detailed analysis in conjunction with voting contract cases.Through the functional analysis and logical analysis of the source code of the Ethereum smart contract,the contract logic process is extracted;if vulnerabilities such as integer overflow and secondary delegation are found in the contract case,the vulnerabilities should be fixed to formally describe the nature,objects and events;Use timed automata to build Voter,Chairperson,Proposal and Sys models,and verify that the proposed method can effectively detect the security vulnerabilities of the voting contract system through the detection of reliability,integrity,functional attributes,timeliness and uniqueness.