Source-linked AI summary
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor
TL;DR
Smart contracts hold valuable assets but cannot be patched after deployment, motivating analysis of vulnerabilities that emerge across repeated invocations. The paper characterizes trace vulnerabilities and implements MAIAN using symbolic analysis with concrete validation. Across nearly one million contracts, MAIAN flags thousands of potentially vulnerable contracts, confirms vulnerabilities at a high true positive rate, and finds the Parity bug.
Problem
Smart contracts are difficult to secure because they are immutable after deployment, interact with complex environments, and can be repeatedly invoked while handling valuable coins.
Method
MAIAN analyzes Ethereum bytecode using symbolic analysis of multi-invocation traces followed by concrete validation of potential vulnerabilities.
Results
34,200 contracts were flagged, and 3,686 vulnerabilities were confirmed among 3,759 validated contracts, yielding an 89% true positive rate.
Takeaways & Limitations
Trace properties provide a way to automatically detect greedy, prodigal, and suicidal contracts across repeated executions, including the Parity bug.
Takeaways & Limitations
The vulnerability characterization may classify intentional contract behavior as vulnerable, since killability, indefinite fund retention, or transfers to unknown addresses can be valid design choices.
Abstract
from arXiv · showhide
Smart contracts---stateful executable objects hosted on blockchains like Ethereum---carry billions of dollars worth of coins and cannot be updated once deployed. We present a new systematic characterization of a class of trace vulnerabilities, which result from analyzing multiple invocations of a contract over its lifetime. We focus attention on three example properties of such trace vulnerabilities: finding contracts that either lock funds indefinitely, leak them carelessly to arbitrary users, or can be killed by anyone. We implemented MAIAN, the first tool for precisely specifying and reasoning about trace properties, which employs inter-procedural symbolic analysis and concrete validator for exhibiting real exploits. Our analysis of nearly one million contracts flags 34,200 (2,365 distinct) contracts vulnerable, in 10 seconds per contract. On a subset of3,759 contracts which we sampled for concrete validation and manual analysis, we reproduce real exploits at a true positive rate of 89%, yielding exploits for3,686 contracts. Our tool finds exploits for the infamous Parity bug that indirectly locked 200 million dollars worth in Ether, which previous analyses failed to capture.
1 Introduction
Smart contracts combine irreversible deployment, difficult testing, repeated invocation, and valuable assets, creating distinctive security risks. The paper characterizes trace vulnerabilities and introduces MAIAN to detect contracts that lock funds, leak funds, or can be killed by arbitrary users.
- Security motivation: Smart contracts cannot be patched after deployment and are difficult to test because they interact with other contracts, external services, and repeated user transactions.The value of coins held or processed by contracts creates strong incentives for profitable attacks.
- Trace vulnerabilities: Trace vulnerabilities are bugs detectable only across long sequences of contract invocations rather than isolated executions.The characterization is intended to capture vulnerabilities in entire execution traces.
- Vulnerability categories: Greedy, prodigal, and suicidal contracts respectively lock funds indefinitely, leak funds to arbitrary users, or can be killed by any user.These categories formalize examples drawn from known incidents and broader classes of previously unreported bugs.
- MAIAN: MAIAN analyzes Ethereum contract bytecode with symbolic analysis and concrete validation, without requiring source-code access.The tool is designed to reason about trace properties and validate potential vulnerabilities with concrete exploits.
- Evaluation: 970,898 contracts were analyzed, with 34,200 flagged and 3,686 confirmed vulnerabilities among 3,759 concretely validated contracts at an 89% true positive rate.Vulnerabilities were uncovered in an average of 10 seconds per contract, and the tool found the Parity bug involving 200 million dollars worth of Ether.
2 Problem
The paper defines trace vulnerabilities as contract weaknesses revealed across sequences of invocations and focuses on greedy, prodigal, and suicidal behaviors. MAIAN analyzes bytecode with symbolic analysis, then concretely validates candidate exploits on a private Ethereum fork.
- Problem: Trace vulnerabilities concern contract behavior across long sequences of invocations rather than isolated execution paths.An execution trace is a sequence of contract runs recorded on the blockchain.
- Problem: The three target properties are arbitrary killing, indefinite Ether locking, and careless Ether release to arbitrary addresses.These correspond to suicidal, greedy, and prodigal contracts, respectively.
- Examples: A bounty contract can leak all its Ether because anyone can invoke payout with recipient lists of their choice and no sender restriction is checked.The function checks only list size, allowing a caller to specify recipients and amounts.
- Examples: The ParityWalletLibrary can be killed through two invocations: first setting ownership and the required owner count, then invoking kill.Providing an empty owner array sets the required count to zero, enabling suicide.
- Examples: Greedy contracts remain alive while locking Ether indefinitely, including contracts that lack reachable instructions for sending Ether out.Killed contracts can also become posthumous when later-sent Ether accumulates without executable code.
- Approach: MAIAN combines symbolic analysis of contract bytecode with concrete validation of generated inputs on a private Ethereum fork.The validation stage classifies candidates as true or false positives without changing the official blockchain.
3 Execution Model and Trace Properties
The paper models smart-contract behavior as labeled, multi-transaction traces and expresses vulnerabilities as predicates over those traces. This framework captures greedy, prodigal, and suicidal behaviors by relating contract states, transitions, and messages.
- Execution Model and Trace Properties: Trace properties characterize unwanted smart-contract behavior across sequences of states and transitions, rather than isolated configurations or instructions.The model includes both safety properties, where nothing bad happens, and liveness properties, where a desired action eventually occurs.
- EVM Semantics and Execution Traces: ETHERLITE represents execution with activation-record stacks and blockchain contexts, while execution labels identify transitions such as storage access, calls, and suicide.The CALL rule transfers Ether subject to the contract’s current balance, and SUICIDE transfers all funds to the caller.
- EVM Semantics and Execution Traces: A projected contract trace records a contract’s states interleaved with its immediate transition labels, ignoring other contracts’ states within the same execution.A multi-transactional trace concatenates complete single-transaction traces over successive blockchain states, with the final transaction not required to be complete.
- Characterising Safety Violations: Leaky contracts are defined by a triggering precondition, a side condition over intermediate trace points, and a postcondition at the trace’s end.The definition is relative to the current blockchain state, so a contract that is leaky now may cease to be leaky later.
- Characterising Safety Violations: Prodigal contracts can transfer funds or control to an arbitrary sender, while suicidal contracts let an unrecognized sender trigger a SUICIDE transition.The prodigal postcondition includes CALL with positive value, DELEGATECALL, or SUICIDE directed to the initial sender.
4 The Algorithm and the Tool
MAIAN analyzes Ethereum contract bytecode with symbolic execution across multiple invocations, then validates candidate violations through concrete executions on a private blockchain fork.
- Algorithm and Tool: MAIAN takes contract bytecode and a concrete starting blockchain context, then symbolically executes ETHERLITE rules to search for trace-property violations.The analysis begins from a state satisfying the property’s precondition and reasons about contract traces over multiple blocks.
- Symbolic Analysis: Symbolic execution represents transaction and block inputs symbolically while maintaining symbolic and concrete memories for computed contract values.This representation allows MAIAN to reason about relationships among values across repeated contract invocations.
- Execution Path Search: MAIAN searches execution paths depth-first, exploring both satisfiable branches when symbolic conditions permit and backtracking when paths cannot be resolved.Calls within the contract are handled inter-procedurally, while calls outside the contract are not simulated and produce symbolic returns.
- Handling Data Accesses: The analyzer encodes EVM memory and storage accesses as 256-bit bit-vector constraints without source-code type information.Because source code is unavailable, MAIAN defaults all encoded types to 256-bit integers.
- Validation: When a symbolic path reaches a violating state, MAIAN checks the path and property constraints for satisfiability and flags a buggy candidate.The concrete validator then executes generated transactions on a private fork and marks the candidate false positive unless the violation is reproduced.
5 Evaluation
MAIAN evaluates nearly one million Ethereum contracts using symbolic analysis, concrete validation, and manual inspection. It reports high true-positive rates for prodigal and suicidal contracts, lower rates for greedy contracts, and identifies limits tied to cross-contract calls, block state, and invocation depth.
- Experimental Setup: 970,898 smart contracts were analyzed from Ethereum’s first block through block 4,799,998, while only 9,825 had retrieved Solidity source code.The approximately 1% source-code availability underscores the bytecode analyzer’s practical scope.
- Experimental Setup: MAIAN required around 10.0 seconds per contract on average for the three vulnerability categories.The average comprised 5.5 seconds for prodigal, 3.2 seconds for suicidal, and 1.3 seconds for greedy checks.
- Results: 1,156 of 1,183 alive prodigal candidates validated on a private fork were true positives, producing a 97.72% true-positive rate.The validation involved sending test Ether to contracts that could receive it and checking whether they leaked Ether to arbitrary addresses.
- Results: 1,057 of 1,058 first-category contracts were confirmed able to receive Ether, while manual inspection found none of 25 sampled second-category contracts to be true positives.The second category was harder to confirm by testing alone, and MAIAN failed to reach relevant CALL instructions in those cases.
- Summary and Observations: 34,200 contracts were flagged, with confirmed true-positive rates of around 97% for prodigal, 97% for suicidal, and 69% for greedy contracts.Only 181 flagged contracts had verified source code on Etherscan, representing 1.06%, 0.47%, and 0.49% across the three categories.
- Summary and Observations: Invocation depth 3 was judged the optimal tradeoff after testing depths 1 through 4, because increasing depth improved results only marginally.The study tested 25,000 contracts for greedy vulnerabilities and 100,000 for the remaining categories.
6 Related Work
Prior smart-contract analyses largely target implementation flaws, language semantics, or low-level safety violations. This work instead characterizes vulnerabilities as properties of contract execution traces, extending systematic detection beyond individual instructions or states.
- Prior work: Earlier work described refund failures through simple examples but did not provide a systematic detection approach.That property is identified as closest to the paper’s greedy-contract notion.
- This work: MAIAN’s characterization is novel because greedy, prodigal, and suicidal bugs are stated as execution-trace properties rather than particular instructions or reached states.This distinguishes the paper’s approach from work focused on bad implementation practices or misused language semantics.
- Prior work: Existing symbolic tools target mishandled exceptions, transaction ordering, timestamp dependence, reentrancy, integer overflows, and related low-level issues.The cited tools analyze specific semantic or implementation vulnerabilities rather than general execution-trace properties.
- Comparison with ZEUS: ZEUS verifies user-provided policies over a Solidity-derived LLVM-like representation, whereas MAIAN reasons about Ethereum bytecode traces.ZEUS uses abstract interpretation, symbolic model checking, and standard constraint or SMT solvers.
- Formal verification: Mechanized EVM semantics and formal contract-verification efforts had not considered trace properties in the paper’s defined sense.The paper also notes related contract languages designed to simplify reasoning about executions.
7 Conclusion
The paper characterizes vulnerabilities defined over entire smart-contract execution traces and demonstrates them through MAIAN’s large-scale analysis. Across 970,898 contracts, the tool flags thousands of vulnerable contracts at a high true positive rate.
- Conclusion: 970,898 contracts were analyzed, and MAIAN flagged thousands of contracts as vulnerable at a high true positive rate.The conclusion summarizes the paper’s trace-vulnerability characterization, including greedy, prodigal, and suicidal contracts.