Specifying the Ethereum Virtual Machine forTheorem Provers
Yoichi Hirai
Ethereum Foundation

Cambridge, Sep. 13, 2017
(FC 2017 + some updates)

1/28

Outline

ProblemMotivation
EVM as a Machine
Wanted Properties
Current Efforts
Writing Specification
Testing the Specification
Proving Ethereum Contracts Correct
Outlook

2/28

Outline

ProblemMotivation
EVM as a Machine
Wanted Properties
Current Efforts
Writing Specification
Testing the Specification
Proving Ethereum Contracts Correct
Outlook

3/28

Ethereum: Program Execution without Trusted Admin“Server side” computation dictates the society now.
Computers have owners and administrators.
I Will my program be executed unmodified?
I Will my program be available?
I Will my data kept secure from unauthenticatedmodification?
Ethereum currently uses a Bitcoin-like approach
1. to replicate programs and program states, and
2. to agree on execution traces.
Over 24,000 nodes1 are running a clone of the Ethereum
Virtual Machine (EVM).
1

According to ethernodes.org.

4/28

Typical Ethereum Usage: Deposits & Announcements
Ethereum Name Service is a sealed second-price auction.
The price is locked while the name is held.
Roughly 168,000 ETH (≈ 42,000,000 GBP) locked
for 161,000 names.

Voting Protocol McCorry, Shahandashti and Hao [FC 2017]
implemented a voting protocol on Ethereum.
The protocol requires a public bulletin board; anduses deposit to incentivize participants to perform
all steps.
Counterparty risks are now on programs (“smart contracts”).
At least you can read the code. Isn’t that enough?

5/28

The Famous Bug“The DAO” (an investment club): funds moved out
unexpectedly.
17% of total existing ETH affected.
Many miners2 accepted a protocol change to remedy thisparticular case; the network split.
The EVM didn’t have a problem; the program on top had.
EVM might be a Good Formalization Target, I Thought
I unstoppable app sounds crazy unless it’s proven correct
I easy machine (deterministic on all inputs)
I test cases for multiple implementations
I a short spec (33 pages).

2

Miners run GPUs to produce valid blocks.

6/28

0x04

