Formal Verification of Smart Contracts

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 2²⁵⁶.

Why3 GUI

Yoichi Hirai (09.2016-)

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.