Survey and Analysis of Smart Contract Quality Assurance: Defense Methodologies

Table of Links

Abstract and Introduction

Overview of Smart Contracts and Survey Methodology

Vulnerability in Smart Contracts

Attacks on Smart Contracts

Defense Methodologies

Evaluation

Conclusions, Acknowledgement and References

5 DEFENSE METHODOLOGIES

Defense technologies evolve alongside the advancement of attacks, and there is a substantial body of work on security measures for smart contracts [31, 126, 145]. Figure 6 provides an overview of a comprehensive set of research solutions for smart contract defense. Generally speaking, defense strategies for smart contracts can be categorized into two main groups: proactive and reactive. Proactive defense strategies involve taking preventive measures to mitigate attacks before they occur, while reactive defense strategies focus on responding to attacks after they have happened. Proactive defense strategies aim to address known attacks that have been previously identified and studied, with defense mechanisms developed specifically for them. These attacks can be prevented or mitigated using contract analyzers or security enhancements. Reactive defense strategies, on the other hand, pertain to attacks that have not been previously identified or studied, and for which defense mechanisms may not exist. Monitoring contracts play a crucial role in addressing such attacks. However, it is important to note that identifying vulnerabilities and deploying monitoring contracts alone are insufficient for effective smart contract defenses. The repair of vulnerable smart contracts is also a key technology in the defense process [109, 128]. While defene encompasses a broader range of strategies and measures, repair serves as a specific action to fix or address vulnerabilities. The following section provides a detailed description of the defense methodologies involved.

5.1 Contract Analyzer

Contract analyzers play a crucial role in reducing the risk of vulnerabilities in smart contracts before their deployment. Researchers employ various methodologies to analyze smart contracts, many of which are publicly available under open-source licenses. There are five common methodologies for smart contract analysis, such as formal verification, symbolic execution, fuzzing, intermediate representation, and machine learning.

5.1.1 Formal Verification. It is a mathematical-based technique to build and check formal proofs that satisfy a particular property. Formal verification is applied to ensure that software behaves and performs as expected in its specifications and requirements based on large reachable state spaces. Smart contracts are often written in programming languages that are amenable to formal verification [62, 70]. For example, the Solidity programming language used for Ethereum smart contracts has a well-defined syntax and semantics that can be precisely modeled and verified. For smart contracts, we distinguish mainly two families of formal verification methods, namely model checking and theorem proving.

Model checking It lists all possible states and checks them individually to confirm whether the contract has the corresponding characteristic. Compared to other programs, smart contracts have some unique characteristics that make model checking particularly well-suited for vulnerability detection [9, 10, 38, 54]. First, model checking is most effective on systems with a finite number of states, and smart contracts are often small enough to be modeled in their entirety. Second, smart contracts are often designed to be deterministic, which makes it easier to construct formal models to accurately capture their behavior. This technique is relevant to check partial specifications early in the design process [88]. Model checkers, such as SIPN [25], FDR [105], and NuSMV [88], are utilized to successfully verify the correctness and necessary properties of smart contracts [105]. Model checking is typically used to detect specific types of vulnerabilities, such as buffer overflows or integer overflows.

Theorem proving It is a technique that describes the desired properties of a system using mathematical logic and uses a theorem prover to generate proofs that verify these properties based on evidence rules. In the context of smart contracts, theorem proving is used to ensure that a contract satisfies a specific set of properties, such as correctness, safety, or liveness. Since smart contracts are typically deterministic, theorem proving can construct mathematical proofs to demonstrate the satisfaction of these properties. Unlike model checking, which is limited to finite systems, theorem proving can handle the verification of infinite systems. This makes it well-suited for analyzing smart contracts that may involve complex interactions and potential infinite behaviors. Several theorem provers, such as Coq and Isabelle/HOL, have been developed to provide formal semantics and support the theorem-proving process for smart contracts. For instance, Amani et al. extended the existing definition of the Ethereum Virtual Machine (EVM) into Isabelle/HOL with the consideration of gas, allowing for formal verification of EVM-based smart contracts. However, it’s worth noting that formal verification through theorem proving is a semi-automated process that often requires manual interaction. It is commonly used to detect broader classes of vulnerabilities, including logic errors and design flaws, rather than specific instances of vulnerabilities.

