# Supplementary Material for Wappler

### Needed Software

Wappler is distributed either as source or as docker container, both available under http://secpriv.wien/wappler.

The docker container contains all dependencies of wappler, if you build the sources via `nix` all dependencies will automatically be installed.

You can enter a shell where `wappler` is available by executing `nix shell .#wappler`.
In the following, we will assume that `wappler` is available (e.g. by having executed `nix shell .#wappler`). 

`nix` can also be used to run `wappler` without entering a shell.
For this, `wappler` has to be replaced by `nix run .#wappler --`.
To run the commands with `docker`, replace `wappler` with `docker run --rm -i -v "$(pwd)":/mnt/ wappler:11112222aaaabbbbccccddddeeeeffff wappler`, where `wappler:11112222aaaabbbbccccddddeeeeffff` is the id of the `wappler` image (the output of `docker load -i wappler-image.tar.gz`).
Also note, that if you want to access files that are not in the current directory (or a subdirectory thereof) you have to adjust the `-v` argument.

Finally, you can also execute the `jar` file directly.
To find out where the `jar` file is stored, execute `nix build .#wappler; readlink -f ./result/lib/wappler.jar`
To run the command via `java`, replace `wappler` with `java -cp <path-to-jar>`.

To prepare the experiments, you need

* `wabt` (to compile wat/wast files to wasm) 
* `curl`, `tar`, `find`, `grep` (helpers for tests), and
* `python`

### Wasm Specification Tests

```shell
# make sure you have wabt available (skip if you have installed it by other means)
nix shell .#wabt
# download official test files from correct 
curl https://codeload.github.com/WebAssembly/spec/tar.gz/f2b62c3067ac7e9e367296378621ccbd4fee79c1 | tar -xz --strip=2 spec-f2b62c3067ac7e9e367296378621ccbd4fee79c1/test/core

# extract individual modules
mkdir out
./scripts/extract-modules.py core/*.wast

# move modules with unsupported features out of the way 
mkdir out/unsupported
cd out
mv -i imports-00{2,3}.* elem-00{2,3,4,5}.* exports-* linking-* start-* unsupported/

# compile wat files to wat
find -maxdepth 1 -iname '*.wat' -exec wat2wasm '{}' ';'

cd ..

# run tests in out/loop-000.spec on module out/loop-000.wasm with 10 seconds z3 timeout 
wappler wien.secpriv.wasm.WasmSpecRunner --spec-in-dir=out --prune-strategy=aggressive --predicate-inlining-strategy=linear --z3-query-timeout 10000 loop-000

# run tests in out/align-000.spec on module out/align-000.wasm with 30 seconds z3 timeout, where the different test cases are assumed not to influence each other
wappler wien.secpriv.wasm.WasmSpecRunner --spec-in-dir out --prune-strategy=aggressive --predicate-inlining-strategy=linear --z3-query-timeout 30000 --execute-independent align-000

# create output directory for smt files 
mkdir -p smt-out/wasm-spec/

# generate smt files without executing z3
wappler wien.secpriv.wasm.WasmSpecRunner --spec-in-dir out --prune-strategy=aggressive --predicate-inlining-strategy=linear --no-output-query-results --smt-out-dir smt-out/wasm-spec loop-000
```

### Examples from Case Study

```shell
# make sure you have z3 available (skip if you have installed it by other means)
nix shell .#z3
# run vulnerable versions of tests
wappler wien.secpriv.wasm.ReachabilityMain --spec-in-dir files/reachability-spec --prune-strategy=aggressive --predicate-inlining-strategy=linear fig1 fig4

# run secured versions of 
wappler wien.secpriv.wasm.ReachabilityMain --spec-in-dir files/reachability-spec --prune-strategy=aggressive --predicate-inlining-strategy=linear fig1-secure fig4-secure

# find problematic return values for fig 1
## create output directory
mkdir -p smt-out/reachability-spec
## create smt output (no inlining/pruning to preserve the structure of the program)
wappler wien.secpriv.wasm.ReachabilityMain --spec-in-dir files/reachability-spec --no-output-query-results --smt-out-dir smt-out/reachability-spec fig1
## find out program counter of call_indirect (call_indirect happens at pc 2 of function 0, meaning that the return value will be on the top of the stack at pc 3)
grep -A19 callIndirectOverapproximated smt-out/reachability-spec/fig1.wasm.smt-testDontReturnNegative_0.smt
## look at concrete value for corresponding predicate in z3 model
z3 fp.print-answer=true fp.xform.inline_linear=false fp.xform.inline_eager=false smt-out/reachability-spec/fig1.wasm.smt-testDontReturnNegative_0.smt | grep -A1 MState_0_3
## the problematic return value is #x0000000080000000
```