Symbolic LLVM Memory Sandboxing for WebAssembly

Proving memory-safety bounds checks away at compile time cut instrumentation overhead by up to 85% across 12 WebAssembly kernels, while preserving full spatial safety and deterministic execution.

Problem

WebAssembly is increasingly used as an execution layer for smart contracts, where a single memory-safety bug can be catastrophic and execution must stay strictly deterministic across replicas. Conventional sandboxing inserts a bounds check on every memory access, paying 1.6–10.6× runtime overhead even when most accesses are provably safe.

The question this project asks: how many of those checks can a compiler prove away statically, and how cheap can the remainder be made without sacrificing determinism or spatial safety?

Architecture

The work extends Droplet, an ahead-of-time compiler that lowers WASM smart contracts to native .so shared objects, which then run on Drizzle, a runtime that executes contracts in parallel and deterministically. My symbolic memory-safety layer plugs into Droplet at the LLVM IR level.

My contribution

Droplet and Drizzle are pre-existing systems in EPFL’s Distributed Computing Lab. My work is the symbolic memory-safety layer inside Droplet, built under the supervision of Prof. Rachid Guerraoui and Dr. Gauthier Voron:

• SymExpr — a symbolic expression framework that represents pointer arithmetic in a canonical normal form, so equivalent access patterns are recognized and analyzed once.
• SymbolicState — a per-basic-block state with inter-block merging that traverses the CFG in reverse post-order, staying precise across control-flow joins instead of conservatively discarding information.
• Memory Check Optimization — the loop-aware analysis and check emitter described below.

Key technical decisions

• Loop detection via CFG back-edges and the dominator tree; the natural loop body is derived from the header/tail boundary.
• Fixed-point refinement over each loop until the symbolic state stabilizes, inferring induction variables and their step (e.g. i += 1) to bound loop accesses in aggregate rather than per iteration.
• Grouping loop-strided accesses by symbolic base/stride, then emitting a single pre-loop block with one range check per group.

From n checks to one

for i in 0..n:
  check(base + i*stride)   // runtime bounds check
  load (base + i*stride)

check_range(base, base + (n-1)*stride)   // once, pre-loop
for i in 0..n:
  load (base + i*stride)

Results

Benchmarked on 12 computation kernels under 4 instrumentation configurations, using µs medians under realistic .so batching. Naive per-access bounds checking costs 1.6–10.6× the un-sandboxed baseline; the optimized instrumentation removes up to 85% of that overhead (median ~66% across the 12 kernels, best configuration per kernel), collapsing most workloads back toward 1.0×.

Limitations and next steps

• Assumption-based check elision — tracking icmp constraints from user code to prove that two access ranges are disjoint (and drop or merge their checks) is a working skeleton, not yet evaluated.
• Sea of Nodes — the original goal of a Sea-of-Nodes IR for precise memory placement was descoped to fit the project timeline; the symbolic infrastructure is designed to later sit beneath a SoN-based optimizer.

The full report has the details; the slide deck gives a condensed overview.