MadMax: surviving out-of-gas conditions in ethereum smart contracts Grech et al., OOPSLA’18
We’re transitioning to look at a selection of papers from the recent OOPSLA conference this week. MadMax won a distinguished paper award, and makes a nice bridge from the CCS blockchain papers we were looking at last week.
Analysis and verification of smart contracts is a high-value task, possibly more so than in any other programming setting. The combination of monetary value and public availability makes the early detection of vulnerabilities a task of paramount importance. (Detection may occur after contract deployment. Despite the code immutability, which prevents bug fixes, discovering a vulnerability before an attacker may exploit it could enable a trusted third party to move vulnerable funds to safety).
MadMax is in the same vein as Securify, performing EVM bytecode analysis using Datalog (also with Soufflé) to infer security issues in contracts. In this instance, MadMax focuses on detecting vulnerabilities caused by out-of-gas conditions. The paper touches on some nice reusable building blocks (e.g. Vandal). I could easily see Vandal + Soufflé becoming a standard foundation for powerful EVM-based smart contract analysis.
MadMax is available on GitHub at https://github.com/nevillegreech/MadMax.
MaxMax analyzes the entirety of smart contracts in the Ethereum blockchain in just 10 hours (with decompilation timeouts in 8% of the cases) and flags contracts with a (highly volatile) monetary value of over $2.8B as vulnerable. Manual inspection of a sample of flagged contracts shows that 81% of the sampled warnings do indeed lead to vulnerabilities, which we report on in our experiment.
(The $2.8B number in the paper is based on an exchange rate of $400 USD/ETH. As I write this the 7.07 million ETH contained in those contracts at the time is today worth around $864M).
Since it takes no more than 20 seconds for MadMax to check a contract, it’s well worth considering adding it to your standard smart contract development arsenal.
What are ‘out-of-gas’ vulnerabilities?
Gas fuels computation in Ethereum, and is a embedded as part of the platform to avoid wasting the resources of miners. If a contract runs out of gas the EVM will raise an exception and abort the transaction.
A contract that does not correctly handle the possible abortion of a transaction, is at risk for a gas-focused vulnerability. Typically, a vulnerable smart contract will be blocked forever due to the incorrect handling of out-of-gas conditions: re-executing the contract’s function will fail to make progress, re-yielding out-of-gas exceptions, indefinitely. Thus, a contract is susceptible to, effectively, denial-of-service attacks, locking its balance away.
For example, the following line of code lead to an out-of-gas vulnerability in the GovernMental smart contract:
creditorAddresses = new address;
Behind the scenes it results in an iteration over all locations in the array, setting them to zero. With enough creditors the contract will run out of gas and be unable to make progress beyond this statement.
The Ethereum programming safety recommendations warn against performing operations for an unbounded number of clients, but outside of the payments case this advice does not seem to have been taken to heart in practice.
The NaiveBank below will no longer be able to apply interest if it succeeds in attracting enough accounts:
When loops are required the recommendation is to check the amount of gas at every iteration, and keep track of progress through the loop so that the contract can resume from that point if it does run out of gas. We could re-write the apply interest routine using these guidelines as follows:
This pattern is, as we determine, rarely used correctly in existing smart contracts, demonstrating the community’s unawareness of the dangers inherent in certain smart contract designs.
A related issue is wallet griefing. When a transfer is made a fallback function may be called on the recipient’s side. Thus sending Ether can end up invoking untrusted code. Ethereum best practice is to check the result of the send and abort the transaction by throwing an exception if a transfer fails. But when the exception is thrown in the middle of a loop, just aborting the transaction may no longer be enough. Consider the following code:
If an attacker makes themselves an investor below the minimum threshold and provides a callback function that deliberately runs out of gas (known as a ‘griefing wallet’) then the contract will fail (and will fail again if retried).
The following code will also run out of gas if 256 or more payees are added, due to integer overflow on the inferred type of var i as uint8. (In this instance at least, that’s arguably better than the infinite loop alternative).
The MadMax approach
MadMax’s most fundamental decision is to operate at the level of EVM bytecode. This means analysis can run on any contract regardless of the source language and regardless of whether the source code is available or not (only 0.34% of contracts on etherscan.io have source code available). This design decision is a bold one though, because the EVM instruction set is low-level (much lower level than e.g. JVM bytecode).
In the bytecode form of a smart contract, symbolic information has been replaced by numeric constants, functions have been fused together, and control flow is hard to reconstruct.
For example, compared to JVM bytecode:
- EVM does not have notions of structs, objects, or methods
- EVM bytecode is untyped
- Control-flow structures are much harder to infer in EVM
- Value-flow analysis is necessary even to determine the connectivity of basic blocks
- EVM bytecode translates calls to jumps, with no defined method invocation and return instructions
MadMax builds on top of the Vandal decompiler which accepts EVM bytecode as input and produces output in a structured intermediate representation comprising a control-flow graph, three-address code for all operations, and likely recognised function boundaries.
We observe that the EVM bytecode input is much like a functional language in continuation-passing style (CPS) form… The setting of CPS input and needing to detect value and control flow is precisely that of control-flow analysis (CFA)…
The CFA is implemented in Datalog, using the Soufflé datalog engine.
Layers of inference
The MadMax analysis consists of several analysis layers that progressively infer higher-level concepts about the analyzed smart contract. Starting from the 3-address-code representation, concepts such as loops, induction variables, and data flow are first recognized. Then an analysis of memory and dynamic data structures is performed, inferring concepts such as dynamic data structures, contracts whose storage increases upon re-entry, nested arrays, etc…. Finally, concepts at the level of analysis for gas-focused vulnerabilities (e.g. loop with unbounded mass storage) are inferred.
Each layer asserts facts that can be used by higher layers. To give a feel, here are the rules for basic loop and data flow inference:
Building on these we can infer loop bounds:
And dynamic data structures:
This lets us specify gas-focused rules:
And at the very top of the tree, the Datalog rules for identifying possible out-of-gas vulnerabilities:
The dataflow analysis is neither sound nor complete (i.e., not all possible flows are guaranteed to be found, and not every inference is guaranteed to hold). However, MadMax is soundy, making an effort to achieve soundness within the limits of scalability. This approach is certainly plenty good enough to make MadMax highly useful.
Findings
One of the interesting findings from an early analysis in the paper is that relatively complex contracts (as measured by the number of basic blocks) are holding most of the Ether. In other words, the most valuable targets are also those most in need of verification assistance.
Using MadMax the team analyse all contracts on the Ethereum blockchain as of April 9, 2018: that’s 6.33 million contract instances from 91.8K unique contracts. MadMax is run on a single machine with 512GB of RAM, and a cutoff off 20s for decompilation. Contracts that take longer than this to decompile are considered to have timed out. It takes 10 hours to analyse all these contracts, with each contract taking on average 5.6s for decompilation, and 0.3s for analysis. 8.2% of contracts overall failed to decompile with Vandal in the allotted 20s timespan.
MadMax flags 4.1% of these contracts as being susceptible to unbounded iteration, 0.12% to wallet griefing, and 1.2% to overflows of loop induction variables. In total these contracts contained 7.07M ETH.
Although checking and budgeting loops by gas at run-time is recommended as a way to avoid gas-focused vulnerabilities, the analysis also shows that programmers have not yet taken this advice to heart:
For the ~5,000 contracts flagged by MadMax, the authors select 13 at random (with the constraint that source is available) for manual analysis (if I’d spent all that effort building a contract analyser, I think I’d be interested to inspect way more than 13 flagged contracts!). The manual inspection reveals that 11 of these contracts do indeed exhibit 13 distinct vulnerabilities, with 16 flagged by MadMax for a precision of 13/16 = 81%. Section 6.1 in the paper presents details of some of the vulnerabilities found in these deployed contracts.
Our approach is validated using all 6.6 million deployed smart contracts on the blockchain and demonstrates a scalability and concrete effectiveness. The threat to some of these smart contracts presented by our tools is overwhelming in financial terms, especially considering the high precision of warnings in a manually-inspected sample.