The artifact consist of:
wanilla-artifacts-docker-container.tar.gz: a Docker container including:wanilla, an executable prototype of the approach described in the paper "Wanilla: Sound Noninterference Analysis for WebAssembly"wanilla/src/test/resources/wien/secpriv/wasm/NoninterferenceTests/json_structure and wanilla/src/test/resources/wien/secpriv/wasm/NoninterferenceTests/)asmt, an experimental solver for a subset of the CHC fragment of SMT-LIB that canwanilla-artifact-sources.zip: scripts and sources for building the Docker container in a reproducible fashionsmt-lib-files.zip: the SMT-LIB files (as they can take a long time to generate and can be affected by a bug in the shipped version of z3 that manifests itself depending on the query order, which in our software is nondeterministic)Furthermore, we packaged the tools we benchmarked against in executable form:
wassail [3] with minor bugfixes and patches that hard-code security policies for our benchmarkrapid with minor patches to compile it with modern compilersvampire in the particular configuration it was used in the RAPID [1] paperAll code was tested on Linux (Kernel 6.1.69, x86_64), but the code should potentially run on macOS or Linux with a different processor architecture.
If you want to recreate the container (possibly with modifications), continue reading this section.
If you want to just reproduce the results, continue at "Reproducing the Results"
We use nix (version 2.28.4) to build the Docker container (as well as all tools separately) to circumvent the reproducibility issues of Docker files.
If you have Docker installed and do not want to install nix, skip to the "Building with Docker" section.
cd wanilla-artifact-sources
nix build .#docker-image
This builds the Docker container, which is stored in a newly created symlink ./result (which points to somewhere in /nix/store/).
The constituent components of the benchmark (asmt, rapid, vampire, wanilla, wassail) are also available as outputs and available to nix.
To enter, e.g. a shell with asmt and wanilla available, execute:
nix shell .#asmt .#wanilla
Instead of installing nix, you can use an (ephemeral) Docker container to build the Docker container containing our artifact.
To do that, execute:
cd wanilla-artifact-sources
docker run -v $PWD:/mnt --rm -ti nixos/nix:2.28.4 sh -c 'cd /mnt && nix --extra-experimental-features nix-command --extra-experimental-features flakes build .#docker-image && cp result wanilla-artifacts-docker-container.tar.gz'`
This will result in the Docker container wanilla-artifacts-docker-container.tar.gz being stored in the current working directory (possibly, you will have to adjust ownership/permissions on this file).
First, load the Docker container:
docker load -i wanilla-artifacts-docker-container.tar.gz
Then enter the container via
docker run -v $PWD:/mnt --rm -ti wanilla-artifacts bash
Replace $PWD with a different path if you want the working directory of the Docker container.
All commands in the following are assumed to be executed in the Docker container.
The wanilla tool can be used to turn a specification (a special .json file that is placed next to a .wasm file with the same name (modulo prefix)) into a set of SMT-LIB files.
The specifications for the EOSFuzzer [2] benchmark are stored in /data/benchmarks/eosfuzzer-specs-for-wanilla/.
echo source atom | tr ' ' '\n' | xargs -I{} wanilla --smt-out-dir smt-out/eosfuzzer/{} --test-in-dir /data/benchmarks/eosfuzzer-specs-for-wanilla/{} --parallelize
The files will be stored in smt-out/eosfuzzer/source and smt-out/eosfuzzer/atom.
To analyze a file x.smt with asmt, just call asmt < x.smt
A result containing a satisfiable query, such as
asmt < smt-out/eosfuzzer/source/eosfun-0.smt
testNoninterferenceResultUnsat_30_0:unsat
testNoninterferenceImportedFunctionParamsUnsat_5_0:sat
testNoninterferenceImportedFunctionContextUnsat_5_0:sat
indicates that the tool has found an interference (which may be a false positive); if all queries are unsatisfiable, the analysed function is surely noninterferent.
To find all SMT-LIB files indicating a potential interference, execute:
ls smt-out/eosfuzzer/*/*smt | xargs -P16 -I{} sh -c 'asmt < {} | grep --quiet :sat && echo {}'
We provide a version of wassail that has been patched to deem the relevant functions in the EOSFuzzer benchmark as sources/sinks for potential flows. Additionally, we provide a script (run_wassail.py) that parses wassail's output for our purposes.o To analyze a WebAssembly module x.wasm, execute run_wassail.py whole-analysis x.wasm.
To analyze all modules in the EOSFuzzer benchmark, execute:
ls /data/benchmarks/eosfuzzer-specs-for-wanilla/*/*.wasm | xargs -P16 -I{} run-wassail.py whole-analysis {}
(Running this command also produces a bunch of .dot files that we do not need for our analysis.)
Generate the SMT-LIB files like this:
ls /data/benchmarks/rapid-specs-for-rapid/ | xargs -I{} mkdir -p smt-out-rapid/{}
ls /data/benchmarks/rapid-specs-for-rapid/ | xargs -I{} rapid -dir smt-out-rapid/{}/ /data/benchmarks/rapid-specs-for-rapid/{}
The relevant files have the prefixe user-conjecture- and a file x.smt can be analyzed with
vampire --input_syntax smtlib2 -tha on -av on x.smt
Note that -tha and -av can also be set to off (we tried all combinations where not able to get all examples to terminate).
Generate the SMT-LIB files:
wanilla --smt-out-dir smt-out/rapid/ --test-in-dir /data/benchmarks/rapid-specs-for-wanilla --parallelize
Solve them with z3:
mkdir -p /tmp/z3out/smt-out/rapid
ls smt-out/rapid/* | xargs -I{} -P16 sh -c 'z3 {} > /tmp/z3out/{}'
The z3 output only contains the result of the queries without their names.
To align the queries with the results, you can use:
ls smt-out/rapid/* | xargs -I{} sh -c 'paste <(grep query {}) /tmp/z3out/{}'
The expected result of the query is encoded in its name, to check the if the result is correct you can run:
ls smt-out/rapid/* | xargs -I{} sh -c 'paste <(grep query {} | grep -oE "Unsat|Sat") /tmp/z3out/{}'
To get a count of how many queries are handled imprecisely by asmt, run:
ls smt-out/rapid/* | xargs -I{} sh -c 'asmt < {}' | grep -c 'Unsat.*:sat'
To get a count of how many test cases have it least one imprecise query, run:
ls smt-out/rapid/* | xargs -I{} sh -c 'asmt < {} | grep --quiet "Unsat.*:sat" && echo {}' | wc -l
The Wanilla benchmarks are generated exactly as the RAPID benchmarks:
ls /data/benchmarks/wanilla | xargs -I{} wanilla --smt-out-dir smt-out/wanilla/{} --test-in-dir /data/benchmarks/wanilla/{} --parallelize
mkdir -p /tmp/z3out/smt-out/wanilla/{basic,complex,zzz_from_others/,integrity,figures,examples}
ls smt-out/wanilla/*/* | xargs -I{} -P16 sh -c 'z3 {} > /tmp/z3out/{}'
ls smt-out/wanilla/*/* | xargs -I{} sh -c 'paste <(grep query {} | grep -oE "Unsat|Sat") /tmp/z3out/{} <(echo {})'
ls smt-out/wanilla/*/* | xargs -I{} sh -c 'paste <(grep query {} | grep -oE "Unsat|Sat") /tmp/z3out/{}' | sort -u
ls smt-out/wanilla/*/* | xargs -I{} sh -c 'asmt < {}' | grep -c 'Unsat.*:sat'
ls smt-out/wanilla/*/* | xargs -I{} sh -c 'asmt < {} | grep --quiet "Unsat.*:sat" && echo {}' | wc -l
We included a tool that uses wassail to output the statistics of the benchmarks stored in a directory. Use the tool as follows:
stats.py /data/benchmarks/wanilla/
stats.py /data/benchmarks/rapid-specs-for-wanilla/
stats.py /data/benchmarks/eosfuzzer-specs-for-wanilla/
[1] G. Barthe, R. Eilers, P. Georgiou, B. Gleiss, L. Kovács, and M. Maffei. Verifying Relational Properties using Trace Logic. In Formal Methods in Computer Aided Design (FMCAD). IEEE, 2019. [2] Y. Huang, B. Jiang, and W. K. Chan. Eosfuzzer: Fuzzing EOSIO smart contracts for vulnerability detection. In Internetware’20: 12th Asia-Pacific Symposium on Internetware, Singapore, November 1-3, 2020, pages 99–109. ACM, 2020. [3] Q. Stiévenart and C. De Roover. Compositional Information Flow Analysis for WebAssembly Programs. In International Working Conference on Source Code Analysis and Manipulation (SCAM). IEEE, 2020.