Automated Security Audit Of Smart Contract Based On Symbolic Execution

Ethereum smart contracts are widely used in finance,games,social media and other fields because of their trusted transactions,open source code,and immutability.Despite its unique advantages in trusted transactions,as an emerging technology,smart contract developers generally lack security development capabilities,which leads to the inevitable security vulnerability in smart contracts.The security vulnerabilities in smart contracts may not only affect the normal use of smart contract functions,but also likely cause huge property losses to contract users.Therefore,it is particularly important to perform security analysis on smart contracts.This thesis designs and implements an automated security audit system for three types of smart contract security vulnerabilities that have been paid less attention and are more harmful: arbitrary storage write vulnerabilities,arbitrary destination address jump vulnerabilities,and gas exhaustion denial of service vulnerabilities.The main research contents are as follows:(1)Proposal of automated detection scheme.By analyzing the specific contract instances with vulnerabilities from the code level and the assembly code level,the principle and conditions of the vulnerabilities are summarized,and the corresponding automated detection scheme is proposed.For arbitrary storage write vulnerabilities,it is proposed to detect whether there is a vulnerability in the contract by detecting the possible value range of the "SSTORE" instruction parameter value in the contract execution instruction stream;for arbitrary destination address jump vulnerability,it is proposed to detect whether there is a vulnerability in the contract by detecting the range of the jump instruction destination address in the contract execution instruction stream;for the gas exhaustion denial of service vulnerability,an annotation technique is used to determine whether a loop exists in the contract execution stream.At the same time,check whether the "SSTORE" instruction exists in the loop to detect whether there is a vulnerability in the contract.(2)Implementation of the disassembler.Based on the study of the Ethereum assembly language instructions and the structure of the Ethereum virtual machine,a disassembler was implemented,which can disassemble the smart contract binary code into the Ethereum assembly code,At the same time,it generates the SVM assembly code required by the LASER symbol execution engine for symbol execution.(3)System design and implementation.The basic block information generated by the LASER symbolic execution engine is used to construct the edges between the basic blocks,and at the same time,the control flow graph of the contract code is generated to assist the security analysis of the smart contract.At the same time,the LASER symbolic execution engine is used to implement the proposed smart contract automatic detection scheme and complete an automated security audit system.(4)Testing and analysis.This thesis tested 750 smart contract applications published on the Internet.The test results show that the system implemented in this thesis can effectively support the detection of the above three types of smart contract vulnerabilities,and the accuracy of the vulnerability detection is more than 80%.