Blockchains:
new home forproven-correct
softwareParis, 2017-2-17
Yoichi Hirai

Lyon: 2014 January“Have you heard of a web sitewhere you can get Bitcoin forproving theorems?”“Yeah,I created the proof market.”Proving software correct•

In Lyon, I was attending workshops about
formal verification•

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

Formal in“formal verification”
Usual Mathideacorrect
but boring

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

Formalised Mathnoidea

just looking
at “form”

correct

Use proof checkers
against lots of cases•

Kepler’s conjecture “•

need to see all other ways are less efficient•This involves checking lots of corner cases.
Flyspeck project (led by Thomas Hales) used
Isabelle and HOL-light•(That sounds useful for software.)is the most compact”

Proven-correct software• seL4: a microkernel

ARM assembly proven to behave as Haskell-like spec
(NICTA, Australia, 2009)• CompCert: a C compilerresults proven to behave the same as the C source(INRIA, France, 2008; Xavier Leroy)

Compiler breaker could not break CompCert

found bugs in every tool that it has tested
more than 50 bugs in GCC,
more than 100 bugs in Clang“The striking thing about our CompCert
results is that the middle-end bugs wefound in all other compilers are absent.”

http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

Testing shows the presence, not the absence of bugs

—E.W. Dijkstra

Can proofs show absence of bugs?
No.
A bug = “what happens”- “what people think should happen”
not accessible, until people are surprised
But, proofs can compare implementations and specifications,for all corner cases.

It takes time to prove
software correct
CompCert took
100,000 lines of Coq & 6 person-years of effort

Step
×1
Final×
Goal×2
Step
Step×3××××

some small change

×××

oof Market

That’s why proof market

https://web.archive.org/web/20140110015851/https://proofmark

The list of all problems / Create a new problem / Recent answers /Follow @proofmarket/ Discuss

Proof Market
This is a proof market for the Coq proof assistant.
The list of all problems / Create a new problem / Recent answers /Follow @proofmarket/ Discuss

The list of all problems
ProofMarketCreatea new problem
Recent answers
This is a proof market for the Coq proof assistant.

Let people andNewsmachine compete for
The list of all problems
Createa new0.999
problem
Somebodyearned
BTC for proving False (bybitcoinschanging the meaning of False). Well deserved.
Recent answers
A new bounty on False

NewsHow to get proofs done for bitcoins

Somebody earned 0.999 BTC for proving False (by Provechangingeverything
the meaning ofcorrect!
False). Well deserved.
1. Create a new problem
But then what would happen?
A newbounty onadd
False
2. (optional)
bounty3. wait for somebody to solve the problem on recent entries
Howto getdone forbitcoins
4. paythe proofs
price in bitcoins
if thesolver sets a strinctly positive price2014

A cat can break
proven-correct software
https://openclipart.org/detail/132427/penguin-admin

https://pixabay.com/en/cat-computer-cable-playing-animal-70736/

Ethereum against
illogical failures•cats-resistant•radiation
resistant•bad admin
resistantNo single cat can break a
proven-correct smart contract?

https://static.pexels.com/photos/54632/cat-animal-eyes-grey-54632.jpeg