5.1.2 Symbolic Execution. It systematically explores more possible execution paths simultaneously to trigger deep program errors. This approach does not require a specified input value but abstracts the input values into symbols. From the vulnerability detection perspective, symbolic execution offers developers specific input to the triggered vulnerability, which can be used to confirm or debug. Symbolic execution has the advantage of achieving high test coverage with as few test cases as possible, thereby digging out deep program errors. Moreover, symbolic execution is often combined with constraint solving to reason whether an execution path is reachable. However, when the program is large and complex, symbolic execution will generate too many paths which may lead to path explosion. A smart contract can be a maximum of 24KB or it will run out of gas [46]. Therefore, symbolic execution is perhaps the most popular approach for smart contracts. Moreover, Z3 SMT solvers are used to check which paths are flexible. Oyente [82] was the first attempt for smart contract verification, using a Control Flow Graph (CFG) representation of the bytecode to identify vulnerabilities like transaction-ordering dependence, timestamp dependence, mishandled exceptions and reentrancy. Other tools, like Manticore and Maian, have extended the capabilities of symbolic execution to detect additional vulnerabilities such as arithmetic overflow/underflow, unsafe suicide, and unchecked send. However, scalability is a concern with symbolic execution, especially in complex application scenarios. The exploration of deep program paths can be slow and resource-intensive. SMARTEST uses symbolic execution to identify vulnerable transaction sequences in smart contracts [116]. By combining symbolic execution with a language model, SMARTEST can effectively prioritize program paths that are likely to reveal vulnerabilities.

5.1.3 Fuzzing. It is a software testing technique that involves executing target programs with a large number of abnormal or random test cases to detect vulnerabilities. It has gained significant attention in both industry and academia [63, 78] due to its simplicity and practical effectiveness in identifying software vulnerabilities. Major software vendors like Google [56] and Microsoft [86] employ fuzzing techniques to uncover vulnerabilities in their products. In the context of smart contracts, fuzzing has been utilized as a means of vulnerability detection, although there are relatively fewer works specifically focused on smart contract fuzzing in recent years. ContractFuzzer [69], for example, uses the Application Binary Interface (ABI) specification of contracts as input for fuzzing to detect vulnerabilities. It relies on user-provided input seeds. Echidna [40], on the other hand, uses falsified user-defined predicates or Solidity assertions as input seeds, which are then subjected to grammar-based fuzzing to detect vulnerabilities. Harvey [137] incorporates a prediction component to generate new input seeds for gray box fuzzing. sFUZZ [89] adopts an adaptive strategy to select input seeds, which are then fed into the prominent fuzzer AFL (American Fuzzy Lop) [39].

However, these methods are more effective in finding shallow bugs and less effective in identifying bugs that lie deep in the execution flow. This limitation is due to the heavy reliance on input seeds in fuzzing. An alternative approach that has shown promising results in traditional programs is hybrid fuzzing, which combines fuzzing with symbolic execution. ILF (Imitation Learning Fuzzer) [63] addresses this limitation by using a symbolic execution expert to generate a large number of training sequences, which are then fed into imitation learning prior to fuzzing. ILF achieves improved coverage and performs well on both large and small contracts. However, ILF is limited to the contracts used for imitation learning in its training phase. ConFuzzius [127], on the other hand, leverages lightweight symbolic execution to analyze execution traces and employs a constraint solver to obtain input seeds for the fuzzer. This approach enhances the effectiveness of fuzzing by incorporating symbolic execution-based analysis. By combining fuzzing with symbolic execution or other complementary techniques, researchers aim to enhance the effectiveness of vulnerability detection in smart contracts, addressing both shallow and deep vulnerabilities.

5.1.4 Intermediate Representation. To accurately analyze smart contracts, some researchers also explore converting contracts into an intermediate representation (IR) with highly semantic information, which is more suitable for the analysis and detection of common security issues. Different from formal verification, IR relies on semantic-based transformation. The analysis process can be divided into four stages: lexical analysis, syntax analysis, semantic analysis, and transformation. The lexical analysis uses Scanner to check whether the input code is a combination of several legitimate words; the syntax analyzer checks whether the combination of these legitimate words meets grammatical rules; semantic analysis checks whether semantics are reasonable; the transformer converts source code or bytecode into machine code, such as XML. Then, the analyzer detects vulnerabilities through specific methods.

