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 4 Design of AVVERIFIER This section elucidates the technical intricacies of AVVERIFIER, which is designed to detect the address verification vulnerability in Ethereum smart contracts. We firstly give a high-level overview in §4.1, and an introduction of adopted notations in §4.2. Then, we delve into the three components, respectively, from §4.3 to §4.5. 4.1 Overview Fig. 1 illustrates the architecture and workflow of AVVERIFIER, which is composed of three main components, i.e., code grapher (denoted as Grapher), EVM simulator (denoted as Simulator), and vulnerability detector (denoted as Detector). Specifically, AVVERIFIER only takes the bytecode of a Solidity smart contract as input. The Grapher parses it into the control flow graph (CFG), filters out all suspicious functions as candidates, and delivers them to the Simulator. The Simulator maintains a state, consisting of two parts. One part is the data structures required by EVM, i.e., stack, memory, and storage (see §2.1); the other part is the collected taint information. According to the CFG, the Simulator updates fields in states according to the opcode sequence. It also adopts a heuristicbased path selection method to focus on the most valuable path, i.e., the ones that may lead to the vulnerability. Once the analysis against a path is finished, the corresponding state is sent to the Detector to determine if the current contract is vulnerable to the address verification vulnerability. The cascaded three-phase detection strategy in the Detector rules out false positives and false negatives based on the intrinsic characteristics (P1 to P3). code grapher EVM simulator vulnerability detector 4.2 Notations To better explain the implementation of AVVERIFIER, we define some notations here: • S, the set of sources that can be controlled by users; S • T, the set of tainted variables; T • CT, a mapping from a tainted variable to its sources; • CT • F, the set of suspicious functions; • F • Mem, Sto, refer to the memory and storage area in EVM. Mem Sto • V, EC, and SM, refer to the three-stage detection in the Detector, respectively. Each of them takes a function f and a parameter p as inputs. V EC SM f p 4.3 Component#1: Code Grapher Generally speaking, the Grapher is responsible for obtaining the sub-tree of CFG of the given function. Given a piece of bytecode, Grapher firstly extracts the runtime code, consisting of implementation of functions [40]. Then, Grapher parses it into basic blocks and constructs the CFG according to their jump relations. However, some jump relations are determined dynamically at runtime instead of statically at the compilation stage. Thus, the Grapher constructs the CFG only on statically determined jump relations considering the soundness. Take the Fig. 2 as an example, where bb1 is the entry of the function foo and its jump relations to bb2 and bb3 can be statically determined. Though bb3 and bb4 can jump to bb5 at runtime, they are determined dynamically. Thus, though the Grapher generates two trees whose roots are bb1 and bb5, respectively, bb5 is actually a subtree of bb1 at runtime. To filter out suspicious functions, i.e., the ones that may be vulnerable to the address verification vulnerability, the Grapher heuristically keeps functions that take addresses as arguments (P1). Specifically, each address parameter undergoes a bitwise AND operation with 0xFF..FF (160-bit long). By identifying such a specific pattern, which is also widely adopted in previous work [7], we can extract functions that meet P1. These functions will be added to the set F . 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. 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
