PaperlayerView exact revision on arXiv

Source-linked AI summary

Security Analysis Methods on Ethereum Smart Contract Vulnerabilities: A Survey

Purathani Praitheeshan, Lei Pan, Jiangshan Yu, Joseph Liu, Robin Doss

arXiv:1908.08605v3cs.CR

TL;DR

This survey examines Ethereum smart-contract vulnerabilities that have caused severe attacks and cryptocurrency losses. It identifies 16 vulnerabilities, relates them to software-security issues, and compares static, dynamic, and formal analysis methods, while highlighting unresolved vulnerabilities and tool limitations.

  • Problem

    Ethereum smart contracts hold cryptocurrency in critical applications, yet technical flaws have enabled severe attacks and some vulnerabilities lack proper solutions.

  • Method

    The survey identifies 16 Ethereum smart-contract vulnerabilities, correlates them with 19 software-security issues, and categorizes detection methods as static analysis, dynamic analysis, and formal verification.

  • Results

    The survey presents vulnerabilities, available analysis tools, detection methods, and comparisons of static, dynamic, and formal approaches across performance, coverage, and accuracy.

  • Takeaways & Limitations

    Developers and users should consider the accuracy and performance of smart-contract analysis methods when assessing security.

  • Takeaways & Limitations

    Formal-verification methods are often only partially automated, and their initial setup takes more time than symbolic-execution tools.

Abstract

from arXiv · show

Smart contracts are software programs featuring both traditional applications and distributed data storage on blockchains. Ethereum is a prominent blockchain platform with the support of smart contracts. The smart contracts act as autonomous agents in critical decentralized applications and hold a significant amount of cryptocurrency to perform trusted transactions and agreements. Millions of dollars as part of the assets held by the smart contracts were stolen or frozen through the notorious attacks just between 2016 and 2018, such as the DAO attack, Parity Multi-Sig Wallet attack, and the integer underflow/overflow attacks. These attacks were caused by a combination of technical flaws in designing and implementing software codes. However, many more vulnerabilities of less severity are to be discovered because of the scripting natures of the Solidity language and the non-updateable feature of blockchains. Hence, we surveyed 16 security vulnerabilities in smart contract programs, and some vulnerabilities do not have a proper solution. This survey aims to identify the key vulnerabilities in smart contracts on Ethereum in the perspectives of their internal mechanisms and software security vulnerabilities. By correlating 16 Ethereum vulnerabilities and 19 software security issues, we predict that many attacks are yet to be exploited. And we have explored many software tools to detect the security vulnerabilities of smart contracts in terms of static analysis, dynamic analysis, and formal verification. This survey presents the security problems in smart contracts together with the available analysis tools and the detection methods. We also investigated the limitations of the tools or analysis methods with respect to the identified security vulnerabilities of the smart contracts.

I. INTRODUCTION

This survey examines Ethereum smart-contract vulnerabilities, their relationship to software-security issues, and methods for detecting them. It organizes prior work around attacks, vulnerability analysis, and static, dynamic, and formal-verification approaches.

  • Motivation: Ethereum smart contracts support decentralized transactions but remain difficult to secure because Solidity is immature, best practices are limited, and deployed code cannot be patched conventionally.Errors detected after deployment generally require terminating the erroneous contract before deploying an updated one.
  • Research Questions: The survey asks which major Ethereum attacks caused substantial crypto-asset losses, how vulnerabilities are exploited, and which analysis methods validate smart-contract security.
  • Scope and Novelty: Unlike broader surveys, this paper specifically analyzes vulnerability-detection methods for Ethereum smart contracts in the context of identified security attacks.
  • Contributions: The survey identifies security problems and vulnerabilities associated with severe attacks and significant cryptocurrency losses.
  • Contributions: It categorizes security analysis methods into static analysis, dynamic analysis, and formal verification.
  • Contributions: The survey compares analysis methods by their applications, vulnerability findings, and coverage, drawing on about 125 papers selected from high-quality journals, transactions, and conferences.

II. BACKGROUND INFORMATION

Ethereum provides a distributed platform where accounts and smart contracts execute code under consensus rules. Smart contracts can act as trusted intermediaries for transactions, but their stored value and permissionless execution create security risks.

  • Ethereum Platform: Ethereum is a blockchain-based platform whose Ethereum Virtual Machine executes smart contracts across a distributed network of permissionless peers.
  • Ethereum Accounts: Ethereum accounts are either externally owned accounts controlled by private keys or contract accounts controlled by compiled programming code.
  • Ethereum Accounts: Each account contains an address, Ether balance, data storage, and nonce, with the nonce ensuring that each transaction is executed only once.
  • Smart Contracts: Smart contracts are Solidity programs compiled into EVM bytecode that can implement applications including cryptocurrency management, wallets, and autonomous governance.
  • Smart Contracts: In the example transaction, a buyer deposits Ether into the contract, the seller verifies and fulfills the request, delivery status is updated, and the contract releases the Ether.
  • Security Context: Because smart contracts can hold substantial virtual-currency value and operate on distributed, permissionless networks, adversaries attempt to manipulate their execution.

