Formal Verification in Tezos

- Ledger DB
- Distributed
- Open network
**Token for incentives**- Smart contracts

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.

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.

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

All of these components must be secure.

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

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.

Mathematically prove programs have good/bad properties.

- Property is assured for
**all the cases**,

if proven. - Proving is generally much harder than tests.

- Static typing
- Model checking
- Theorem proving

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.

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.

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 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.

- 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.

- 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}\), ꜩ.

- No runtime type mismatch like
- Arbitrary precision \(\mathbb{N}\) and \(\mathbb{Z}\). No overflow / underflow
- VM level data structures: Lists, sets, maps, options

Implements the semantics of Michelson in node:

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

Michelson is reimplemented in Coq proof assistant.

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

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.

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

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

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.

- 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.