Slither [52] transfer contracts to its internal representation language (SlithIR) which uses Static Single Assignment (SSA) form to facilitate the computation of code analyses. EthIR [14] based on Oyente translates CFGs to a rule-based representation (RBR) of the bytecode. Smartcheck [122] directly translates source code into an XML-based IR and then checks it against XPath patterns. MadMax [57] based on the Vandal [28] decompiler translates EVM bytecode to a structured IR to check gas-related Vulnerabilities. NeuCheck [81] employs the Solidity parser ANTLR to complete the transformation from source code to an IR (XML parse tree). VRust [42] successfully translates Rust source code of Solana smart contracts into Mid-level IR.

However, there are two challenges in IR analysis: (1) Because of semantic heterogeneity, it is unavoidable to produce semantic missing during the security analysis; (2) IR takes more processing time.

5.1.5 Machine Learning. It has achieved encouraging results in the field of program security [30, 60, 142]. Compared with the above methods, machine learning combines static analysis and dynamic detection, so as to solve the problems of the high false negative rate of static analysis and low code coverage of dynamic analysis. Moreover, machine learning has good scalability and adaptability for novel vulnerabilities type.

There exist a few prior works that use machine learning methods to analyze smart contracts. Tann et al. [121] introduced a long short-term memory (LSTM) [142] model to handle the semantic representations of smart contract opcode to detect contract security threats. Their model can achieve higher detection accuracy than symbolic execution analyzer Maian [91], where both are based on the same vulnerabilities taxonomy. Qian et al. [104] applied the bidirectional long short-term memory with the attention (BLSTM-ATT) mechanism in their sequential model to reentrancy detection. This framework transforms source code into contract snippets and feeds the sequential model with feature vector representations parsed from these snippets. Zhuang et al. [146] proposed a degree-free graph convolutional neural network (DR-GCN) and a novel temporal message propagation network (TMP) detect vulnerabilities. The source code of a contract is converted to a contracted graph and then to the normalized graphs by a node elimination process. The normalized graphs are fed to DR-GCN and TMP for vulnerability modeling and detection. ContractWard [134] trains its machine learning model on bigram features extracted from the opcodes of the compiled smart contract. SmartMixModel [113] extracts high-level syntactic features from source code as well as low-level bytecode features from the smart contract. And then these features are trained on a machine learning model.

Some researchers also proposed that machine learning will be more efficient if it is in conjunction with fuzzing. SoliAudit [79] employs machine learning to detect known vulnerabilities without expert knowledge or predefined patterns and fuzzing to identify potential weaknesses. However, there is no correlation between the two methods, and fuzzing is more of a complement to machine learning in terms of the detection of vulnerabilities. ILF [63] uses an imitation learning model to learn a fuzzer from training sequences.

5.2 Security Enhancement

Before deployment, some measures can be done to enforce the security of smart contracts. Gas and data are the most important factors for smart contracts. Thus, if gas cost and data privacy have been carefully checked before being deployed, the security of smart contracts will be enhanced. There are some methods for gas cost and data privacy.

5.2.1 Gas Estimation and Optimization. Gas is one of the most important mechanisms in EVM to assign a cost to the execution of an instruction. This mechanism can effectively prevent resource abuse (especially DoS attack) and avoid “infinite" loops [34]. When issuing a transaction, the sender needs to specify a gas limit and a gas price before submitting it to the network. Gas represents much more than just the cost of processing transactions on the Ethereum network. A smart contract is capable of running various applications, allowing it to form a decentralized web. As such, while gas could technically be described as “transaction fees", it should be used with caution. Referring to Section 3, there are several gas-related vulnerabilities. The EVM throws an exception when a transaction run out of gas during its execution, and then EVM will immediately return to the former state.

