Gauntlet
Published in

Gauntlet

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

Two liquids merging
Photo by Adrien Converse
  • 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

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

More on uniswap.io
  • 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.

Part 2. How to test the security of blockchain systems

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

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

Formal verification

Prior work

  • 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

pragma solidity ^0.5.1contract 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;
}
}

Symbolic analysis

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

  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

1. Weak performance

Example modified bytecode output
  • 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
╔═════════════════════╦═══════════════╦═══════════════╗
║ 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 ║
╚═════════════════════╩═══════════════╩═══════════════╝

2. Difficulty of applying optimization to choose actions

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

3. Necessity to modify the contract

  • 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

  • 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

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store