Formal Verification in Tezos

What is Blockchain (again)

  • Ledger DB
  • Distributed
  • Open network
  • Token for incentives
  • Smart contracts

Safety Requirements of Blockchain

As a consequence of introduction of token rewards
for open distributed DB:

  • Speculative money flows in.
  • System must be open source.
  • Security holes are immediate targets for theft.

Blockchain must have very high level of security.

Safety of Smart Contracts

Smart contracts must be also very secure.

Past incidents around smart contracts:

  • The DAO (3.6M ETH, 15% of circulation, 50M USD stolen)
  • Parity vulnerability#1 (150K ETH, 32M USD stolen)
  • Parity vulnerability#2 (513K ETH, 160M USD frozen)

High level of security is required here too.

The DAO

The DAO

Blockchain is a Big Pile of Components

  • Protocol: consensus, incentive design, transaction semantics
  • Smart contract: semantics, compiler
  • Cryptographic algorithms
  • P2P networking
  • Storage

All of these components must be secure.

How to Secure Blockchain

Test
Important but not enough.
Formal verification
The way to go.

Software Test

Run a system under given conditions
to see everything goes fine.

  • Run and see, then repeat. Easy.
  • Testable only few corner cases
  • No guarantee for the untested cases.

Formal Verification

Mathematically prove programs have good/bad properties.

  • Property is assured for all the cases,
    if proven.
  • Proving is generally much harder than tests.

Formal Verification Methods

  • Static typing
  • Model checking
  • Theorem proving

Static Type Checking

Express properties of values and expressions in types.
Restrict program compositions to those typable,
to assure the properties hold for the entire program.

  • Pros: automatic if type inference is available.
  • Cons: relatively weak expressive power.

Model Checking

Abstract a program to a finite state transition system,
then check it satisfies the properties we want.

  • Pros: automatic. A counterexample is given at failure.
  • Cons: Hard to provide a good modeling.

Theorem Proving

Prove the property of program directly,
using proof assistant such as Coq:

  • Pros: most powerful
  • Cons: Writing a proof can be very hard.

Formal Verification for Blockchain

Formal verification is used for critical systems such as:

  • Aerospace industry
  • Nuclear plants

Blockchain is also a critical system. It must be formally verified.

It is also an ideal target of formal verification:

  • No hardware. Open source.
  • Smart contract is a programming language.

Tezos and Formal Verification

  • Statically typed smart contracts
    both at VM and high level language levels
  • Modeling of smart contract interpreter using Coq,
    and correctness proofs of smart contracts using it.
  • Correctness of cryptographic primitives

Incoming:

  • Correctness proof of sparse Merkle tree storage using F*.
  • Certified compiler of smart contracts.
  • etc.

Michelson: Tezos Smart Contract VM

  • Stack VM
  • Purely functional: no side effects
    • No mutable variables
    • Transactions are not side effects. Re-entrancy bug is impossible.
  • With strong static typing
    • No runtime type mismatch like "hello" + 10
    • Different numeric types for currency, \(\mathbb{N}\), \(\mathbb{Z}\), ꜩ.
  • Arbitrary precision \(\mathbb{N}\) and \(\mathbb{Z}\). No overflow / underflow
  • VM level data structures: Lists, sets, maps, options

Michelson interpreter

Implements the semantics of Michelson in node:

Purely functional: no side effects

Secured by GADTs (Guarded Algebraic Data Types)

  • VM state (code and stack) construction is assured well-typed in the VM type system.
  • Evaluation (state-to-state transition) preserves the well-typedness.

Mi-Cho-Coq: VM modeling in Coq

Michelson is reimplemented in Coq proof assistant.

  • Provides framework to prove correctness around Michelson.
  • Found documentation bugs in the specification.

Smart Contract Correctness Proofs

Using Mi-Cho-Coq.

例: multi-sig contract
An operation to the account is performed only when enough number of signatures of registered users are attached.

https://gitlab.com/nomadic-labs/mi-cho-coq/blob/master/src/contracts_coq/multisig.v

HACL*: Verified Cryptography

Formally verified cryptographic functions in F*.

  • ChaCha20, Salsa20, HMAC, SHA-256, SHA-512, Ed25519, etc.
  • F* compiles down to fast C code.
  • Properties proved:
    • Memory safety
    • Correctness of the algorithm
    • Secret independence: immune to the side channel attacks

F*

Functional language with refinement types, developed by Microsoft:

  • Compatible syntax with OCaml
  • Some verifications can be done automatically by Z3
  • Extraction to OCaml, F#, C, WASM, ASM

On Going Projects

They are just I know so far:

Plebeia
Sparse Merkle tree for storage.
The correctness of tree operations will be verified by F*
Certified compiler of smart contract
Prove the correctness of compilation from higher level language to Michelson
Archetype
DSL for contracts in Tezos. Verification using Why3 deductive program verification platform.

Tezos and Formal Verification

  • Blockchain is a critical system.
  • Test is important, but FV is also required.
  • All components should be verified.
  • Tezos is a very good target to perform FV.