NOTE: This software is still in the early stages of development. If you are confused, find some bugs, or just want some help, please file an issue or come talk to us at https://dapphub.chat/channel/k-framework.
Klab is a tool for generating and debugging proofs in the K Framework, tailored for the formal verification of ethereum smart contracts. It includes a succinct specification language for expressing the behavior of ethereum contracts, and an interactive debugger.
Installing klab automatically installs
KEVM. You will therefore need the dependencies of K.
To install all of these dependencies on Ubuntu, try:
sudo apt-get install make gcc maven openjdk-8-jdk flex pkg-config libmpfr-dev autoconf libtool pandoc zlib1g-dev z3 libz3-dev npm parallel gnu-time jq
sudo pacman -S base-devel rsync opam pandoc jre8-openjdk mpfr maven z3 nodejs npm parallel
On OSX, using Homebrew, after installing the command line tools package:
brew tap homebrew/cask-versions brew cask install caskroom/versions/java8 brew install automake libtool gmp mpfr pkg-config pandoc maven opam z3 node gnu-getopt jq
This project uses the
GNU version of
gnu have a complicated relationship but you can run:
to make them get along.
Clone the repo and install the latest stable version
git clone --branch 0.3 https://github.com/dapphub/klab.git cd klab make deps
klab has some optional Haskell components, for which the recommended installation method is nix. If you have
nix, you can install the Haskell components with
To make klab available from the terminal, you can either just export the path to the
klab executable in
bin/, or use:
This installs symlinks globally at
/usr/local/libexec (will require
sudo on Linux machines). You can also specify a custom directory for installation by doing:
PREFIX=/path/to/custom/prefix make link
env will setup the environment for you if sourced from the root directory of the repo.
It sets three environment variables:
PATH: include the
KLAB_EVMS_PATH: the EVM semantics to use.
OPTIONAL: If you want to use a different version of K than what the KEVM ships with, you can set:
KLAB_K_PATH: override implementation of K.
OPTIONAL: You might also want to add the K tool binaries in
evm-semantics/.build/k/k-distribution/bin to your
$PATH, if you didn't already have K installed.
OPTIONAL: You can also use
nix-shell for a more deterministic environment experience. If you have
nix installed, run
nix-shell in this repo to start a deterministic shell environment.
To see how klab is used, we can explore the project in
config.json tells klab where to look for both the specification and the implementation of our contract. In this case, our specification lives in
src/, and our implementation lives in
Note that this example includes
dapp/out/SafeAdd.sol.json compiled from the solidity source. With solc installed, you can compile it yourself:
solc --combined-json=abi,bin,bin-runtime,srcmap,srcmap-runtime,ast dapp/src/SafeAdd.sol > dapp/out/SafeAdd.sol.json
Our goal is to prove that our implementation satisfies our specification. To do so, we'll start by building a set of K modules from our spec:
This will generate success and failure reachability rules for each
act of our specification. We can find the results in the
Now we're ready to prove each case, for example:
klab prove --dump SafeAdd_add_fail
--dump flag outputs a log to
out/data/<hash>.log, which will be needed later for interactive debugging. We can also do
klab prove-all to prove all outstanding claims.
Once the proof is complete, we can explore the generated symbolic execution trace using:
klab debug <hash>
Toggle different views by pressing any of the following keys:
t- display the (somewhat) pretty K term.
c- display current constraints.
b- display behavior tree.
s- diaplay source code.
e- display evm specific module.
m- display memory cell.
d- display debug cells (see toggling debug cells below).
r- display applied K rule.
z- display z3 feedback from attempted rule application.
Up/Dn- scroll view up and down.
n- step to next opcode
p- step to previous opcode
Shift+n- step to next k term
Shift+p- step to previous k term
Ctrl+n- step to next branch point
Ctrl+p- step to previous branch point
Toggling Debug Cells:
The following commands are prefixed with
: (and are typed at the bottom of the interface).
It's possible to toggle the debug cells view for specific cells, which prints out the JSON representation of the given cells.
Remember, you must turn on the debug cells view to see these (above).
:show ethereum.evm.callState.gas- show the contents of the
<gas>cell in the debug cells view.
:hide ethereum.evm.callStack.pc- hide the contents of the
<pc>cell in the debug cells view.
:omit gas pc- omit the contents of the
<pc>cells in the term view.
:unomit pc programBytes- unomit the contents of the
<programBytes>cells in the term view.
Available klab Commands
klab build- builds a set of K reachability claims in
out/specsbased on the spec, lemmas and source code as specified in the projects
klab prove <hash> [--dump]- executes a K reachability claim specified as a hash to the K prover. If the
--dumpflag is present, the proof can be explored using
klab prove-all- builds and executes all proof objects in the project directory.
klab debug <hash>- opens up the cli proof explorer of a particular proof execution. See key bindings above.
klab focus <hash>- focus on a hash, allowing you to leave out it as an argument to other commands.
klab hash- prints the hash of the focused proof
klab get-gas <hash>- Traverses the execution trace of a proof object to fetch its gas usage, put in
klab solve-gas <hash>- Constructs the gas condition necessary for an execution to succeed.
klab evm <hash>- Shows opcodes and source code side-by-side (useful for extracting pc values).
klab status <hash>- Shows whether a proof has been run, and whether it was accepted or rejected.
klab status-js <hash>- Shows the behaviour tree for an executed proof.
klab fetch <url>- Fetches the execution trace of a proof object at the url, preparing it for local debugging.
klab zip <hash>- zips up an execution trace so you can share it with a friend (or enemy).
klab storage <contractName>- Guesses what the storage layout of a given contract is
klab report- Generates a html report of the current project state in
klab help- Generates this view
There are automatic tab completions for
zsh that can be installed by adding the following to your
# completions for klab fpath=(~/dapphub/klab/resources/zsh $fpath) autoload -U compinit compinit
You might have problems due to an outdated
npm, in that case try updating it with:
npm install npm@latest -g npm install -g n n stable
KLab server requesting files at incorrect directory
What it looks like:
$ klab server 18.07.30 14-46-50: exec dfc688db4cc98b5de315bdfaa2512b84d14c3aaf3e58581ae728247097ff300d/run.sh 18.07.30 14-47-32: out Debugg: dfc688db4cc98b5de315bdfaa2512b84d14c3aaf3e58581ae728247097ff300d fs.js:119 throw err; ^ Error: ENOENT: no such file or directory, open '/tmp/klab/b042c99687ae5018744dc96107032b291e4a91f1ab38a6286b2aff9a78056665/abstract-semantics.k' at Object.openSync (fs.js:443:3) at Object.readFileSync (fs.js:348:35) at getFileExcerpt (/home/dev/src/klab/lib/rule.js:5:4) at Object.parseRule (/home/dev/src/klab/lib/rule.js:21:16) at Object.getblob (/home/dev/src/klab/lib/driver/dbDriver.js:49:19) at Object.next (/home/dev/src/klab/lib/driver/dbDriver.js:113:56) at Stream._n (/home/dev/src/klab/node_modules/xstream/index.js:797:18) at /home/dev/src/klab/node_modules/@cycle/run/lib/cjs/index.js:57:61 at process._tickCallback (internal/process/next_tick.js:61:11)  [dev@arch-ehildenb klab]% klab server fs.js:119 throw err;
Notice how it's requesting
abstract-semantics.k from proof-hash
b042... but we're actually running proof-hash
This is a problem with how K caches compiled definitions, and must be fixed upstream.
To fix this, run:
make clean && make deps
This will remove and recompile the KEVM semantics.
All contributions to this repository are licensed under AGPL-3.0. Authors:
- Denis Erfurt
- Martin Lundfall
- Everett Hildenbrandt
- Lev Livnev