Research On Formal Verification For Ethereum Token Smart Contracts

With the development of Ethereum blockchain,smart contract,the core technol-ogy of Ethereum,has been increasingly used in different application scenarios.One of the application scenarios is the token smart contract used to create new tokens.In addi-tion to Ether,Ethereum allows users to create and manage their own tokens using token smart contracts.Token smart contracts hold a large amount of funds and are vulnerable to attack by attackers.Token smart contracts have been discovered various of types of vulnerabilities,and security problems of token smart contracts have resulted in serious losses.Therefore,it is urgently important and necessary to ensure the the security of to-ken smart contracts.Formal verification is an automated method proposed specifically for security analysis,which is the highest security level and can more comprehensively and deeply analyze the security of contracts.In order to solve the above problems,this dissertation focuses on the formal mod-eling and verification of token smart contracts.The formalized model of token smart contracts is proposed with the most popular ERC20 token standard,and applied to the formal analysis of high-risk vulnerabilities.The main work carried out is as follows:1.Aiming at the requirement of formal modeling of token smart contracts,the formalized model of ERC20 token smart contract is proposed.The specific behaviors of the functions and the abstract structure of the attackers are described.The model rules are defined by multi-set rewriting rules.The formal security attributes of token smart contracts based on ERC20 token standard are proposed,including basic attributes,transaction attributes and permission attributes.The model has practical significance for analyzing the security of ERC20 token smart contracts.2.In order to verify and analyze the high-risk vulnerabilities that caused a lot of losses of token smart contracts,this dissertation focuses on the formal modeling and verification of integer overflow vulnerability.The modeling difficulty of integer over-flow vulnerability is analyzed and solved.Based on the above formal model of token smart contract and the analysis of the attack principle of integer overflow vulnerability,the formal modeling of integer overflow vulnerability is completed.Furthermore,the corresponding improvement measures are put forward.The SmartVerif tool is used to verify the contract instances,including contracts with integer overflow vulnerability and improved contract instances.The experiment results show that the security attributes are feasible and the improvement measures can avoid the attacks in the original contracts.3.In order to verify and analyze the vulnerabilities of token smart contracts with high-risk threat,this dissertation proposes to analyze reentrancy vulnerability and give the formal analysis method of reentrancy vulnerability.Based on the aforementioned token smart contract modeling model,the security attributes and modeling methods are analyzed.The modeling difficulty of reentrancy vulnerability is analyzed and solved.The experimental results show that the contract instances with reentrancy vulnerability are verified,and further proposed corresponding improvement measures for the hid-den dangers of reentrancy vulnerabilities are put forward.The results show that the improvement measures can avoid the attacks.