| Since the appearance of Bitcoin in 2008,blockchain technology has attracted widespread attention.Blockchain technology can solve security issues in many areas such as healthcare,finance,and the Internet of Things,including evidence preservation,anti-counterfeiting,privacy protection,decentralized data management,and services.However,blockchain itself also faces many security problems such as consensus mechanism security,supply chain security,and smart contract security.Among the security issues with smart contracts,reentrancy vulnerability exploitation is one of the most destructive attacks that can cause a large amount of fund loss.Based on the analysis of existing smart contract security vulnerability detection work,this article proposes a reentrancy vulnerability detection method based on symbolic execution and designs a reentrancy vulnerability detection tool called Lucifer.The main work of this article includes:Firstly,we propose a method to construct a full control flow graph using the call relationship between public functions among contracts and then use symbolic execution combined with contract state consistency checks on the complete control flow graph for reentrancy vulnerability detection in smart contracts.This method connects the control flow subgraph of public functions that may be called multiple times by external contracts to the control flow graph of the called contract,constructing a complete control flow graph that can simulate reentry attacks.By combining contract state consistency checks,this method achieves reentrancy vulnerability detection for three different types of reentry vulnerabilities:within the same function,across functions,and across contracts.Secondly,based on the above reentrancy vulnerability detection method,we design and implement the detection tool Lucifer.Lucifer simulates the execution of EVM instructions on the complete control flow graph and discovers reentrancy vulnerabilities in the contract based on the consistency check rules of contract states.Lucifer also pays attention to the incorrect use of mutex locks and user-defined function modifiers involved with reentrancy vulnerabilities in smart contracts.The design of Lucifer also uses loop processing and heuristic time optimization algorithms to control branching execution time,uses the SMT solver Yices2 to further improve symbolic execution efficiency,and handles different contract versions for better fault tolerance.Finally,we conduct experiments on a known label dataset,a vulnerability injection dataset,a custom classification dataset,and a real dataset of Ethereum smart contracts.The reentrancy vulnerability detection tool Lucifer designed in this article is compared with four other popular reentrancy vulnerability detection tools.The experimental results show that Lucifer outperforms other reentrancy vulnerability detection tools in terms of false positive rate,false negative rate,and fault tolerance. |