Smart Contract Vulnerability Detection Based On Symbolic Execution

The blockchain 2.0 platform represented by Ethereum has developed rapidly in recent years,compared with the blockchain 1.0,one of the main breakthroughs of Ethereum is the realization of smart contract programming,which changes the role of the blockchain from the original distributed ledger to decentralized applications.Smart contracts based on blockchain are generally programmed by Turing-complete language,which has the natural advantages of decentralization and trusted transaction.Different from the standard software application,the smart contract cannot be updated once it was deployed on the blockchain.The deployment of vulnerable smart contract on the blockchain can cause unpredictable consequences,and can even seriously damage the blockchain ecosystem.Therefore,a strict code review mechanism is required before the smart contract code is deployed.Although the academia and industry have already developed some vulnerability detection tools for smart contracts,due to the short development history of smart contracts,some tools still have the disadvantages including rough detection,low accuracy and low efficiency.At the same time,with the increasing on smart contracts,some security audit tools consume huge system resource in detection.Symbolic execution is one of the important measures for smart contract vulnerability detection.Tools based on symbolic execution have the problems on state space explosion and accuracy conservation of detection model.This paper focuses on these problems.The main work and contributions are as follows:(1)In this paper,to improve the efficiency of vulnerability detection,we propose a method of optimizing symbolic execution to search state space,which is based on pile insertion of static analysis results.Focusing on the problem that a single search algorithm of the symbolic execution engine cannot cover the vulnerable code area effectively,we insert piles for sensitive code blocks by static analysis so as to obtain higher priority for detection.Static analysis has added unequal weights to the code block entry point of the program control flow graph based on the potential danger of instructions determination.With the weighted results,the symbolic execution engine searches the candidate state space,which is based on a hybrid state search algorithm,so the basic code block with dangerous instruction can be located more efficiently,so as to increase the detection efficiency.(2)To improve the detection accuracy,a novel loop structure recognition algorithm without source code is proposed.Aiming at the potential state space explosion caused by the symbolic execution engine under complex structure procession,we recognized the count of loop structures based on forward matching principle of control flow graph,and we used loop detection to prevent the symbol execution engine from running deep into the source code and generating large copies of state spaces.In this way,we prevent the detection system from abnormal termination due to the huge state space when facing the loop structure.Finally,the false negative and precision of the smart contract detection system can be reduced.(3)We designed a symbolic execution detection system for smart contract vulnerabilities,which based on the open-source framework Mythril,to verify the algorithm improvement scheme proposed in this paper.The experimental results show that,our smart contract vulnerability detection system performs well against the following vulnerabilities: reentrancy vulnerabilities and integer overflow vulnerabilities,bad randomness vulnerabilities and access control vulnerabilities,transaction order dependency vulnerabilities.Based on the detection results of the real smart contracts of Ethereum,the detection accuracy rate of our system has increased,and the execution efficiency has improved by 1.61 times,compared with the existing symbolic execution tools Mythril and Oyente.