Formal Verification forEthereum
Amsterdam, 3 May 2017
Yoichi Hirai

“formal” verification?

http://www.telegraph.co.uk/culture/tvandradio/10803323/Why-cant-we-make-drama-like-The-Pallisers-anymore.html

“formal” comes fromformalised math
Usual Mathidea
correct butboring

https://en.wikipedia.org/wiki/Emmy_Noether#/media/File:Noether.jpg

Formalised Mathno ideajustlooking at“form”
correct

formal proofs on twitter

Use proof checkers
against lots of cases•

Kepler’s conjecture “•one needs to see all other ways are less efficient•This involves checking lots of corner cases.

is the most compact”

Flyspeck project (led by Thomas Hales) used
Isabelle and HOL-light•(That sounds useful for software development too.)Proving software correct•using interactive proof assistants

CoqHOL•they use only ~20 inference rules to derive the whole math•… and that code matches specification

Steps for Proving Ethereum
contracts correct•

Ethereum Virtual Machine for theorem provers•

Test the EVM in the provers against otherimplementations•

Use the EVM for proving byte code correct againstspecifications

Proving smart contractscorrect!

The proof finishes somehow

https://github.com/pirapira/eth-isabelle

Did you prove the right thing?
•The account should not do anything wrong.
The balance should not decrease unless anauthorised account tells so.

Did you prove the right thing?
•The account should not do anything wrong.
The balance should not decrease unless anauthorised account tells so.
A non-authorised account cannot authorise anyaccount.

It’s not just about one
Ethereum contract…
Verifying Ethereum as a Whole•

Theorem (Sami Mäkelä):
No Ethereum transaction can increase the total
amount of Ether.

•Q. How can the total amount of Ether decrease?

CasperWhat is Casper•

Ethereum’s coming consensus mechanism.

•

Several different Casper protocols
https://github.com/ethereum/research/tree/master/casper
https://github.com/ethereum/research/tree/master/
casper3
https://github.com/ethereum/research/tree/master/
casper4
Vlad’s Casper
Meredith’s Casper(s)•Not easy to comprehend everything

Consensus•

The whole thing is for avoiding forks(or double-spends)•PBFT (practical byzantine fault tolerance) has“2/3 honest implies no fork”•

To make it cryptoeconomic, we need:“If a fork happens,1/3 of the deposits can beforfeited”

Proof-of-stake requires
blaming bad behaviours•“If 2/3 are honest, everything stays good” is notenough•“if something goes bad, some participants can bepenalised” is better•

Alice: “I sent it”
Bob: “I didn’t receive it”•Blaming a single party is much better.

Slashing conditions•

if a fork happens, some 1/3 should be blamed forviolating slashing conditions(signing contradicting “commit” messages /signing “commit” messages without evidence /signing “prepare” messages without evidence /signing “commit” message between two “prepare”)•many modes of failures because everyone can dowhatever•theorem prover to check all failure modes

Whenever there is a fork,some slashing condition is violated

but the pictures help only as much.

(not skippable)

Accountable safety states that, if there is a fork with commits, tlegitimate heir of the validator sets of the root, of which 2/3 artheorem

lemma accountable-safety :validator-sets-finite s =)v0 =)fork-with-commits s (h, v ) (h1 , v1 ) (h235, v2 ) =)9 h 0 v 0.
ancestor-descendant-with-chosen-validators s (h, v ) (h 0, v 0) ^one-third-of-fwd-or-rear-slashed s h 0
hproof iend

Links•@pirapira on Twitter•

pirapira on GitHub•

github.com/pirapira/eth-isabelle
Smart contract verification•

github.com/pirapira/pos
Casper verification•

yoichi@ethereum.org