Overview
Some Technicality
Own Evaluation
Summary

Defining the Ethereum Virtual Machine forInteractive Theorem Provers
Yoichi Hirai
Ethereum Foundation

Workshop on Trusted Smart Contracts
Malta, Apr. 7, 2017

1/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Outline1

Overview
Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

2

Some Technicality
EVM
Choice on Reentrancy

3

Own Evaluation
Remaining Problems

4

Summary
2/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Outline1Overview
Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

2

Some Technicality
EVM
Choice on Reentrancy

3

Own Evaluation
Remaining Problems

4

Summary
3/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Ethereum: Public Ledger with CodePublic ledger with accounts:. . . some controlled by private key holders,. . . the others (called Ethereum contracts) controlled bycode stored on the ledger.
Accounts (including Ethereum contracts) can call otheraccounts and send balance.
Calls invoke code in Ethereum contracts.
4/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Bugs in Ethereum Programs.
The DAO: funds moved much more than expected /led to network split into twoPrograms stop working when array iteration becomes toolongEthereum Name Service (prev. version):in a secret auction, bids could be added after other bids
were revealed..
.
This does not work:
1

Develop the source code of Ethereum contracts on GitHub.

2

Enough people would look at it.

3

Bugs would be found early enough.
5/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Potential Ways to Prevent Bugs in Ethereum
Programs.

Testing can check prepared scenarios
cannot find unknown attacks without luck
Code review sometimes finds attacks
Never known: how much review is enough?
Machine-checked theorem proving can enumerate everythingthat can happen, if it finishes.
You can see when proofs finish.

6/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Why Formal Proofs might Make Sense for EthereumContracts
My speculation: for Ethereum contracts the benefit of proving
might outweigh the costs.
You cannot change deployed programs
Bugs remain.
An upgradable Ethereum contract is somehow at odds withthe cause of decentralization.

The bugs are visible to all potential attackers
Ethereum contracts sometimes manage big amount of fund7/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Need of a Definition of a Programming Language inTheorem Provers

In some cases, the semantics looks like an interpreter.
In other cases, it contains clauses of possibilities.
The definition in theorem provers is code,
but it should be readable/comparable against spec.
The definition needs to be tested
Goal: what happens on-chain should be an instantiation ofthe definition in theorem provers

8/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Outline1

Overview
Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

2

Some Technicality
EVM
Choice on Reentrancy

3

Own Evaluation
Remaining Problems

4

Summary
9/32
Yoichi HiraiDefining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

We Defined the Ethereum Virtual Machine for
Isabelle/HOL, HOL4 and Coq

Coq (27 yrs. old), Isabelle (31 yrs. old) and HOL4 (ca. 30yrs. old) are interactive theorem provers, where
one can develop math proofs and have them checked.
one can also develop software and prove correctness.

“Programs” look similar in all these theorem provers
Strategic Goal: inviting users of these tools to Ethereum
contract verification.

10/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Our EVM Definition is Originally in Lem

We used a language called Lem.
Lem code can be translated into HOL4, Isabelle/HOL, Coqand OCaml.

11/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

0x04

DIV

