Skip to content

Commit bb75ac3

Browse files
ehildenbehildenb
authored
Trufflecon - Presentations and demo files added (#425)
* Makefile: target test-proof => test-prove * Makefile, media/201905-exercise-k-workshop: add EthNYC Workshop * media/201905-exercise-k-workshop: flesh out rest of presentation * media/201905-exercise-k-workshop: updates * media/201905-exercise-k-workshop: final updates * Makefile, media/201908-trufflecon-workshop: add initial trufflecon presentation * .gitignore: ignore generated pdfs * media/201908-trufflecon: shorten and simplify for trufflecon * media/201908-trufflecon: more updates to presentation * media/201908-trufflecon: update instructions for KLab * Makefile, media/201908-trufflecon-firefly: firefly presentation/demo slides * media/images/k-overview: updated image * add-spec: add relevant file * media/201908-trufflecon-workshop: update instructions * add-*-spec.k: more specs * kevm-ltl: add LTL example * addition: add example addition program * kevm, kevm-ltl, addition.evm: LTL instrumentation * kevm: remove ltl command * media/201908-trufflecon-workshop: update slides * media/201908-trufflecon-workshop: Update title * media/201808-trufflecon-workshop: update presentation with docker instructions * media/201908-trufflecon: add proxy dockerhub account * media/201908-trufflecon-workshop: update instructions * kevm-ltl, addition: labeled event sets in trace * media/201908-trufflecon-firefly: update presentation * kevm-ltl: event collection done as a monitor too * media/201908-trufflecon-firefly: updated demo slides * kevm-ltl: add invalid event * kevm-ltl: manually set exit code to 0 * kevm: allow overriding KEVM_DEFN_DIR * * => media/201908-trufflecon: move files to subdirectory * media/201908-trufflecon: update documentation * media/201908-trufflecon: update documentation * Jenkinsfile: test-proof => test-prove * README: fix path .build/k => deps/k
1 parent 31446e7 commit bb75ac3

File tree

14 files changed

+744
-7
lines changed

14 files changed

+744
-7
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,3 +4,4 @@
44
/src
55
/package/pkg
66
/package/src
7+
/media/*.pdf

‎Jenkinsfile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ pipeline {
7373
sh '''
7474
nprocs=$(nproc)
7575
[ "$nprocs" -gt '6' ] && nprocs='6'
76-
make test-proof -j"$nprocs"
76+
make test-prove -j"$nprocs"
7777
'''
7878
}
7979
}

‎Makefile‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ export LUA_PATH
4040
defn java-defn ocaml-defn node-defn haskell-defn llvm-defn \
4141
test test-all test-conformance test-slow-conformance test-all-conformance \
4242
test-vm test-slow-vm test-all-vm test-bchain test-slow-bchain test-all-bchain \
43-
test-proof test-klab-prove test-parse test-failure \
43+
test-prove test-klab-prove test-parse test-failure \
4444
test-interactive test-interactive-help test-interactive-run test-interactive-prove test-interactive-search test-interactive-firefly \
4545
media media-pdf sphinx metropolis-theme
4646
.SECONDARY:
@@ -448,7 +448,7 @@ test-bchain: $(quick_bchain_tests:=.run)
448448
proof_specs_dir:=tests/specs
449449
proof_tests=$(wildcard $(proof_specs_dir)/*/*-spec.k)
450450

451-
test-proof: $(proof_tests:=.prove)
451+
test-prove: $(test_prove_specs:=.prove)
452452
test-klab-prove: $(smoke_tests_prove:=.klab-prove)
453453

454454
# Parse Tests
@@ -497,7 +497,10 @@ media: sphinx media-pdf
497497

498498
### Media generated PDFs
499499

500-
media_pdfs:=201710-presentation-devcon3 201801-presentation-csf
500+
media_pdfs := 201710-presentation-devcon3 \
501+
201801-presentation-csf \
502+
201905-exercise-k-workshop \
503+
201908-trufflecon-workshop 201908-trufflecon-firefly
501504

