Authors: (1) Tianle Sun, Huazhong University of Science and Technology; (2) Ningyu He, Peking University; (3) Jiang Xiao, Huazhong University of Science and Technology; (4) Yinliang Yue, Zhongguancun Laboratory; (5) Xiapu Luo, The Hong Kong Polytechnic University; (6) Haoyu Wang, Huazhong University of Science and Technology. Authors: Authors (1) Tianle Sun, Huazhong University of Science and Technology; (2) Ningyu He, Peking University; (3) Jiang Xiao, Huazhong University of Science and Technology; (4) Yinliang Yue, Zhongguancun Laboratory; (5) Xiapu Luo, The Hong Kong Polytechnic University; (6) Haoyu Wang, Huazhong University of Science and Technology. Table of Links Abstract and 1. Introduction Abstract and 1. Introduction Background 2.1 Ethereum Primer 2.2 Whitelisted Address Verification 2.3 Taint Analysis on Smart Contracts and 2.4 Threat Model Motivating Example and Challenges 3.1 Motivating Example 3.2 Challenges 3.3 Limitations of Existing Tools Design of AVVERIFIER and 4.1 Overview 4.2 Notations 4.3 Component#1: Code Grapher 4.4 Component#2: EVM Simulator 4.5 Component#3: Vulnerability Detector Evaluation 5.1 Experimental Setup & Research Questions 5.2 RQ1: Effectiveness & Efficiency 5.3 RQ2: Characteristics of Real-world Vulnerable Contracts 5.4 RQ3: Real-time Detection Discussion 6.1 Threats to Validity and 6.2 Limitations 6.3 Ethical Consideration Related Work Conclusion, Availability, and References Background 2.1 Ethereum Primer 2.2 Whitelisted Address Verification 2.3 Taint Analysis on Smart Contracts and 2.4 Threat Model Background 2.1 Ethereum Primer 2.1 Ethereum Primer 2.2 Whitelisted Address Verification 2.2 Whitelisted Address Verification 2.3 Taint Analysis on Smart Contracts and 2.4 Threat Model 2.3 Taint Analysis on Smart Contracts and 2.4 Threat Model Motivating Example and Challenges 3.1 Motivating Example 3.2 Challenges 3.3 Limitations of Existing Tools Motivating Example and Challenges 3.1 Motivating Example 3.1 Motivating Example 3.2 Challenges 3.2 Challenges 3.3 Limitations of Existing Tools 3.3 Limitations of Existing Tools Design of AVVERIFIER and 4.1 Overview 4.2 Notations 4.3 Component#1: Code Grapher 4.4 Component#2: EVM Simulator 4.5 Component#3: Vulnerability Detector Design of AVVERIFIER and 4.1 Overview Design of AVVERIFIER and 4.1 Overview 4.2 Notations 4.2 Notations 4.3 Component#1: Code Grapher 4.3 Component#1: Code Grapher 4.4 Component#2: EVM Simulator 4.4 Component#2: EVM Simulator 4.5 Component#3: Vulnerability Detector 4.5 Component#3: Vulnerability Detector Evaluation 5.1 Experimental Setup & Research Questions 5.2 RQ1: Effectiveness & Efficiency 5.3 RQ2: Characteristics of Real-world Vulnerable Contracts 5.4 RQ3: Real-time Detection Evaluation 5.1 Experimental Setup & Research Questions 5.1 Experimental Setup & Research Questions 5.2 RQ1: Effectiveness & Efficiency 5.2 RQ1: Effectiveness & Efficiency 5.3 RQ2: Characteristics of Real-world Vulnerable Contracts 5.3 RQ2: Characteristics of Real-world Vulnerable Contracts 5.4 RQ3: Real-time Detection 5.4 RQ3: Real-time Detection Discussion 6.1 Threats to Validity and 6.2 Limitations 6.3 Ethical Consideration Discussion 6.1 Threats to Validity and 6.2 Limitations 6.1 Threats to Validity and 6.2 Limitations 6.3 Ethical Consideration 6.3 Ethical Consideration Related Work Related Work Related Work Conclusion, Availability, and References Conclusion, Availability, and References Conclusion, Availability, and References Abstract In Ethereum, the practice of verifying the validity of the passed addresses is a common practice, which is a crucial step to ensure the secure execution of smart contracts. Vulnerabilities in the process of address verification can lead to great security issues, and anecdotal evidence has been reported by our community. However, this type of vulnerability has not been well studied. To fill the void, in this paper, we aim to characterize and detect this kind of emerging vulnerability. We design and implement AVVERIFIER, a lightweight taint analyzer based on static EVM opcode simulation. Its three-phase detector can progressively rule out false positives and false negatives based on the intrinsic characteristics. Upon a well-established and unbiased benchmark, AVVERIFIER can improve efficiency 2 to 5 times than the SOTA while maintaining a 94.3% precision and 100% recall. After a largescale evaluation of over 5 million Ethereum smart contracts, we have identified 812 vulnerable smart contracts that were undisclosed by our community before this work, and 348 open-source smart contracts were further verified, whose largest total value locked is over $11.2 billion. We further deploy AVVERIFIER as a real-time detector on Ethereum and Binance Smart Chain, and the results suggest that AVVERIFIER can raise timely warnings once contracts are deployed. 1 Introduction After Satoshi Nakamoto launched Bitcoin [60], blockchain platforms have sprung up. Among them, Ethereum [18] is the most well-known one. Apart from these common characteristics among all blockchain platforms, the most eye-catching feature in Ethereum is the smart contract. It can be taken as a piece of unchangeable script that shall be executed in a determined way once the pre-defined conditions are met. smart contract As billions of USD equivalent assets are stored within smart contracts, identifying and exploiting hidden vulnerabilities in them is the top priority for attackers. According to a recent report [68], there exist around 303 large attack events against well-known Ethereum contracts within the past year, amounting to losses of approximately $3.8 billion. Chen et al. [21] have summarized 26 major types of vulnerabilities in Ethereum smart contracts, and new types of vulnerabilities are still emerging in an endless stream along the constant feature introduction and deprecation in Ethereum [48]. The automatic identification of vulnerabilities in Ethereum smart contracts is a well-studied topic [14, 37, 46, 47, 56, 70, 72, 78]. Considering the number of contracts and the economic loss caused by false negatives, static symbolic execution, which can guarantee soundness to a certain extent, is used as the main analysis method. For example, Mythril [70] is a static bytecode-level symbolic executor for Ethereum contracts, while Slither [31] works on source code, which claims to achieve high efficiency and effectiveness. Verifying the validity of the input addresses is a common practic and a key step to ensure the secure execution of smart contracts. Vulnerabilities in the process of address verification can lead to great security issues, and anecdotal evidence has been reported by our community [11]. To be specific, functions in smart contracts can be addressed as arguments. If developers accidentally neglect the verification on the passed address, once it is taken as the target of an external call, arbitrary operations, including malicious ones, within an address can be invoked. Therefore, if any on-chain state modification relies on that external call, such modification may go against the developer’s wishes. Currently, no existing tools can detect the address verification vulnerability, and implementing such a vulnerability detector based on existing framework is challenging. On the one hand, according to the characteristics of the address verification vulnerability, to effectively identify it, the detector should perform an inter-procedural or even inter-contract analysis. Existing work, however, invariably suffers from either the efficiency or the effectiveness problem when conducting such analyses. For example, a pattern-based detector can barely handle such a complicated vulnerability pattern, while the symbolic execution suffers the path explosion issues and the bottleneck brought from the constraints solving. On the one hand, most contracts are close-sourced, and bytecode lacks sufficient semantics, making it difficult to precisely identify hidden vulnerabilities. Specifically, the address verification vulnerability requires fine-grained tracking in both memory and storage areas. In bytecode, it is hard to distinguish different variables stored in these two areas. Moreover, tracking them via symbolic execution would suffer severe path explosion issue due to the large space of feasible slots. This work. To fill the void, we aim to characterize and detect this kind of emerging vulnerability. To be specific, we design and implement AVVERIFIER, a novel lightweight static taint analysis framework that can efficiently and effectively identify the address verification vulnerability. Its taint analysis relies on the static simulation of the opcode sequence. In other words, without considering the feasibility of paths, AVVERIFIER maintains the values of data structures (e.g., stack and memory) and the taint propagation status. Such a static simulation traverses lots of paths, including the originally infeasible ones. Thus, according to the corresponding states collected, AVVERIFIER formally detects the address verification vulnerability through a three-phase detection. It can progressively rule out false positives and false negatives based on the intrinsic characteristics of the vulnerability. This work. Based on our crafted benchmarks, AVVERIFIER significantly outperforms state-of-the-art smart contract detection tools (i.e., Mythril, Ethainter, Jackal, and ETHBMC)[1] in both terms of efficiency and effectiveness. According to a comprehensive evaluation of over 5 million deployed Ethereum contracts, AVVERIFIER flags over 812 vulnerable contracts, and 348 open-source smart contracts were further verified, whose total value locked is over $11.2 billion. Finally, we deploy AVVERIFIER as a real-time detector on Ethereum and BSC, an EVM-like blockchain platform. The results show that AVVERIFIER is capable of raising early warnings to developers and the community timely. A real-world case, where AVVERIFIER raises the warning 1.5 hours ahead of the attack, proves its effectiveness and efficiency. This paper makes the following contributions: • This is the first work on detecting address verification vulnerability. We have designed and implemented AVVERIFIER, an efficient and effective taint analyzer based on static EVM simulation. • We have applied AVVERIFIER to over 5 million smart contracts on Ethereum, and uncovered hundreds of vulnerable smart contracts which were undisclosed by our community before. This is the first large scale in-the-wild characterization study of this kind of vulnerability. • Compared to Mythril, Ethainter, Jackal, and ETHBMC, AVVERIFIER can improve the analysis efficiency around 2 to 5 times while achieving 94.3% precision and 100% recall on well-established benchmarks. • We have deployed AVVERIFIER as a real-time detector on Ethereum and BSC. The results suggest that AVVERIFIER is able to raise early warnings once contracts are deployed before the attack is initiated by attackers. This paper is available on arxiv under CC BY 4.0 DEED license. This paper is available on arxiv under CC BY 4.0 DEED license. available on arxiv available on arxiv [1] Note that these tools cannot detect address verification vulnerability, we have implemented the same detection logic atop them, for a fair comparison.