A. The DAO Attack

The DAO attack exploited re-entrancy in a withdrawal function, recursively draining more than 3.6 million Ethers before the contract balance reached zero. The incident reflected a programming error involving external calls and delayed balance updates, while blockchain immutability complicated remediation.

  • Attack mechanism: More than 3.6 million Ethers were stolen in the June 2016 DAO hack through a re-entrancy vulnerability.The attacker repeatedly invoked the vulnerable DAO.sol withdrawal function.
  • Attack mechanism: The attacker embedded withdraw in a fallback function, causing recursive calls before the user’s balance was updated.Receiving funds automatically triggered the fallback function and another withdrawal.
  • Vulnerability: The DAO contract used call to transfer funds, while the balance update occurred afterward, leaving an exploitable intermediate state.The delayed state update enabled repeated withdrawals before the balance was corrected.
  • Vulnerability: The attack was attributed to a smart contract programming error rather than an Ethereum network defect.The survey states that any network with the same erroneous contract could facilitate the re-entrancy hack.
  • Remediation: The hard fork reversed transaction history to refund victims, but the old branch continued as Ethereum Classic.Blockchain immutability and deterministic execution made sudden attack resolution difficult.

B. Parity Multi-Sig Wallet Attack

The Parity multi-signature wallet attack exploited publicly callable initialization functions in an external library invoked through delegatecall. Attackers claimed wallet ownership and withdrew funds, while blockchain non-updatability left affected libraries and contracts exposed.

  • Wallet design: Parity multi-signature wallets store ownership, withdrawal limits, and voting information while requiring multiple signatures for withdrawals.The signature requirement was intended to strengthen wallet security.
  • Attack mechanism: Attackers first claimed wallet ownership and then withdrew all available funds through the wallet library’s initialization logic.The publicly callable initWallet function accepted owners, required signatures, and day-limit parameters.
  • Vulnerability: The library’s public initialization functions lacked access modifiers, allowing unauthorized callers to invoke them through delegatecall.Functions such as initDayLimit and initMultiowned were callable by anyone.
  • Vulnerability: The attack involved improper file access and information leakage issues caused by unrestricted calls to an external library.The survey links the vulnerability to weak library access control and non-restricted invocations.
  • Remediation: Blockchain non-updatability enabled attackers to continue targeting problematic libraries and smart contracts after deployment.The affected library’s reusable abstraction also exposed its functions to unauthorized delegatecalls.

C. Integer Overflow/Underflow Attack

The integer overflow/underflow attack exploited Solidity’s fixed-size unsigned integers to reset balances after arithmetic exceeded their valid range. In the POWH Coin attack, repeated withdrawals drained around 2,000 Ethers, while SafeMath was identified as a mitigation.

  • Vulnerability: A uint256 is limited to 256 bits, and values outside its range reset rather than producing a safe arithmetic error.The survey describes wraparound behavior for values exceeding or falling below the permitted range.
  • Attack mechanism: An attacker could withdraw 1 Wei from a zero balance, trigger a fallback call, and repeatedly exploit subtraction that wrapped the balance around.The repeating mechanism resembled the DAO re-entrancy attack and enabled funds to be stolen.
  • Mitigation: The Solidity compiler did not flag integer overflow/underflow errors, leaving insecure arithmetic undetected by compilation alone.The survey identifies SafeMath arithmetic functions as a mitigation for addition, subtraction, and multiplication.
  • Broader context: Solidity’s fixed value and integer-type limitations contribute to memory and bounds-checking concerns in smart contract development.The survey compares these concerns with established bounds-checking techniques for C and C++.

B. Transaction Ordering Dependency