502505
media/%.pdf: media/%.md media/citations.md
503506
@echo "== media: $@"

‎README.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ git submodule update --init --recursive
9898
If you haven't already setup K's OCaml dependencies more recently than February 1, 2019, then you also need to setup the K OCaml dependencies:
9999

100100
```sh
101-
./.build/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev
101+
./deps/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev
102102
```
103103

104104
Finally, you can install repository specific dependencies and build the semantics:
@@ -146,7 +146,7 @@ On Arch, you'll also need `crypto++` package.
146146
And you need to setup Rust:
147147

148148
```sh
149-
.build/k/llvm-backend/src/main/native/llvm-backend/install-rust
149+
./deps/k/llvm-backend/src/main/native/llvm-backend/install-rust
150150
```
151151

152152
Additionally, you need to setup the remaining LLVM dependencies.

‎kevm‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ shopt -s extglob
55

66
kevm_dir="${KEVM_DIR:-.}"
77
build_dir="$kevm_dir/.build"
8-
defn_dir="$build_dir/defn"
8+
defn_dir="${KEVM_DEFN_DIR:-$build_dir/defn}"
99
lib_dir="$build_dir/local/lib"
1010
k_release_dir="${K_RELEASE:-$kevm_dir/deps/k/k-distribution/target/release/k}"
1111

‎media/201905-exercise-k-workshop.md‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
---
2+
title: 'K Workshop'
3+
subtitle: 'Understanding the K Prover'
4+
author:
5+
- Everett Hildenbrandt
6+
institute:
7+
- Runtime Verification
8+
- ConsenSys
9+
date: '\today'
10+
theme: metropolis
11+
fontsize: 8pt
12+
---
13+
14+
Overview
15+
--------
16+
17+
- Install KEVM and KLab on your machine
18+
- Simple uses of the `./kevm` script
19+
- (Brief) introduction to KEVM
20+
- Verification examples: KEVM lemma proofs, ERC20 `transfer` function
21+
- Open verification challenge
22+
23+
Install KEVM
24+
------------
25+
26+
### KEVM
27+
28+
- Branch `kevm-lemmas` of KEVM: <https://github.com/kframework/evm-semantics>
29+
- Build instructions in README.
30+
31+
```sh
32+
make deps
33+
make build-java
34+
make build-ocaml
35+
```
36+
37+
- Should be able to run:
38+
39+
```sh
40+
make test-prove-verified
41+
make test-prove-gen -j3
42+
```
43+
44+
. . .
45+
46+
### KLab
47+
48+
- Branch `master` of KLab: <https://github.com/dapphub/klab>
49+
- Build instructions in README.
50+
51+
```sh
52+
make deps-npm
53+
```
54+
55+
- Should be able to run (in KEVM repo with `klab/bin` on your `PATH`):
56+
57+
```sh
58+
make tests/specs/verified/kevm-lemmas-spec.k
59+
./kevm klab-prove tests/specs/verified/kevm-lemmas-spec.k --boundary-cells k,pc
60+
```
61+
62+
`./kevm help`
63+
-------------
64+
65+
```sh
66+
$ ./kevm help
67+
68+
usage: ./kevm (run|kast) [--backend (ocaml|java|llvm|haskell)] <pgm> <K args>*
69+
./kevm interpret [--backend (ocaml|llvm)] <pgm>
70+
./kevm prove [--backend (java|haskell)] <spec> <K args>*
71+
./kevm klab-(run|prove) <spec> <K args>*
72+
73+
./kevm run : Run a single EVM program
74+
./kevm interpret : Run JSON EVM programs without K Frontend (external parser)
75+
./kevm prove : Run an EVM K proof
76+
./kevm klab-(run|prove) : Run or prove a spec and launch KLab on the execution graph.
77+
78+
Note: <pgm> is a path to a file containing an EVM program/test.
79+
<spec> is a K specification to be proved.
80+
<K args> are any arguments you want to pass to K when executing/proving.
81+
82+
KLab: Make sure that the 'klab/bin' directory is on your PATH to use this option.
83+
```
84+
85+
`./kevm` examples
86+
-----------------
87+
88+
> - Run a test: `MODE=... SCHEDULE=... ./kevm run tests/etheremu-tests/...`
89+
> - Interpret a test (fast): `MODE=... SCHEDULE=... ./kevm interpret tests/etheremu-tests/...`
90+
> - Run a proof: `./kevm prove tests/specs/*-spec.k`
91+
> - Run a test under KLab: `MODE=... SCHEDULE=... ./kevm klab-run tests/ethereum-tests/...`
92+
> - Run a proof under KLab: `./kevm klab-prove tests/ethereum-tests/...`
93+
94+
Introduction to KEVM
95+
--------------------
96+
97+
- File [data.md](../data.md) defines data-structures of EVM.
98+
- File [evm.md](../evm.md) defines the semantics itself.
99+
- File [driver.md](../driver.md) defines the testing harness.
100+
- File [edsl.md](../edsl.md) defines a DSL for aiding specification for proofs.
101+
102+
Verification Examples
103+
---------------------
104+
105+
### KEVM Lemmas
106+
107+
- File [kevm-lemmas-spec.md](../kevm-lemmas-spec.k)
108+
- Summaries of the "positive" cases of arithmetic opcodes and push
109+
- Work through how to use KLab to discover preconditions
110+
- Complete the push, push, add specification
111+
112+
```sh
113+
make test-prove-verified
114+
```
115+
116+
. . .
117+
118+
### ERC20 `transfer` functions
119+
120+
- Run proof.
121+
122+
```sh
123+
make test-prove-gen
124+
```
125+
126+
- Explain ini file format of [ds-token-erc20-spec.ini](../tests/specs/ds-token-erc20/ds-token-erc20-spec.ini)
127+
- Delete all except the `transfer` blocks
128+
- Remove `requires` clauses to explore result in KLab
129+
130+
Open Verification Challenge
131+
---------------------------
132+
133+
Rest of time.
134+
135+
- Work on `transferFrom` function?
136+
- Try to setup your own contract?
137+
138+
Thanks!
139+
-------
140+
141+
- ConsenSys for hosting us!
142+
- You all for attending!