2 Overview
1 Integer division
operation.
(Why Prove Ethereum Programs Correct
Some Technicality
0 EVM for Theorem Provers
if µs [1] = 0
We DefinedOwn Evaluation 0µ [0] ≡Summary sbµs [0] ÷ µs [1]c otherwise

How 0x05
the paper
spec2 andLeminteger
specdivision
lookoperation (truncated).
SDIV1 Signed

if
0255
−2if
The EVM definition in Lem has 2,000 lines.
sgn(µs [0] ÷ µs [1])b|µs [0] ÷ µs [1]|c ot
Most instructions are simply encoded as functions in Lem. . .
Where all values are treated as two’s complemen
Yellow Paper (original spec): Note the overflow semantic when −2255 is negateµ0s [0] ≡0x06

MOD0x07
Lem:SMOD

21

2

1

31

Modulo (remainder operation.
0if µs [1] = 0µ0s [0] ≡µs [0] mod µs [1] otherwise

Signed modulo
remainder operation.
(0if µsµ0s [0] v≡ c| A r i t h MOD −> stack_2_1_op
sgn(µs [0])(|µs [0]| mod |µs [1]|) otherw( f u n a d i v i s o r −> ( i f d i v i s o r = 0 then 0 e l s e
Where (alltreated
word256FromInteger( uvaluesi n t aare) mod( u iasn t two’sd i v icomplemensor ))0x08

Modulo (addition operation.
0if µs [2] =. . . except CALL and friends. µ0s [0] ≡(µs [0] + µs [1]) mod µs [2] otherwise
12/32
All intermediate calculations of this operationar))
ADDMOD

Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Special Treatment of CALL
During CALL instruction, nested calls can enter our program.
Nasty effects after executing CALL:
the balance of the contract might have changed
the storage of the contract might have changed
Our blackbox treatment of CALL:
by default, the storage and the balance change arbitrarily
during a CALL.
optionally, you can impose an invariant of the contract,which is assumed to be kept during a CALL
but you are supposed to prove the invariant.
Currently, we are working on a precise model of what happens
during a CALL.
13/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some TechnicalityOwn Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

We Tested Our EVM Definition against
Implementations’ Common Test
Luckily, we have test suites for EVM definitions
The test suites compare Ethereum Virtual Machine
implementations in Python, Go, Rust, C++, . . .
All EVM implementations need to behave the same, lest theEthereum network forks (ugly)

Definitions in Lem are translated into OCaml
Our OCaml test harness reads test cases from Json, runs
the Lem-defined EVM, checks the result v.s. expectationsin Json
VM Test suite: 40,617 cases (24 cases skipped; theyinvolve multiple calls)Running those 24 involves implementing multiple calls(current efforts).
14/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Problems in LATEX Specification
Test suits are the spec in effect; the LATEX spec is not tested.
While writing definitions in Lem (or previously in Coq)memory usage when accessing addresses [2256 − 31, 1)
an instruction had a wrong number of arguments
ambiguities in signed modulo:sgn(µs [0])|µs [0]| mod |µs [1]|some instructions touched memory but did not charge formemory usage
malformed definition: o was defined to be oWhile testing the Lem definition:
spurious modulo 2256 in read positions of call data
exceptional halting did not consume all remaining gas
15/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

Proving Theorems about Ethereum Programs
We used Isabelle/HOL to prove theorems about Ethereum
programs.
One theorem about a program (501 instructions) says:
If the caller’s address is not at the storage index 1, the callcannot decrease the balance
On the same condition, the call cannot change the storageTechniques:
Brute-force directly on the big-step semantics(naïvely ignoring many techniques from 1960’s and on).
Human spends 3 days constructing the proof
Machine spends 3 hours checking the proof
16/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

An InvariantWell-defined, but questionable as documentation.
inductive fail_on_reentrance_invariant :: "account_state ⇒ bool"
where
depth_zero:"account_address st = fail_on_reentrance_address =⇒account_storage st 0 = 0 =⇒account_code st = program_of_lst
fail_on_reentrance_program program_content_of_lst =⇒account_ongoing_calls st = [] =⇒ account_killed st = False =⇒fail_on_reentrance_invariant st"| depth_one:"account_code st = program_of_lst
fail_on_reentrance_program program_content_of_lst =⇒account_storage st 0 = 1 =⇒account_address st = fail_on_reentrance_address =⇒account_ongoing_calls st = [(ve, 0, 0)] =⇒account_killed st = False =⇒Yoichi Hirai
Defining EVM for Interactive Theorem Provers

17/32

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

Outline1

Overview
Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

2

Some Technicality
EVM
Choice on Reentrancy

3

Own Evaluation
Remaining Problems

4

Summary
18/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

Overall Data Structure
An account contains:balance (256-bit word)code (byte sequence)storage (2256 words)
nonce (256-bit word)
A contract invocation provides:
input data (byte sequence)
memory (2256 bytes, charged by max accessed word)
stack (up to 1024 words)
information by miner (timestamp, block number etc)
19/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

How EVM Works 1
Untitled Page

Origin AccountContract A

storage [ 50@0, 4@25996 ]byte seq
Etherprogram
counter[]

code0x60 PUSH10x080x08
0x60 PUSH1
0xff
0xff
0x55 SSTORE
...

20/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

How EVM Works 2
Untitled Page

Origin AccountContract A

storage [ 50@0, 4@25996 ]byte seq
Ether

code

programcounter[0x08]

0x60 PUSH1
0x08
0x08
0x60 PUSH1
0xff
0xff
0x55 SSTORE
...

21/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

How EVM Works 3
Untitled PageOrigin AccountContract A

storage [ 50@0, 4@25996 ]byte seq
Ethercode

programcounter[0x08; 0xff]

0x60 PUSH1
0x08
0x08
0x60 PUSH1
0xff
0xff
0x55 SSTORE
...

22/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

How EVM Works 4
Untitled Page

Origin AccountContract A

storage [ 50@0, 8@255, 4@25996 ]byte seq
Ether

code

programcounter[]

0x60 PUSH1
0x08
0x08
0x60 PUSH1
0xff
0xff
0x55 SSTORE
...

23/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

Outline1Overview
Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

2

Some Technicality
EVM
Choice on Reentrancy

3

Own Evaluation
Remaining Problems

4

Summary
24/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

An Annoying Phenomenon Called Reentrancy(transaction’s view)
Untitled Page

storage&balance are shared
Origin Accountbyte seq
EtherContract B Contract AContract A

codecode

CALL...

programcounter
[...]

...
...

CALL
...

programcounter[]

25/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

An Annoying Phenomenon Called Reentrancy(invocation’s view)
Untitled Page

Origin AccountContract A

byte seq
Etherstorage [ 50@0, 8@255, 4@25996 ]
...

CALL
...

programcounter[1]
storage [ (can be very different) ]26/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

EVM
Choice on Reentrancy

We Picked the Invocation’s View
ProA partial implementation of the other approach
Just enough for program syntax, no bigger view necessaryCon
Unnecessary diversion from the implementations/spec
Complexity due to mixture of determinism/nondeterminism
After the paper. . .
We got a deterministic definition that covers a whole block (nowsome newly-covered tests are failing).

27/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
SummaryEVM
Choice on Reentrancy

One Proving Strategy that We Took

1

Speculate an invariant of a contract“the code of the account can only stay the same orbecome empty”

2

Prove the invariant, assuming the invariant on reentrant
calls

3

(hand-waiving argument that reentrant depth is finite)

4

Take the invariant for granted and prove pre-post
conditions“if the caller is not the owner, the balance of the accountdoes not decrease”
28/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Remaining Problems

Outline1

Overview
Why Prove Ethereum Programs Correct
We Defined EVM for Theorem Provers

2

Some TechnicalityEVM
Choice on Reentrancy

3

Own Evaluation
Remaining Problems

4

Summary
29/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Remaining Problems

What can still Go WrongThis work only connects EVM spec and programs’ properties
Things can go wrong with/above programs’ properties
Proven properties are different from desired ones.
Signature forged / inverse of hash functions computed.
An exchanges calls Ethereum contracts on behalf of users
with wrong parameters (as reported yesterday)
Things can go wrong with/below EVM specBug in EVM definition can turn the theorems valueless.
Protocol changes.
Theorem provers have bugs sometimes
30/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
Summary

Remaining Problems

More Work
Ongoing:definition of a whole block, containing transactions
containing calls
modular reasoning on bytecode snippets (Hoare logic w/separating conjunction)
Not started:common Ethereum contract method/argument encoding
specification language for end-users of smart contracts
connect to test/main network

31/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers

Overview
Some Technicality
Own Evaluation
SummarySummary
We defined EVM for proof assistants Isabelle/HOL, Coqand HOL4
The EVM definition is usable for proving Ethereum
contracts correct for a specification
OutlookFormalization efforts underway for multiple message calls
Proof/tool/language/protocol developments in the proofassistants welcome
https://github.com/pirapira/eth-isabelle(Apache License ver. 2)
32/32
Yoichi Hirai

Defining EVM for Interactive Theorem Provers