Formal Verification and Incentive Simulation as Necessary Complements in Smart Contract Security

Photo by Adrien Converse

This post is the product of collaboration between Gauntlet and Peteris Erins (Auditless) in the intersection of formal verification and incentive simulation. We thank Haseeb Qureshi and Charlie Noyes for their review feedback.

We believe that agent-based simulation can help analyze smart contracts and protocol behavior. But other methods exist, such as formal verification. Formal verification makes logical guarantees that appear stronger than the statistical guarantees of simulation. Is it better than incentive simulation at answering security questions we care about? In this post we explore formal verification and argue that it is a strong complement to simulation.

We will cover:

• Part 1. A high level overview of the Uniswap contract
• Part 2. How to test the security of blockchain systems
• Part 3. A history of formal verification for the Uniswap smart contracts
• Part 4. How we applied formal verification
• Part 5. Our results and why we don’t think formal verification is a complete solution for testing security

Overview

Formal verification can provide unique insights into smart contract logic and security. However, when trying to make statements about the financial outcomes of a smart contract, formal verification is insufficient.

Agent-based simulation allows a set of simulated agents to interact with a contract. Our goal was to apply formal verification technology to automatically discover valid contract actions on a Uniswap exchange and analyze a sequence of transactions.

The purpose of using agents is two-fold: it allows us to anticipate actual use in the protocol design phase, and it supports on going verification in the implementation phase. Agent simulations allow us to project how real users will behave when they interact with the contract.

Follow-up blog posts will show how more efficient stochastic techniques in incentive simulation can be applied to derive several insights about Uniswap.

Part 1. A high-level overview of the Uniswap contract

More on uniswap.io

The Uniswap exchange is a set of smart contracts that allow anyone to trade ether and ERC20 token pairs without submitting an order to an order book. A single Uniswap Exchange contract supports a specific ether/ERC20 token and anyone can create a new token pair by using the Uniswap Factory contract. Once the exchange is set up, it operates autonomously:

• Liquidity creation. A liquidity provider will first provide ether and the token at the current exchange rate to Uniswap. More can be added/removed at any point.
• Trading. Market participants can then trade directly with the Uniswap Exchange contract.
• Pricing algorithm. The price for a given trade is automatically determined using a “constant product market maker” model. During a given trade Uniswap will set the price so as to preserve the product (x * y = k) of quantities of ether and the given token,
• Liquidity fees. A small fee is levied and allocated to the liquidity providers.

For a more detailed explanation of how Uniswap works, see this post.

Part 2. How to test the security of blockchain systems

There are two questions we need to answer to know a system like Uniswap is secure:

• Correctness. Does the code follow our intended model (written as a specification or otherwise)?
• Effectiveness. Would our intended model incentivize the desired behaviors?

Formal verification can only help with some of the former and little of the latter. A question like “how should we set the fee rate” simply cannot be answered by formal verification.

Part 3. A history of formal verification for the Uniswap smart contracts

Formal verification

Many projects have experimented with using formal verification techniques to prove their contracts are correct. For relatively simple smart contracts, this can be very doable. Formal verification and program analysis techniques can determine whether the code obeys a given specification, and it can often surface deadly counterexamples.

Prior work

The existing lightweight formal verification of Uniswap is a good example of what can be achieved with these techniques. Both the market maker (x * y = k) model and its implementation through addLiquidity, removeLiquidity, ethToTokenSwapInput, and ethToTokenSwapOutput is verified using the KEVM framework. An assumption is made that the existing ERC20 contract is “well-behaved”.

In a follow-up audit by ConsenSys Diligence, the team was able to reason what could happen if this assumption was broken. They discovered that malicious implementations of ERC20 tokens could be used to trick market participants, allowing the attacker to reenter the Uniswap contract and drain more funds at the same cost.

In principle, it’s possible to capture this extended specification as a code template. One could represent and call a semi-ERC20 compliant contract (same interface, but not necessarily ERC20 behavior) and attempt to use formal verification to discover the attack. In practice, this makes the formal verification problem much more computationally complex due to increased branching in the underlying SMT solver when it's used to discover arbitrary programs. This technique is sometimes called “program synthesis”. This survey by Microsoft Research is a good starting point to learn more.

These challenges illustrate two additional limitations associated with formal verification (including program synthesis):

• Complete specifications can be challenging to write and express.
• Current formal verifiers only work well with simple contracts and simple specifications.

Part 4. How we applied formal verification

Formulating the problem

To test how the contract would behave under the influence of a set of agents, we first tried to use symbolic analysis applying it to automated action discovery. Symbolic analysis translates code into a set of formulas that can be solved by an SMT solver. SMT solvers are an extension to SAT solvers that go beyond boolean formulas (making statements about simple propositions) to formulas that involve integers, bit vectors, arrays and others forms of data that commonly occur in programming.

A simple way of looking at symbolic analysis is that it can be used to formally specify a hypothesis about a given smart contract, prove that hypothesis true, or produce a counter-example.

For example, in formal verification, a hypothesis is usually an assertion about the contract, e.g., “the value returned from function double is always even”.

pragma solidity ^0.5.1
contract Doubler {
  function double(uint x) pure public returns (uint) {
    uint y = 2 * x;
    require (y % 2 == 0); // This assertion could be checked via FV
    return y;
  }
}

We are looking for validation that the given assertion holds true under some set of transactions.

To use symbolic analysis for action discovery, we set the following hypothesis: “the Uniswap contract supports no valid transactions”. If that was proved false, the counter-example would then be a set of inputs that produce a valid contract transaction.

