Swoosh

Swoosh is a verification pipeline for proving constant-time security properties of C programs. It translates C code through SMACK into Boogie IVL, then performs abductive verification using cvc5 to prove that programs don't leak secrets through timing side channels.

Architecture

C source → SMACK → Boogie (.bpl) → Compile → Interpret → Verify (abduction)

Component	Path	Runtime	Purpose
Parser	parser/, boogie.lark	PyPy	Lark LALR parser for Boogie IVL
Compiler	passes/, tools/compile.py	PyPy	Shadowing, inlining, CFG construction
Interpreter	interpreter.py, interpreter/	PyPy	Concrete execution for positive examples
Verifier	passes/abduction.py, tools/driver.py	Python 3	Abductive verification via Ray + Redis + cvc5

Prerequisites

• Ubuntu 22.04/24.04 (x86-64)
• LLVM 12 + Clang (built from source)
• SMACK (built against LLVM 12)
• Boogie (dotnet tool install --global boogie)
• .NET 8 SDK
• PyPy 3.11
• Python 3 with packages: lark, cvc5, ray, redis, graphviz, networkx
• Redis server

See Environment Setup for full installation instructions.

Pipeline

All commands run from the project root (~/boogie-parser).

1. Generate (C -> Boogie)

Use SMACK to produce .bpl files from C source code. The build system is in examples/CMakeLists.txt and outputs to examples/build/.

2. Compile (Boogie -> IR)

Parse, shadow, inline, and dump metadata into a package directory.

pypy -m tools.compile examples/build/aead.bpl

Output: test_packages/aead_pkg/ containing pickled AST and metadata.

3. Interpret (Positive Examples)

Generate concrete execution traces stored as positive examples in the package.

pypy interpreter.py test_packages/aead_pkg/

4. Verify (Abductive Driver)

Run the abductive verification engine using Ray for parallelism and Redis for shared state.

python3 -m tools.driver redis_conf/aead.conf

Output: swooshh.log containing the proof tree. Each [ROOT] line is a (pc, predicate) pair representing a proved assertion. An empty log means all assertions passed.

Running Benchmarks

There are two benchmark systems: one for the Boogie verifier baseline (ct-verif) and one for Swoosh.

Swoosh Benchmarks (benchmark/benchmark.py)

Runs the full Swoosh pipeline across different configurations (CPU counts, ordering strategies) and records results to CSV.

python3 -m benchmark.benchmark

Edit the test_configs dict in benchmark/benchmark.py to select which programs to benchmark. Each entry maps a test name to its configuration:

test_configs = {
    "aead": {
        "parallelize_df": True,
        "order_sweep": ["full", "data_first", "path_first"],
        "cpu_sweep": [64, 32, 16]
    },
}

Config Key	Values	Default
parallelize_df	True / False	False
order_sweep	"data_first", "path_first", "full"	["data_first", "path_first"]
cpu_sweep	list of ints	[32, 16, 1]

Results are written to swhh_bench_results/run_<timestamp>/results.csv with columns for execution time, assertion counts, backtrack counts, and proof obligation breakdowns.

Each run has a 10-hour timeout (configurable via the timeout parameter).

ct-verif Benchmarks (benchmark/ctverif.py)

Runs Boogie directly on shadowed programs as a baseline comparison. Sweeps across CPU counts and VCS splitting strategies.

python3 -m benchmark.ctverif

Edit ctverif.py to select test configs. Available splitting modes:

Mode	Description
full_hsplit	Aggressive path splitting (/vcsMaxCost:0.01 /vcsPathSplitMult:0.0)
full_vsplit	Split on every assert (/vcsSplitOnEveryAssert)
normal	Default splitting with max splits = CPU count

Results are written to ct_verif_runs/<timestamp>/ct_verif_results.csv.

The benchmark first compiles shadowed programs using bam (the Swoosh compiler CLI) into ct_verif_out/, then runs Boogie on each with the specified configurations.