‎media/201908-trufflecon-firefly.md‎

Lines changed: 180 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
---
2+
title: 'Firefly'
3+
subtitle: 'Solidity testing using KEVM'
4+
author:
5+
- Everett Hildenbrandt
6+
- Grigore Rosu
7+
institute:
8+
- Runtime Verification
9+
date: '\today'
10+
theme: metropolis
11+
fontsize: 8pt
12+
---
13+
14+
Overview
15+
--------
16+
17+
- (Brief) Introduction to KEVM
18+
- Introduction to Firefly
19+
- Firefly Demo
20+
- Future Directions
21+
22+
(Brief) Introduction to KEVM
23+
----------------------------
24+
25+
- Repository: <https://github.com/kframework/evm-semantics>
26+
- Considered the canonical spec of EVM: <https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389>
27+
- All K tooling is derived automatically:
28+
- Reference EVM interpreter
29+
- Symbolic execution engine
30+
- EVM bytecode formal verification engine
31+
- Several EVM bytecode debugger options
32+
33+
Introduction to Firefly
34+
-----------------------
35+
36+
- `npm` package here: <https://www.npmjs.com/package/kevm-ganache-cli>.
37+
- Drop-in replacement for `ganache-cli`, can be used directly by Truffle.
38+
39+
Instead of:
40+
41+
```sh
42+
npx ganache-cli
43+
```
44+
45+
run:
46+
47+
```sh
48+
npx kevm-ganache-cli
49+
```
50+
51+
. . .
52+
53+
### Why??
54+
55+
- Higher confidence in results (run tests with both!).
56+
- More features to come:
57+
- Test coverage metrics.
58+
- Automated property verification.
59+
- Test generation.
60+
- Contract symbolic execution.
61+
- ... your ideas??
62+
63+
Firefly Demo - Setup
64+
--------------------
65+
66+
Instructions from <https://www.npmjs.com/package/kevm-ganache-cli>:
67+
68+
. . .
69+
70+
### Install KEVM (once)
71+
72+
**TODO**: Update release URL.
73+
74+
```sh
75+
sudo apt install nodejs npm curl git
76+
curl --location 'https://github.com/kframework/evm-semantics/releases/download/v1.0.0-a47e4b2/kevm_1.0.0_amd64.deb' \
77+
--output kevm_1.0.0_amd64.deb
78+
sudo apt install ./kevm_1.0.0_amd64.deb
79+
```
80+
81+
. . .
82+
83+
### Install `npx` (once)
84+
85+
```sh
86+
sudo npm install -g npx
87+
```
88+
89+
Firefly Demo - Run OpenZeppelin Tests
90+
-------------------------------------
91+
92+
### Start `kevm-ganache-cli`
93+
94+
```sh
95+
npx kevm-ganache-cli \
96+
--gasLimit 0xfffffffffff \
97+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501200,1000000000000000000000000" \
98+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501201,1000000000000000000000000" \
99+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501202,1000000000000000000000000" \
100+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501203,1000000000000000000000000" \
101+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501204,1000000000000000000000000" \
102+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501205,1000000000000000000000000" \
103+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501206,1000000000000000000000000" \
104+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501207,1000000000000000000000000" \
105+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501208,1000000000000000000000000" \
106+
--account="0x2bdd21761a483f71054e14f5b827213567971c676928d9a1808cbfa4b7501209,1000000000000000000000000"
107+
```
108+
109+
. . .
110+
111+
### Run OpenZeppelin tests
112+
113+
```sh
114+
git clone 'https://github.com/OpenZeppelin/openzeppelin-contracts.git'
115+
cd openzeppelin-contracts
116+
git checkout b8c8308
117+
npm install
118+
npx truffle test test/token/ERC20/ERC20.test.js
119+
```
120+
121+
KEVM Extensions - Event Monitoring
122+
----------------------------------
123+
124+
Compile semantics with additional file `media/201908-trufflecon/kevm-ltl.md`.
125+
126+
```k
127+
syntax LTLEvent ::= "overflow"
128+
// ------------------------------
129+
rule <k> ADD W0 W1 ... </k>
130+
<events> EVENTS (.Set => SetItem(overflow)) </events>
131+
requires notBool overflow in EVENTS
132+
andBool W0 +Word W1 =/=Int W0 +Int W1
133+
[priority(24)]
134+
135+
syntax LTLEvent ::= "revert"
136+
// ----------------------------
137+
rule <k> REVERT _ _ ... </k>
138+
<events> EVENTS (.Set => SetItem(revert)) </events>
139+
requires notBool revert in EVENTS
140+
[priority(24)]
141+
```
142+
143+
- Monitors built-in to the KEVM semantics as an extension.
144+
- Can build arbitrary LTL formula over the monitors.
145+
146+
KEVM Extensions - LTL Model Checking
147+
------------------------------------
148+
149+
### Input file `addition.evm`
150+
151+
```evm
152+
load { "gas" : 10000000
153+
// Query: always ((~ overflow) \/ eventually revert)
154+
// , "code" : UNSAFEADD(100 , 100) // True
155+
// , "code" : UNSAFEADD(maxUInt256 , 100) // False
156+
// , "code" : SAFEADD(100 , 100) // True
157+
, "code" : SAFEADD(maxUInt256 , 100) // True
158+
}
159+
160+
start
161+
```
162+
163+
. . .
164+
165+
### Query
166+
167+
```sh
168+
./kevm run --backend llvm media/201908-trufflecon/addition.evm -cLTLFORMULA='always (overflow -> eventually revert)'
169+
```
170+
171+
Truffle Firefly Plugin
172+
----------------------
173+
174+
- Developed with help from Truffle devs today as plugin!
175+
- Modified OpenZeppelin test-suite which links to `truffle-plugin-firefly`.
176+
177+
```sh
178+
npx truffle run firefly SafeMath 'always (overflow -> eventually revert)'
179+
```
180+

0 commit comments

Comments
 (0)