Symbolic analysis

We supplied a black box symbolic interpreter with a modified Uniswap Exchange contract, an agent pool of available funded Ethereum accounts and a restricted set of actions (matching to contract functions). Completed actions were replayed on two test chains — a consensus test chain and a pure EVM copy (maintained in order to preserve changes to contract storage). The goal was to discover a valid set of arguments to complete a transaction and advance the current state.

Part 5. Our results and why we don’t think formal verification is a complete solution for testing security

This approach is tenable, but we discovered three limitations for this particular contract that are indicative of challenges with symbolic analysis and formal verification in general:

1. Weak performance
2. Difficulty of applying optimization to choose actions
3. Necessity to modify the contract/set-up, in this case for performance: inlining calls, removing deadline considerations and send actions

We believe challenges 1–2 can be overcome by using stochastic simulation, and therefore concluded that symbolic analysis is best used tactically to verify certain aspects of the contract/model or support its understanding. In the following we detail our approach and explain our findings.

1. Weak performance

We used a rewriting-based bounded model checker for the symbolic analysis that operates at EVM bytecode level. It differs from state-based symbolic interpreters like Mythril and Manticore in that it applies the SMT-solver in one go after contract blocks are fully expanded rather than incrementally on discovery of each block. Another difference is that false negatives are not tolerated. The underlying SMT solver we used is Z3. The interpreter includes several optimizations, which we detail below.

As an output, we extracted the argument array (also known as CALLDATA) and using the contract interface, translated into a valid set of high-level arguments for the relevant contract function.

Example modified bytecode output

We started with a direct SMT-translation of the bytecode contract and implemented several optimizations:

• A multi-level decompiler with block pruning
• A custom wrapper over Z3 with operators for non-determinism
• Modular representations of common data
• Binary typing at EVM level
• Advanced concretization

Excerpt from our SSA representation

This was the performance for each function/action:

[All times measured on a MacBook Air 2013, i7 8GB]

╔═════════════════════╦═══════════════╦═══════════════╗
║    Function name    ║ Time of 1 run ║ Action space  ║
╠═════════════════════╬═══════════════╬═══════════════╣
║ addLiquidity        ║ 30 minutes    ║ {add, remove} ║
║ removeLiquidity     ║ 7 hours       ║ {add, remove} ║
║ ethToTokenSwapInput ║ 8 hours       ║ {add, swap}   ║
║ *removeLiquidity Z3 ║ 2 minutes     ║ n/a           ║
╚═════════════════════╩═══════════════╩═══════════════╝

The final starred example was a direct Z3 implementation of the removeLiquidity function, e.g., a representative “theoretical minimum”. The action space represents which contract functions were available as actions to the agent. Add stands for addLiquidity, etc.

To interpret these results, we have to explain symbolic analyzer performance characteristics. In our instance, more than 90% of computational time is spent directly in the SMT solver. Therefore most of the effort in performance optimization is spent on optimizing how the contract is rewritten for the SMT solver.

Unfortunately bit-vector multiplication is a challenge for current SMT solvers. Let’s assume the SMT solver performance is (very) loosely tied to the number of propositional terms required. To illustrate, each number in the EVM is represented as a 256-bit word. In Z3, these words are further “exploded” into 256 propositional variables representing each bit. Up to 256 partial sums are required to represent bit vector multiplication, each one represented as another 256-bit word, requiring on the order of 65,000 variables. The removeLiquidity function contains four multiplications in total.

While SMT solver performance is not predictable in any straightforward or arithmetic way, the impact of multiplication and division on this contract was also independently verified by removing it from the source (the resulting run-time was negligible).

This is a good example where a conceptually simple contract can require unpredictably large solution times. In general, it’s hard for a non-expert to predict SMT-solver performance, and as we have seen it’s not necessarily correlated with lines of code used or other easily discernible metrics.

2. Difficulty of applying optimization to choose actions

What made SMT solving attractive for this application is its potential to discover optimal actions. The optimizing SMT solver “vZ” is provided as part of Z3 and supports solving for valid and optimal counter-examples according to a variable we optimize. It combines various optimization algorithms for sub-problems.

Optimizing solver interface from vZ — an Optimizing SMT Solver by Bjørner et al.

We completed experiments to assert whether the optimizing solver can be used to discover optimal trades according to a given price schedule, but unfortunately the solver ran for over 24 hours.

We think optimization could still be computationally feasible in specific instances where the contract is simpler and the optimization problem readily maps to an available algorithm in “vZ”, e.g., the simplex method for linear problems.

3. Necessity to modify the contract

In formal verification, reducing contract complexity (especially at bytecode level) can be critical for performance or a pre-requisite to apply formal verifiers that depend on input structure.

The key modifications we made to the Uniswap contract were to remove complexity associated with sub-calls and external calls and focus on the exchange logic:

• Removed internal and external sub-calls, inlining internal calls and modeling ERC20 account holdings internally within the contract
• Removed send actions
• Removed deadline constraint for timestamps

The role of symbolic analysis in incentive simulation

In this blog post, we’ve shown how symbolic analysis often falls short for analyzing complex systems like Uniswap when compared to agent-based simulations. That said, formal verification is an important and powerful tool. But it is best applied tactically as an augmentation of broader incentive simulations:

• Model verification. Verify a simplified simulation model
• Model extraction. Help extract a model automatically from code by validating actions
• State suggestion. Supply the simulation with novel or extreme starting states
• Local optimization. Verify assumptions about local optimality using built in optimizers