I doubt it.
• But Ethereum seems an optimal deployment target
for proven-correct software.
•{

pre-condition

A simpletheorem:
ADD does
additionpost-condition"triple {OutOfGas}(⟨ h ≤ 1023⟩ **stack_height (h + 2) **stack (h + 1) v **stack h w **program_counter k **gas_pred g **continuing){(k, Arith ADD)}{(stack_height (h + 1) **stack h (v + w) **program_counter (k + 1) **gas_pred (g - Gverylow) **continuing)"

Can that scale?
•Yes, but slowly•

Verified bytecode snippets can be composed•

It takes 5 minutes of manual work to combine two
bytecode snippets•~ 10 instructions / hour•more speed requires some months of tooling•much faster than testing all possible inputs

Does this match the actual
Ethereum Virtual Machine?
•Yes, as far as the VM test suite can tell.
(with small prints)

EVM definition in Lemtcar
xte

EVM in OCaml✓

extract

EVM definiton in Isabelle
used for proving

VM test suite passes
Works the same as Ethereum Virtual Machine in C++ etc.

Does this matchthe Yellow Paper?
•No.
See pullrequests•

If you canreview
LaTeX,
that’s great
help!
Changescoming.

Small Community• EVM definition available for Isabelle/HOL andHOL4 (Coq is coming, thanks to somebody.)• received some external contributions• some researchers started projects

Proof IDE
input commands

current goal shown

you can jumpto definitions etc.

So far: EVM definitions ready•bytecode isexecutable intheorem provers& in OCaml•

Nov. 2016•

balance increaseat any moment•

reentrancy•code removal
after self-destruct
Oct. 2016

bytecode
execution on asingle contract
passes VM test
Jan. 2017•

For a 500 instruction
byte code, proved
balance does notdecrease undersome conditions
Nov. 2016

Plan: reusable verified
snippets•

string manipulation•••

math functions•

datetime

every instruction•

if-then-else•

while loop

March, 2017

July, 2017•ABIJuly, 2017•

June, 2017•reentrancy
May, 2017

provencorrect
libraries

Hire an IsabelleHOL user anddevelop provencorrect smart
contracts!

Don’t trust it•

because, just see what happened tothe proof market

(obsolete) bug bounty program:prove falsehood and get a bitcoin
Theorem f : False.
Proof.
(* fill in and change Admitted into Qed *)Admitted.

I put 0.999 BTC as bounty.

2014This is a proof market for the Coq proof assistant.
The list of all problems
Create a new problem
Recent answers

NewsSomebody earned 0.999 BTC for proving False (by changing the meaning of False). Well deserved.
A new bounty on False

How to get proofs done for bitcoins
1. Create a new problem
2. (optional) add bounty
3. wait for somebody to solve the problem on recent entries
4. pay the price in bitcoins if the solver sets a strinctly positive price
5. see the proof

How to get bitcoins for proving
1. find a problem on the list of all problems
2. (optional) contact possible payers
3. solve the problem
4. post your solution with an additional price and your bitcoin address2014

by 1A8a55WuT2oCCUsHitZzHPdZ
at
2014-01-03
21:37:47.045297
UTCThe proof of False
price 0 satoshi
that bounty
I boughtwith1
BTC
99900000 satoshi
Inductive False := I.
Theorem inhabitant : False.
Proof.
exact I.
Qed.

The content of this web page is licensed unLicense.

2014

From: x@y.fr
Hi there,
this is just a quick mail to state that I was the guy who made theexploit of the False proof on ProofMarket.
…
I have not lost the hope to prove that Coq is inconsistent though...
Cheers,Indeed, anything was provable in Coq.
I closed the site.

I trust bounties more than proof checkers.

2014

Another bounty(what could go wrong)•I proved a wallet correct (to a spec). I put 1,000 ETH at
0x0fcc015903e7e51a947ed7276a21d37a11b29e61•

Please try to take the fund•

The first one is as simple as “prove False”•A blog post is scheduled 1pm today on medium.

•(From here, I’ll set up more and more complicatedproven-correct Ethereum contracts.)

Projects waiting for you•

Resource Consumption by Gas
There is a proof on github:“With G gas, only G steps are possible”.
# of (CALL, EXTCODE, BALANCE, SSTOREs)•CompCert-style proven-correct compiler into EVM•

Proven-correct transpiler from EVM to eWASM•

Extending Oyente:
an automatic vulnerability checker (supporting all instructions)•

CSmith-style Solidity compiler fuzzing@pirapira (twitter, GitHub)

blockchainstheoremprovingstrong internal consistency
by small number
by deterministic rules &of trusted rules
cryptographic hashes &&cooperative games
contradiction explodes
limited external interface
because distributed nodes
see the world differently

because it can only talkabout mathematics
defined withinlemma whole_program_invalid_caller:"triple {OutOfGas} (⟨unat bn ≥ 2463000 ∧ ucast c ≠ w⟩ **block_number_pred bn **stack_height 0 **program_counter 0 ** caller c **storage (word_rcat [0]) w **gas_pred g **continuing)
whole_concrete_program(block_number_pred bn **stack_height 0 **program_counter 8 ** caller c **storage (word_rcat [0]) w **gas_pred(g + (- Gsload (unat bn) - 2)
- 2 * Gverylow - Gverylow - Ghigh) **not_continuing ** action (ContractReturn []))"

lemma check_pass_whole_concrete:"triple {OutOfGas} (⟨unat bn ≥ 2463000 ⟩ **block_number_pred bn **stack_height 0 **program_counter 0 ** caller c **storage (word_rcat [0]) (ucast c) **gas_pred g **continuing **this_account t **balance t b **memory_usage 0)
whole_concrete_program(memory_usage 0 **stack_topmost 0 [] **program_counter 22 **this_account t **balance t 0 **gas_any **not_continuing **action (ContractCall ⦇
callarg_gas = word_rcat [(8 :: byte), 0], callarg_code = c, callarg_recipient = c, callarg_value = b, callarg_data = [], callarg_output_begin = word_rcat [0], callarg_output_size = word_rcat [0] ⦈) **block_number_pred bn **caller c **storage (word_rcat [0]) (ucast c))"