Research And Implementation Of Formal Verification Technology Based On Ethereum Smart Contract

With the booming development of Ethereum,the smart contract is the core of the Ethereum blockchain,and its security has gradually received the attention of the public.However,the gradual enrichment of application scenarios has led to an increase in the amount and complexity of smart contracts.This makes traditional security auditing methods such as testing or manual analysis unable to meet the security requirements of the current smart contract development process.Formal verification is recognized by the public as the most reliable method of security verification based on mathematical theory and is widely used in the software and hardware security field of computers.In this thesis,the theorem proving method in formal verification is used to formally model and verify the contract code of the smart contract from the source code and bytecode respectively,through the formal definition and proof of the program specification of the smart contract to verify the security of smart contracts.Combining the underlying implementation of Ethereum and its technical characteristics,this thesis presents a formal verification method for different verification scenarios of smart contracts,and designs a verification framework for formal verification of Ethereum smart contracts,which can satisfy source code based and word based.Formal verification requirements for two smart contract organization forms of the section code.Through the verification framework,the verification process of smart contracts in two verification modes is described in detail,including formal specification acquisition of smart contracts,formal modeling of intelligent contracts,intelligent contract pending verification theorem and proof of intelligent contract theorem.The realization of formal verification of intelligent contracts mainly involves constructing inference systems about solidity and bytecode in the auxiliary theorem proving tools.The Ethereum operating environment was modeled in the inference system,including computational simulation,state model,solidity grammar model and Ethereum opcode model.The smart contract source code and the compiled bytecode are respectively converted into corresponding models,and after the specified contract module is executed under the preconditions given by the security attribute,the system termination state is obtained,and the relationship between the system and the postcondition is proved,thereby Get the proof of whether the smart contract meets the security attributes.Through the formalization of the security attributes of the smart contract,the verifier can effectively analyze the problem code segment in the positioning contract code from the proof result,thereby accelerating the speed of smart contract iteration and improving the quality and efficiency of industrial production.