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

Important for Ethereum!

• Like for a web service, attacker can be anywhere
• Source code often available (good and bad)
• Prominent example: The DAO

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

Existing Languages / Tools

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

Write program in existing language and annotate with pre- and postconditions.
Program is compiled into language that understands these conditions (often why3). VC-generator generates verification conditions, 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

Following example is verified to be safe against re-entrant calls:

/// @why3 ensures {
/// @why3   to_int (old #shares) - to_int (old this.balance)
/// @why3     = to_int #shares - to_int this.balance
/// @why3 }
contract Fund {
    uint shares;
    function withdraw(uint amount) {
        if (amount <= shares) {
            shares = shares - amount;
            if (!msg.sender.call.value(amount)())
                throw;
        }
    }
}

Fineprint: We still have to reject incoming Ether

Future Steps

• Very near future:
  • Verify example token contract
  • Model "msg" (add msg.sender, etc.)
• Multi-contract conditions
• Correlate bytecode-level model with high-level language model
• Multi-transaction conditions (safety and liveness) - process calculus?

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