Formal Verification of Smart Contracts

Dr. Christian Reitwiessner
@ethchris   github.com/chriseth   chris@ethereum.org

Dr. Yoichi Hirai
@pirapira   github.com/pirapira   yoichi@ethereum.org

ÐΞVCON2 - Shanghai - 2016-09-20

Problem

  • writing code correctly is hard
  • key goal: align mental model with machine model
  • easy to test desired behaviour
  • hard to check absence of undesired behaviour
  • reason: testing catches only finite amount of cases

How can Formal Verification Help?

Example (shortened):

contract Token {
  mapping(address => uint) balances;
  function transfer(address from, address to, uint amount) {
    if (balances[from] >= amount) {
      balances[from] -= amount;
      balances[to] += amount
    }
  }
}

Testing would probably not find an error here (do you?).

Formal verification uses techniques to "test" a program on all possible inputs and states.
Example: Is the sum of all balances unchanged by transfer()?

Formal Verification in General

  • provide formal statements
  • prove that code satisfies the statements
  • We live in 2016: there are automated provers

  • No silver bullet - source code is already formal statement!
  • Formal specification useless if not understandable
  • Key purpose of FV: complexity reduction by probing properties
    • Is the sum of balances fixed?
    • Can the smart cotnract get "stuck"?

Formal Verification is Coming!

Many big names are already in the field.

  • Ten authors from Microsoft Research, INRIA, Harvard
    "Short Paper: Formal Verification of Smart Contracts"
  • Loi Luu et al. (NUS) "Making Smart Contracts Smarter"
  • Herlihy "Blockchains and the Logic of Accountability"
    (LICS 2016 invited talk)

Blockchains are a paradise for formal verification
(Yoichi will tell why).

Existing Languages / Tools

  • C: Frama-C
  • Java: Krakatoa
  • Ada: SPARK

Write program in existing language and annotate with pre- and postconditions.
Program is compiled into language that understands these conditions (often why3), automated prover verifies conditions.

Example: Frama-C

/*@ requires 1 < num_candidates && num_candidates < MAX_CANDIDATES;
    assigns \nothing;
    ensures \result >= 1 && \result < num_candidates;
    ensures \forall integer i; 
       1 <= i < num_candidates ==> counters[\result] >= counters[i];
 */
int compute_winner(void) {
  int i, winner = 1; /* "No vote" is NOT taken into account */
  /*@ loop invariant 2 <= i && i < MAX_CANDIDATES;
      loop invariant \forall integer j;
              1 <= j < i ==> counters[winner] >= counters[j];
      loop invariant winner >= 1 && winner < num_candidates;
   */
  for (i = 2; i < num_candidates; i++)
    if (counters[i] > counters[winner]) winner = i;
  return winner;
}

Formal Verification for Solidity

This code is verified to maintain the total balance of tokens:

/// @why3 contract-prelude constant total : int
/// @why3 contract-prelude axiom total_small : total <= max_uint256
/// @why3 contract-account invariant { sum #balance = total }
contract Token {
  mapping (address => uint256) balance;
    function transfer(address _from, address _to, uint256 _val) {
    if (balance[_from] < _val) throw;
    balance[_from] = balance[_from] - _val;
    /// @why3 here assert { sum #balance = total - to_int !(__val) };
    /// @why3 here assert { to_int #balance[_to] <= sum #balance };
    balance[_to] = balance[_to] + _val;
    /// @why3 here assert { sum #balance = (total - to_int _val) + to_int _val};
  }
}

assuming the total is less than 2256.

Why3 GUI

Yoichi Hirai (09.2016-)

Logical proofs are based on computation ...jobs? Univ. Tokyo
Bring formal methods to the industry...source code? Research institute in Japan
Formal methods for OS kernels
...shorter specs?
U.S. company
Verify smart contracts! Ethereum DEV

Future Steps

  • Very near future:
    • Model "msg" (add msg.sender, etc.)
    • Mappings to mappings (e.g. transfer allowence)
  • Multi-contract conditions
  • Correlate bytecode-level model with high-level language model
  • Multi-transaction conditions (safety and liveness) - process calculus?
  • Combination with off-chain protocols
  • Provide counterexamples for verification failures

In comparison to C, we are lucky: no concurrency, simple VM, simple programs, simple language.