Source LoC Counting

python3 -m benchmark.loc

Counts lines in *_inline.bpl files under bpl_out/.

Available Test Programs

Programs in redis_conf/ with pre-built configurations:

Category	Programs
Small	aead, mee-cbc, curve25519-donna
Medium	auth, auth_length_pub, Hacl_HMAC_compute_sha2_256, Hacl_HMAC_compute_sha2_384, Hacl_HMAC_compute_sha2_512, Hacl_HMAC_compute_blake2b_32, Hacl_HMAC_compute_blake2s_32
Large	bearssl_test_pkcs1_i15, bearssl_test_pkcs1_i31, bearssl_test_pms_ecdh

Expected Results

• aead: one assertion failure in swooshh.log (known/expected)
• mee-cbc, all HACL*, auth: swooshh.log should be empty (all assertions proved)

Redis Configuration

Each test has a config in redis_conf/<name>.conf. Redis runs on port 6380 with password password. Key settings:

io-threads 16
bind 0.0.0.0
requirepass password
save ""
appendonly no

The driver starts Redis automatically from the config file.

Environment Setup

System Dependencies

sudo apt update && sudo apt upgrade -y
sudo apt install -y build-essential cmake libboost-all-dev redis-server dotnet-sdk-8.0
sudo systemctl enable --now redis-server

LLVM 12

export LLVM_DIR=$HOME/llvm-dir
mkdir -p "$LLVM_DIR"/{src/build,src/tools/clang,src/projects/compiler-rt}
cd "$LLVM_DIR"

wget -q https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/llvm-12.0.1.src.tar.xz
wget -q https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/clang-12.0.1.src.tar.xz
wget -q https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/compiler-rt-12.0.1.src.tar.xz

sudo tar -C src -xf llvm-12.0.1.src.tar.xz --strip-components=1
sudo tar -C src/tools/clang -xf clang-12.0.1.src.tar.xz --strip-components=1
sudo tar -C src/projects/compiler-rt -xf compiler-rt-12.0.1.src.tar.xz --strip-components=1

cd "$LLVM_DIR/build"
cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ../src
make -j$(nproc)

# Add to ~/.bashrc
export PATH=$LLVM_DIR/build/bin:$PATH

SMACK

cd ~/boogie-parser
mkdir -p smack/build && cd smack/build
cmake -G "Unix Makefiles" \
  -DCMAKE_C_COMPILER=clang \
  -DCMAKE_CXX_COMPILER=clang++ \
  -DCMAKE_BUILD_TYPE=Release ..
make -j$(nproc)

Boogie

dotnet tool install --global boogie
echo 'export PATH="$PATH:$HOME/.dotnet/tools"' >> ~/.bashrc
source ~/.bashrc

PyPy 3.11

cd /tmp
wget -q https://downloads.python.org/pypy/pypy3.11-v7.3.19-linux64.tar.bz2
sudo mkdir -p /opt/pypy-7.3.19
sudo tar -C /opt/pypy-7.3.19 --strip-components=1 -xjf pypy3.11-v7.3.19-linux64.tar.bz2
echo 'export PATH=/opt/pypy-7.3.19/bin:$PATH' >> ~/.bashrc
source ~/.bashrc

Python Packages

# PyPy (compiler & interpreter)
pypy -m ensurepip --upgrade
pypy -m pip install lark graphviz

# Python 3 (driver, benchmarks)
pip install -r requirements.txt

Quick Reference

Action	Runtime	Command
Compile	PyPy	pypy -m tools.compile <file.bpl>
Interpret	PyPy	pypy interpreter.py <pkg_dir>
Verify	Python 3	python3 -m tools.driver <config.conf>
Benchmark (Swoosh)	Python 3	python3 -m benchmark.benchmark
Benchmark (ct-verif)	Python 3	python3 -m benchmark.ctverif
Tests	Python 3	python3 -m pytest tests/