Transaction ordering dependency arises because concurrently submitted transactions may execute in miner-determined order, making the contract’s final state depend on transaction ordering. This can expose applications such as decentralized stock markets to unexpected prices, while timestamp-based critical operations introduce a related manipulation risk.

  • Transaction ordering dependency: Concurrent transactions can execute in miner-determined order, so the contract’s final state depends on which transaction runs first.Transactions Ti and Tj can move the contract from state S to different states Si or Sj.
  • Transaction ordering dependency: In decentralized stock markets, reordered transactions can make buyers pay significantly more than the price they observed when submitting an order.Sellers may update prices while buyers’ transactions await execution.
  • Timestamp dependency: Timestamp-dependent operations are vulnerable because miners can vary block timestamps and manipulate critical execution outcomes.The timestamp may vary by approximately 900 seconds across blocks, and miners can alter local timestamps by a few seconds.
  • Timestamp dependency: A timestamp-based random value can control a critical call, allowing a malicious miner to modify the timestamp and trigger the operation.The random function derives roll from the block timestamp, then conditionally executes a send operation.
  • Mitigations: The survey recommends locking transaction order with a FIFO mechanism and avoiding block timestamps in critical variables, using block numbers for constants instead.It also advises against relying on block hash values in crucial components because miners may manipulate related execution inputs.

D. Mishandled Exception Issues

Mishandled exception issues occur when calls fail but the caller does not detect or propagate the failure. Attackers can deliberately exhaust the EVM call stack, causing payments to fail and enabling earlier payout in vulnerable contracts.

  • Exception handling: Exceptions in callee contracts can arise from insufficient gas, call-stack limits, or system errors, and callers must explicitly check return values.The callee’s exception should be propagated so the caller can verify whether execution succeeded.
  • Call-stack depth: The EVM limits call-stack depth to 1,024 frames, and an attacker can call a contract 1,023 times before invoking send to force failure.A malicious caller can intentionally interrupt execution by exceeding the limit.
  • Call-stack depth: In a Ponzi contract, exploiting call-stack depth can make other investors’ payments fail while allowing the attacker’s interest payment to arrive earlier.The attacker increases call-stack depth to 1,023 before other payments execute.
  • Ponzi example: The illustrated contract records the current investor and investment amount before sending payment to the previous investor.Its payable fallback requires a minimum investment and computes the next investment using currentInvestment * 11 / 10.
  • Unchecked send: Unchecked send operations are dangerous because failed transfers may leave the caller’s state updated as though payment succeeded.Failures can result from excessive call-stack depth or insufficient recipient gas.

E. Sequential Execution of Smart Contracts

Ethereum orders smart-contract invocations through consensus and executes them sequentially on all nodes. This sequential model limits throughput because only a bounded number of contracts can execute per second.

  • Sequential execution: Ethereum’s consensus mechanism orders smart-contract invocations and makes all nodes execute them in the same sequence.The model provides sequential execution across the network.
  • Performance limitation: Sequential execution limits transaction throughput by restricting how many smart contracts can execute per second.The paper notes that independently executable contracts could instead be run in parallel to improve throughput.

F. Other Ethereum Vulnerabilities

Ethereum smart contracts exhibit additional vulnerabilities involving call-stack limits, arithmetic, access control, transfer behavior, contract destruction, external dependencies, and gas usage. The survey organizes detection into static analysis, dynamic analysis, and formal verification methods.

  • Execution and call vulnerabilities: A 1,024-frame call-stack limit can be exceeded by recursive self-calls, allowing attackers to disrupt subsequent send operations.The attacker calls the contract 1,023 times before invoking send.
  • Arithmetic vulnerabilities: Integer overflow or underflow occurs when 256-bit integer values wrap around after reaching their maximum or minimum limits.A value reaching 2^256−1 resets to zero when incremented by one.
  • Access and transfer vulnerabilities: Unchecked send, unsecured balances, unrestricted writes, unrestricted transfers, and ORIGIN-based authentication can expose funds or storage to unauthorized behavior.The survey links unrestricted writes to the Parity multisig attack and unrestricted transfers to the DAO attack.
  • Lifecycle vulnerabilities: Destroyable contracts can be terminated through externally invoked self-destruct behavior unless killing is restricted to legitimate owners.The vulnerability concerns contracts that can be killed by an external user account or another contract.
  • Dependency vulnerabilities: Greedy contracts can permanently lock Ether when their external library contracts become inaccessible or are destroyed.The Parity multisig wallets became greedy contracts after an attacker claimed and destructed the wallet library.
  • Gas vulnerabilities: Gas-costly coding patterns increase execution costs, and GASPER was used to detect seven such patterns.The survey recommends optimizing code before deployment to reduce users’ costs.
  • Analysis methods: The paper identifies contract immutability as a security constraint because deployed errors cannot be patched like traditional software.The survey compares static, dynamic, and formal verification methods for detecting vulnerabilities before or around deployment.
  • Static analysis: Static analysis inspects source or compiled code without runtime execution to examine possible behaviors, vulnerable patterns, and expected flaws.The survey presents static analysis as one of three security-analysis categories.

