search

dapphub / klab

K framework proof explorer & smart contract specification format
GNU Affero General Public License v3.0
123 stars 36 forks source link

readme

KLab

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.

Installation

Dependencies

See dependency installation instructions here

This project uses the GNU version of getopt and time. OSX and gnu have a complicated relationship but you can run:

export PATH=/usr/local/opt/gnu-getopt/bin:/usr/local/opt/gnu-time/libexec/gnubin:/usr/local/opt/coreutils/libexec/gnubin:$PATH

to make them get along.

Building

Clone the repo and install the latest stable version v0.4.0 with

git clone --branch v0.4.0 https://github.com/dapphub/klab.git
cd klab
make deps

OPTIONAL: 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

make deps-haskell

Environment Setup

To make klab available from the terminal, you can either just export the path to the klab executable in bin/, or use:

make link

This installs symlinks globally at /usr/local/bin and /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

The file env will setup the environment for you if sourced from the root directory of the repo.

source ./env

It sets three environment variables:

OPTIONAL: If you want to use a different version of K than what the KEVM ships with, you can set:

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.

Usage

To see how klab is used, we can explore the project in examples/SafeAdd:

cd examples/SafeAdd/

Specification

The file 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 dapp/.

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

Proof

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:

klab build

This will generate success and failure reachability rules for each act of our specification. We can find the results in the out/specs directory.

Now we're ready to prove each case, for example:

klab prove --dump SafeAdd_add_fail

The --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>

Embedded rules

klab comes with a set of pre-defined K rewrite rules, additional to the ones defined in evm-semantics. They are located in resources/rules.k.tmpl.

Key Bindings

Toggle different views by pressing any of the following keys:

View Commands:

Navigation Commands:

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).

Available klab Commands

Configuration

The config.json file is used to configure klab.

Here's an example:

{
  "name": "k-dss",
  "url": "https://github.com/dapphub/k-dss",
  "src": {
    "specification": "./src/dss.md",
    "smt_prelude": "./src/prelude.smt2.md",
    "rules": [
      "./src/storage.k.md",
      "./src/lemmas.k.md"
    ],
    "dirty_rules": [
      "./src/dirty_lemmas.k.md"
    ]
  },
  "implementations": {
    "Vat": {
      "src": "src/vat.sol"
    },
    "Vow": {
      "src": "src/vow.sol"
    },
  },
  "timeouts": {
    "Vat_grab_pass_rough": "16h",
  },
  "memory" : {
    "Vat_frob-diff-nonzero_fail_rough": "25G",
  },
  "dapp_root": "./dss",
  "solc_output_path": "out/dapp.sol.json",
  "host": "127.0.0.1:8080"
}

Limits

Time

By default, klab-prove sets a timeout of 1 day. This can be changed by passing the --timeout flag a value of the format [0-9]+[dhms].

klab-prove-all defaults to a per-proof timeout of 200m. This can be changed by setting timeouts to a different value in config.json, as shown above.

Memory

By default, both klab-prove and klab-prove-all run the JVM with a maximum heap size of 10GB.

This can be changed by setting the K_OPTS environment variable to something like --Xmx4G. Refer to the JVM docs for more information.

klab-prove-all also reads the config.json file, and the maximum heap size can be changed with the memory key, as shown above.

Gas

In rough specs, the amount of gas available defaults to 3,000,000. This can be changed using the gas header.

Once a pass_rough spec has been proven, the gas used for each execution path is combined into a single expression, which is the upper gas bound for the stronger pass spec.

Zsh completions

There are automatic tab completions for zsh that can be installed by adding the following to your .zshrc:

# completions for klab
fpath=(~/dapphub/klab/resources/zsh $fpath)
autoload -U compinit
compinit

Troubleshooting

Outdated npm

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)
[1] [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 dfc6.... 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.

License

All contributions to this repository are licensed under AGPL-3.0. Authors: