Wanilla: Sound Noninterference Analysis for WebAssembly (artifacts)

This dataset contains the software and benchmarks accompanying the paper "Wanilla: Sound Noninterference Analysis for WebAssembly" (to be published at the ACM Conference on Computer and Communications Security (CCS) 2025). Additionally, we provided build instructions for the tools we compare against (RAPID [1], wassail [3]) and the benchmarks used (RAPID [1], EOSFuzzer [2]) in the form of a nix flake.

wanilla-artifact-sources.zip contains the sources for our prototype noninterference analyzer Wanilla (./wanilla) and its dependencies (./horst, ./wparser). It furthermore contains the code of our prototype abstract interpretation for constrained Horn clause programs (./asmt). The build instructions and patches for the software we compare with (RAPID, wassail) are stored in the respective subdirectories (./rapid, ./wassail). The scripts to filter out trivial examples and generate test specifications from the EOSFuzzer benchmark are stored in ./eosfuzzer-benchmark-data, while the code used in the figures of the paper (including the test specifications) is stored in ./figures-benchmark-data. stats.py is a script to calculate statistics on the benchmark. The flake files (flake.nix, flake.lock) contain code to build the different components separately or 
bundle them in a Docker container. README.md contains exact build/reproduction instructions.

wanilla-artifacts-docker-container.tar.gz is a Docker container image that realizes the sources in wanilla-artifact-sources.zip. It contains all executables (in the versions we evaluated, with our patches applied) and all benchmark data in a form that Wanilla can understand.

smt-lib-files.zip contains the outputs of Wanilla when applied to the benchmark inputs (our own benchmarks + the EOSFuzzer benchmark + the RAPID benchmarks) as constrained Horn clause programs (in the z3 dialect of SMT-LIB). The outputs are supplied for convenience (as the files can take some time to generate) and because Wanilla has some nondeterminism in its output, which (while producing semantically equivalent programs) can impact solver performance.

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