1) OYENTE:

OYENTE uses symbolic execution and control-flow analysis to detect several Ethereum smart-contract vulnerabilities. Its architecture processes bytecode and blockchain state, analyzes execution paths, filters false positives, and reports vulnerable source lines.

  • OYENTE uses symbolic execution to detect transaction-ordering dependence, timestamp dependence, mishandled exceptions, and re-entrancy vulnerabilities.
  • The tool takes smart-contract bytecode and Ethereum’s current global state as inputs, using initial variable values to improve analysis accuracy.
  • OYENTE’s CFGBuilder, Explorer, CoreAnalysis, and Validator modules construct control-flow graphs, symbolically execute code, identify vulnerabilities, and filter false positives.
  • ZEUS combines abstract interpretation and symbolic model checking to verify safe programming practices and reportedly outperformed OYENTE in false-positive rate and analysis time.
  • GASPER identifies seven gas-costly Solidity patterns, while Vandal converts EVM bytecode into semantic logic relations for security analysis.

4) Vandal:

The surveyed approaches extend smart-contract analysis from static vulnerability detection to runtime traces and graph-based Ethereum activity analysis. They identify problematic contract behaviors, attacker-controlled accounts, and resource-intensive contract creation.

  • Dynamic analysis examines programs at runtime and can identify vulnerabilities missed by static analysis while validating static-analysis findings.
  • MAIAN classifies trace vulnerabilities as greedy, prodigal, or suicidal contracts by analyzing repeated invocation paths.
  • MAIAN combines symbolic analysis with concrete validation, searching execution traces according to a specified vulnerability category and search depth.
  • Graph analysis constructs Money Flow, Contract Creation, and Contract Invocation graphs from dynamically collected Ethereum data.
  • Cross-graph analysis identifies accounts controlled by attackers and abnormal contract creation that consumes substantial resources.
  • The graph-analysis methodology consists of data collection, graph construction, and graph analysis using internal and external transaction data.

C. Formal Verification Method

Formal verification applies theorem provers and mathematical methods to establish smart-contract safety and correctness properties. The surveyed frameworks translate Solidity or EVM artifacts into formal models and use different proof systems.

  • C. Formal Verification Method: Formal verification uses theorem provers or mathematical methods to prove properties such as functional correctness, runtime safety, soundness, and reliability.
  • 1) F* Framework:: The F* framework translates Solidity source and EVM bytecode into F* programs to verify runtime safety and functional correctness.
  • 1) F* Framework:: The Solidity* and EVM* tools translate source code and bytecode into shallow embedded F* programs for verification.
  • Table V summarizes formal-verification methods and the smart-contract properties they prove, while Table VI lists analysis tools, source links, and dependencies.
  • 2) Formalization using Isabelle/HOL:: Isabelle/HOL provides a sound separation-logic-based program logic for reasoning about correctness properties of EVM bytecode.
  • 2) Formalization using Isabelle/HOL:: The Isabelle/HOL method reasons about termination through Ethereum gas costs and separates deployment pre-loader code from runtime code.
  • 3) FEher interpreter using Coq:: FEther combines symbolic execution with higher-order-logic theorem proving, using Lolisa to formalize a Solidity subset’s syntax and semantics.

D. Comparison between the three analysis Methods

Static, dynamic, and formal methods differ in automation, coverage, and verification goals. Static and dynamic tools target defined vulnerability patterns, whereas formal methods prove broader correctness properties but require greater effort and expertise.

  • Static analysis cannot detect vulnerabilities that arise during execution, while dynamic analysis uses traceability to identify erroneous runtime behavior.
  • OYENTE detects four vulnerabilities, ZEUS identifies seven, GASPER detects seven gas-costly patterns, and MAIAN traces three erroneous-contract categories.
  • Formal-verification methods prove functional correctness and safety properties rather than detecting specific Ethereum vulnerability categories.
  • OYENTE missed transaction-ordering dependence and exception-handling problems in some contracts and produced more false warnings than Securify for re-entrancy.
  • Automated tools such as OYENTE, Securify, MAIAN, and Vandal are easier to deploy at scale than partially automated formal-verification methods.
  • The Solidity compiler detects basic errors and vulnerable patterns during development, and future tools could integrate with it as external plugins.
  • Formal verification requires substantial manual proof effort and scales poorly to thousands of deployed Ethereum smart contracts, despite accurate security validation.
  • The survey concludes that static and dynamic tools are handy but pattern-specific, whereas formal methods use theorem provers to validate interpreted correctness properties.
Loading 1908.08605v3…