Integer division
operation.
(0if µs [1] = 0
EVM turns out not too Bigµ0stoFormalize[0] ≡bµs [0] ÷ µs [1]c otherwise
DIV212 1 (anSignedintegerdivision operation(truncated).
The0x05
EVMSDIV
definition in Lem
ML likelanguage)
 specification
0if
has 2,000 lines.
µ0s [0] ≡ −2255
ifMost instructions are simply encoded as functions in Lem:

sgn(µs [0] ÷ µs [1])b|µs [0] ÷ µs [1]|c ot
Where all values are treated as two’s complemen
Yellow Paper (original spec): Note the overflow semantic when −2255 is negate
0x06

MOD

2

10x07

SMOD

210x09MULMOD

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

Signed modulo
remainder operation.
(0if µsLem:µ0s [0] ≡sgn(µs [0])(|µs [0]| mod |µs [1]|) otherw
Where| Arith MOD -> stack_2_1_op
v all
c values are treated as two’s complemen(funadivisor->(ifdivisor= 0then 0 else
0x08 ADDMOD
3 1 Modulo (additionoperation.
word256FromInteger ((uinta) mod (uint divisor))0
if µs [2] =))µ0s [0] ≡(µs [0] + µs [1]) mod µs [2] otherwise
All intermediate calculations of this operation ar
Modulo multiplication operation.

7/28

Outline

ProblemMotivation
EVM as a Machine
Wanted Properties
Current Efforts
Writing Specification
Testing the Specification
Proving Ethereum Contracts Correct
Outlook

8/28

How EVM Works 1
Untitled Page

Origin AccountContract A

storage [ 50@0, 4@25996 ]byte seq
Etherprogram
counter[]code
0x60 PUSH1
0x08
0x08
0x60 PUSH1
0xff
0xff
0x55 SSTORE...

Exported from Pencil ­ Thu Mar 30 2017 19:37:34 GMT+0200 (CEST) ­ Page 1 of 1

9/28

How EVM Works 2
Untitled Page

Origin AccountContract A

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

programcounter[0x08]

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

Exported from Pencil ­ Thu Mar 30 2017 19:38:00 GMT+0200 (CEST) ­ Page 1 of 1

10/28

How EVM Works 3
Untitled Page

Origin AccountContract A

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

programcounter[0x08; 0xff]

0x60 PUSH1
0x08
0x08
0x60 PUSH1
0xff0xff
0x55 SSTORE...

Exported from Pencil ­ Thu Mar 30 2017 19:40:01 GMT+0200 (CEST) ­ Page 1 of 1

11/28

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 PUSH10xff
0xff
0x55 SSTORE...

Exported from Pencil ­ Thu Mar 30 2017 19:39:11 GMT+0200 (CEST) ­ Page 1 of 1

12/28

An Annoying Phenomenon Called Reentrancy(Transaction’s View)
Untitled Page

storage&balance are shared
Origin Accountbyte seq
Ether

Contract A

Contract B Contract A

code

code

CALL
...

programcounter
[...]

...
...

CALL
...

programcounter[]

Exported from Pencil ­ Fri Mar 31 2017 22:41:55 GMT+0200 (CEST) ­ Page 1 of 1

13/28

An Annoying Phenomenon Called Reentrancy(Invocation’s View)
Untitled Page

Origin AccountContract Abyte seq
Etherstorage [ 50@0, 8@255, 4@25996 ]...

program CALL...
counter[1]
storage [ (can be very different) ]Exported from Pencil ­ Fri Mar 31 2017 22:43:05 GMT+0200 (CEST) ­ Page 1 of 1

14/28

Outline

ProblemMotivation
EVM as a Machine
Wanted Properties
Current Efforts
Writing Specification
Testing the Specification
Proving Ethereum Contracts Correct
Outlook

15/28

Properties Wanted about a Contract

Safety Properties
I only this kind of callers can alter storage
I only this kind of callers can decrease the balance3
I the invalid opcode 0xfd is never hit(Some compilers encode safety properties using 0xfd)

Game Theoretic / Cryptographic Properties“bidding honestly” should be a dominant strategy
if a contract implements a second-price sealed auction correctly.

3

Anyone can add balance to any account /16/28

Phases of EVM ModelingPhase 1 single call—done
Phase 2 caller-callee interaction—in testing & debugging
Phase 3 follow the blockchain—not started

17/28

Phase 1: Take the Single Invocation’s View
Involves some artificial nondeterminism.

Untitled Page

Origin AccountContract Abyte seq
Etherstorage [ 50@0, 8@255, 4@25996 ]
...

CALL
...

programcounter[1]
storage [ (can be very different) ]Exported from Pencil ­ Fri Mar 31 2017 22:43:05 GMT+0200 (CEST) ­ Page 1 of 1

18/28

Special Treatment of CALL

During CALL instruction, nested calls can enter our program.
Our black box treatment of CALL during phase 1
I by default, the storage and the balance change arbitrarily

during a CALL.
I 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.

19/28

Outline

ProblemMotivation
EVM as a Machine
Wanted Properties
Current Efforts
Writing Specification
Testing the Specification
Proving Ethereum Contracts Correct
Outlook

20/28

Lem

I a specification language
I translates into HOL4, Isabelle/HOL, OCaml (and Coq)How I started using Lem
1. I started this project in 2015 in Coq.
2. I tried Isabelle/HOL and my proofs got shorter.
3. Sami Mäkelä saw this and started the Lem version.

21/28

Outline

ProblemMotivation
EVM as a Machine
Wanted Properties
Current Efforts
Writing Specification
Testing the Specification
Proving Ethereum Contracts Correct
Outlook22/28

OCaml for Testing

I Lem to OCaml extraction
I OCaml code to parse test cases (simplest “VMTest” format)

I Luckily, EVM has test suites
Ifor implementations in Python, Go, Rust, C++, . . . need tomatch exactly

I VM Test suite: 40,617 cases (24 cases skipped; they

involve multiple calls)
Need to run other formats.

23/28

Outline

ProblemMotivation
EVM as a Machine
Wanted Properties
Current Efforts
Writing Specification
Testing the Specification
Proving Ethereum Contracts Correct
Outlook24/28

Isabelle/HOL for Proving
Lem to Isabelle/HOL translation seems to be working.
As an off-the-shelf symbolic executor
Keeping the input x, without making it concrete.
Just watching the states evolve after each instruction.
Soon we see one stack element“¬ (the first four bytes of x == 0x44552211)”
Number & size of the cases explode.
One instruction takes 15 seconds for a realistic code.
Separation logic
Amani Sidney and Maksym Bortin ported a separation logic
library onto EVM.
Compositional reasoning.
25/28

Proving Theorems about Ethereum Programs inIsabelle/HOL

With symbolic execution
One theorem about a program (501 instructions) says:
I If the caller’s address is not at the storage index 1, the callcannot decrease the balance
I On the same condition, the call cannot change the storage

With separation logic
I deployed a proven wallet as a bounty program (since closed).

26/28

Way AheadOngoing
I testing the formalization of a whole transaction, containing

transactions containing calls
I verified compiler for a simple language (by Sami Mäkelä)

Not started
I implementing the next protocol change
I common Ethereum contract method/argument encoding
I connect to test/main network

A Competitor
I KEVM by Grigore Rosu and his team: EVM definition in

K-framework, gets some tools “for free”.
27/28

Summary
I We defined EVM for proof assistants Isabelle/HOL, Coqand HOL4I The EVM definition is usable for proving Ethereum

contracts against a specification
I We found mistakes in the LAT X spec while writing andE

testing our definition.
I Proof/tool/language/protocol developments in the proof

assistants welcome
https://github.com/pirapira/eth-isabelle(Apache License ver. 2 except material from Lem)

28/28