Formal Smart Contract Verification Based On Word-level Model Checking

With the rapid development of the Ethereum blockchain,smart contracts have become the core of digital asset management and trading,managing enormous assets.However,the decentralized and transparent nature of smart contracts makes them a target for attackers.Smart contract vulnerabilities are constantly exploited by attackers,resulting in billions of dollars in asset losses for the Ethereum network.Therefore,conducting formal verification of smart contracts is essential.Formal verification is a technique that uses mathematical methods to prove that a program complies with a set of rules and specifications,ensuring the correctness of the program.Applying formal verification techniques to smart contracts can detect vulnerabilities in smart contracts,ensuring their security.Currently,the formal verification of smart contracts can be divided into two parts.The first part is to verify the correctness of specific smart contract transactions,that is,to verify whether the code of a single smart contract is correct.The second part is to verify the correctness of the contract supply chain,that is,to verify whether the interaction process between the entire contract and the client is correct.This article mainly focuses on the verification of specific smart contract transactions to ensure the security of smart contracts.This article first proposes a set of rules for transforming the smart contract language Solidity into the verification language Btor2.Since the semantics of the two languages are different,it is necessary to establish a set of conversion rules to achieve the transformation from Solidity to Btor2.These conversion rules cover the translation of control structures,data types,and functions in the Solidity language into their corresponding structures in the Btor2 language,to ensure that the resulting model code can be properly verified.Secondly,This article applies model checking technology to smart contracts,models the transaction process of smart contracts,and implements verification model code.Based on the specific analysis of Solidity smart contract transaction process and contract security vulnerabilities on the Ethereum network,a smart contract verification model was built and the properties that needed to be verified were abstracted.Then,based on the Solidity and Btor2 conversion rules,extracted properties,and established models,the verification code was implemented to verify the security of smart contracts.Finally,this article validates the model under examination using the model checking tool AVR.AVR conducts formal verification of the extracted properties from security vulnerabilities of smart contracts to determine whether the model is secure.By analyzing the verification results,the presence of security vulnerabilities in the Solidity smart contract transaction process can be checked,thereby verifying the security of the smart contract.