To prevent this, many Ethereum wallets, such as Metamask [85], can statically estimate the cost of a transaction before it is executed. However, there are many operations that are difficult to estimate during executions. In order to address this problem, some researchers proposed some methods that estimate gas and optimize smart contracts [15, 18, 43]. Albert et al. proposed an automatic gas analyzer Gastap that infers gas upper bounds for all its public functions [15]. Gastap requires complex transformation and analysis of the source code that includes several key techniques: Oyente [82], EthIR [14], Saco [11] and Pubs [12]. Gasol [13], as an extension of Gastap, introduces an automatic optimization of the selected function that reduces inefficient gas consumption. Li et al. [33] developed a GasChecker tool that identifies the gas-inefficient code of smart contracts. They summarized ten gas-inefficient programming patterns that assisted users in better tailoring contracts to avoid gas waste. Gas Gauge [87] can automatically estimate the gas cost for the target function and the loop-bound threshold. Besides, Gas Gauge can find all the loops and furnish the gas-related instances to help developers with suggestions. Li et al. [77] estimated the gas for new transactions by learning the relationship between the historical transaction traces and their gas costs.

5.2.2 Data Privacy-Preserving. In addition to gas concerns, another major concern for the smart contract is private data [73]. Since the openness and transparency of public blockchains, the privacy overlay feature on the chain is absent. This not only leads to some security issues but also prevents their wider adoption. It is problematic for applications that handle sensitive data such as voting schemes [84], electronic medical records[80], or crowdsensing [98].

A promising approach to address private data is to design new blockchain infrastructures supporting private data [75]. Several blockchain infrastructures have been proposed to support private data by adding trust third-party assumptions, such as Hawk [75], Arbitrum [73], Ekiden [35], and Town Crier [139]. Hawk [75] helps programmers write a private smart contract without any specialists and generates an efficient cryptographic protocol for interacting with other parties. Arbitrum [73] helps programmers create a private smart contract by following the specific behavior of a virtual machine (VM) and allows honest parties to advance the VM state on-chain. Both Hawk and Arbitrum rely on trusted managers, which may be instantiated with trusted computing hardware or a multi-party computation among the users themselves. Ekiden [35] processes a smart contract over private data off-chain in trusted execution environments (TEEs) and provides safe interaction among smart contracts on-chain.

An alternative approach is hiding it with cryptographic primitives, such as zero-knowledge proofs. Hawk [75] relies on zero-knowledge proofs to enforce the correctness of contract execution and money conservation on the chain. Steffen et al. [117] proposed zkay contracts containing private data and utilized non-interactive zero-knowledge (NIZK) proof to protect private data. To be more executable on blockchains, zkay contracts are transferred into contracts equivalent in terms of privacy and functionality. Zapper [118] also leverages NIZK proof to correct state updates without revealing private information and an oblivious Merkle tree construction to hide the sender and receiver.

5.3 Runtime Monitoring

The capability to deploy smart contracts is one of the most important features of blockchains. Once deployed on a blockchain, smart contracts become immutable, including any vulnerabilities they may have. While tools are available for scanning smart contracts prior to deployment, they often have limited scopes and may not detect all vulnerabilities, leaving room for unknown runtime attacks. As a solution to enhance the security of post-deployment smart contracts, runtime monitoring techniques analyze and monitor the runtime behavior of smart contracts, providing higher coverage and precision in detecting attacks compared to pre-deployment analysis alone [47]. Runtime monitoring can be categorized into transaction monitoring and state monitoring.

5.3.1 Transactions Monitoring. As Ethereum can be seen as a transaction-based state machine, a transaction contains much information aiming to change the blockchain state. This information also can be used to detect and prevent attacks. ECFChecker [58] examines transactions to determine if they exhibit the characteristics of a reentrancy attack, where a contract can be called recursively before previous invocations have been completed. Sereum [108] aims to prevent reentrancy attacks by employing taint tracking techniques. It tracks the flow of data from storage variables to control-flow decisions, helping identify potential vulnerabilities [32, 66]. Both ECFChecker and Sereum rely on modified versions of Ethereum Virtual Machine (EVM) and primarily focus on detecting reentrancy attacks. In contrast, ÆGIS [124, 125] takes a broader approach by providing an extensible framework for detecting new vulnerabilities in smart contracts. It maintains attack patterns and reverts transactions that match these patterns, thereby enhancing security. The framework allows for the storage and voting of new attack patterns through a smart contract, enabling the community to actively contribute to the detection and prevention of novel attacks. SODA [32] based on a modified EVM-based client provided a platform for developing various applications to detect malicious transactions in real time. SODA has been integrated into popular blockchains that support the EVM, increasing its accessibility and usability. Horus [144] leverages transaction graph-based analysis to identify the flow of stolen assets. By examining the transaction graph, Horus traces the movement of assets and detect potential theft or unauthorized transfers.

