Awesome
Formalization of Ethereum Virtual Machine in Lem
This repository contains
- an EVM implementation in Lem
lem/evm.lem
- a Keccak-256 implementation in Lem
lem/keccak.lem
- a form of functional correctness defined in Lem
lem/evmNonExec.lem
- a relational semantics that captures the environment's nondeterministic behavior
RelationalSem.thy
- some example verified contracts in
example
- a parser that parses hex code and emits an Isabelle/HOL expression representing the program
parser/hexparser.rb
When you see \<Rightarrow>
in the source, try using the Isabelle2017 interface. There you see ⇒
instead.
Lem?
Lem is a language that can be translated into Coq, Isabelle/HOL, HOL4, OCaml, HTML and LaTeX.
Prerequisites
- Isabelle2017
- lem
- OCaml 4.02.3
- opam 1.2.2
- Some opam packages: use
opam install ocamlfind batteries yojson bignum easy-format bisect_ppx ocamlbuild sha secp256k1
- ECC-OCaml from mrsmkl
- secp256k1
- On Ubuntu Artful,
apt install secp256k1-0 secp256k1-dev
is enough - On older versions of Ubuntu, installation from the current
master
branch is necessary - configure option
--enable-module-recovery
is needed
- On Ubuntu Artful,
How to read the proofs
First translate the Lem definitions into Isabelle/HOL:
$ make lem-thy
Then, use Isabelle2017 to open ./examples/AlwaysFail.thy
. The prerequisite Isabelle/HOL files are automatically opened.
How to run VM tests and state tests
Make sure the tests submodule is cloned
$ git submodule init tests
$ git submodule update tests
Extract the OCaml definitions
$ make lem-ocaml
And move to tester
directory.
$ cd tester
One way is to run the VM Test.
$ sh compile.sh
$ ./runVmTest.native
(When ./runVmTest.native
takes an argument, it executes only the test cases whose names contain the argument as a substring.)
Another way is to run the VM Test and measure the coverage.
$ sh measure_coverage.sh
Moreover, it's possible to run Blockchain Tests.
$ ./runBlockchainTest.native
Makefile goals
make doc
producesoutput/document.pdf
as well aslem/*.pdf
.make lem-thy
compiles the Lem sources into Isabelle/HOLmake lem-hol
compiles the Lem sources into HOL4make lem-coq; cd lem; make
compiles the Lem sources into Coq (and then compiles the Coq sources)make lem-pdf
compiles some of the Lem sources into PDF through LaTeXmake all-isabelle
checks all Isabelle/HOL sources (but not the ones compiled from Lem)make
does everything abovescript/gen_coq.sh
generates a distribution useful for Coq users
Links
- For a bigger picture, see overview of Yoichi's formal verification efforts on smart contracts
- For updates, visit a gitter channel
- A related project EVM formalization in K framework