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), andpython# 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
# 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