Skip to content

Why Model-checking in Smart Contract

Smart contracts handle assets and crypto-currencies, errors can cause huge economical losses. Example:

  • DAO hack 3.6 million Ether stolen
  • Parity Wallet hack: 150k Ether stolen
  • Parity Wallet freeze: 500k Ether frozen

Smart contracts cannot be modified after deployment. Immutable code results in immutable bugs.

Thus, formal verification of contracts prior to deployment is desiderable.

On Software Verification

Testing can't prove absence of bugs.

Formal verification allows to

  • prove/disprove correctness
  • find bugs

Most verification problems are undecidable.

Soundness: \(V(P,S)\Rightarrow\) program \(P\) satisfies specification \(S\).

Completeness: program \(P\) satisfies property \(S\Rightarrow V(P,S)\)

Formal verification techniques are usually sound but not complete.

Software Model Checking

Translate code and properties of interest to constraints.

Check whether the constraint are satisfiable with solvers (e.g. SMT)

Solidity Complier

Solidity compiler has a built-in software model checker

Usage:

  • pragma experimental SMTChecker

Require and Assert

require(bExpr): The require function should be used to ensure valid condition on inputs and contracts state variables, or to validate return values from calls to external contracts.

assert(bExpr): An assertion represents an invariant in the code. A property that must be true for all transactions, including all input and storage values, otherwise there is a bug.

At runtime, require and assert behave similarly: if the condition does not hold, they revert the transaction

For the model checker, instead:

  • Require is an assumption
  • Assert is the verification target

Solidity Model Checker

The solidity model checker tries to verify that all assert are always satisfied.

If verification fails it returns a warning and possibly a counter-example.

  • Arithmetic underflow and overflow
  • Division by zero
  • Trivial conditions and unreachable code
  • Popping an empty array
  • Out of bounds index access
  • Insufficient funds for a transfer