5.3.2 State Monitoring. In addition to transactions, blockchain state variables can provide valuable information about the real-time status of a smart contract. Monitoring and analyzing the state variables can be an effective approach to detecting and preventing attacks. Solythesis [76] allows users to instrument user-specified invariants into smart contract code. These invariants represent specific conditions that should always hold true during the execution of the contract. By tracking the transactions that violate these invariants, Solythesis can efficiently enforce powerful monitoring of the contract’s state. This approach helps identify abnormal or unexpected changes in the state variables and allows for proactive detection of potential vulnerabilities. ContractGuard [135] takes a similar approach but introduces the concept of an intrusion detection system (IDS) to monitor the behavior of a deployed smart contract. The IDS continuously monitors the state variables and looks for abnormal or suspicious behaviors that deviate from expected patterns.

5.4 Post-deployment Repair

Ideally, smart contracts should be deployed with the highest possible level of security. However, this presents a challenge not only for smart contracts but also for all software programs. Furthermore, the underlying blockchain technology ensures immutability, meaning that the past cannot be altered. Consequently, updating the code of a deployed contract or addressing vulnerabilities becomes unfeasible. Apart from fixing vulnerabilities, there are numerous other reasons to modify contract code, including adapting business logic or enhancing functionality.

5.4.1 Contract Migration. In many cases, an available approach is to deploy a new instance of the contract and migrate old contract data to it. This approach is called contract migration and has been successfully implemented in various token migration events, such as Augur [24], VeChainThor[133], and TRON [132]. A contract migration process typically involves two steps: data recovery and data writing [72]. During data recovery, the data from the old contract is extracted, including both public and private variables. While retrieving public variables is relatively straightforward, handling private variables and mappings can be more complex. Special measures need to be taken to ensure the integrity and consistency of the migrated data. To address the challenges associated with data migration, some developers employ separate contracts to store and manage the data [95]. This can simplify the migration process by separating the logic from the data storage. By migrating the logic to a new contract and keeping the data in a separate contract, the migration becomes more manageable. It’s important to note that contract migration procedures can be costly, especially for token-based contracts with a large number of accounts [72]. Migrating data for a large number of accounts requires careful planning and execution to avoid potential issues and ensure the accuracy and security of the migrated data.

5.4.2 Upgradable Contracts. Another promising approach to modify smart contracts code is upgradable contract [71, 95, 141]. This approach involves incorporating an upgradability mechanism into smart contracts, allowing for seamless upgrades without the need for data migration or external reference updates. An upgradeable contract can be implemented by setting up a proxy pattern architecture [141]. In this pattern, one contract is split into two separate contracts, one for logic execution and another for data storage. A logic contract stores no state but implements all the business logic; a proxy contract holds all funds and all internal states, but does not implement any business logic. Instead of replacing the entire contract, only the logic contract needs to be modified or replaced. The proxy contract remains intact, and all existing data and external references are maintained. This allows for seamless upgrades without disrupting the contract’s functionality or requiring data migration. Several approaches have been proposed to realize upgradable contracts. Zeppelin [95] proposed three proxy pattern architectures: inherited storage, eternal storage, and unstructured storage. All three patterns rely on the DELEGATECALL instruction, thus these patterns are also called delegate-proxy patterns. For example, EVMPatch [109] uses a proxy pattern to enable the quick and cost-effective upgrade of smart contracts. EVMPatch[109] utilizes the delegate-proxy pattern to enable quick and cost-effective upgrades of smart contracts. It provides a framework for patching vulnerabilities or adding new features to deployed contracts without requiring data migration or disrupting the contract’s functionality.

In this section, we have thoroughly examined and categorized various defense methodologies aimed at preventing or mitigating the damage caused by smart contract attacks. The findings provide a clear and comprehensive response to the third research question, RQ3, as outlined in Section 2.2. However, it is important to acknowledge the existing dearth of empirical evidence that would enable an evaluation of the effectiveness of these methodologies and their associated tools. Despite their claims of superiority, it is imperative for researchers and developers to undertake empirical studies to ascertain which methods are truly practical and beneficial in real-world scenarios.