← projects

// case study

Symbolic LLVM Memory Sandboxing for WebAssembly

2025 · EPFL · Research project

  • LLVM
  • WebAssembly
  • C++
  • Static Analysis
  • Symbolic Execution

Context

WebAssembly is increasingly used as an execution layer for smart contracts, where a single memory-safety bug can be catastrophic and execution must remain strictly deterministic. Conventional sandboxing approaches insert bounds checks on every memory access, paying a heavy runtime cost even when most accesses are provably safe.

This research project asks: how many of those checks can a compiler prove away — and how cheap can the remaining ones be made?

Approach

I built a static analysis framework operating on LLVM IR that reasons symbolically about memory accesses:

  • Canonical symbolic expressions represent pointer arithmetic in a normal form, so equivalent access patterns are recognized and analyzed once.
  • Phi-aware state merging keeps the analysis precise across control-flow joins instead of conservatively discarding information.
  • Loop-bound inference derives iteration bounds so accesses inside loops can be proven safe in aggregate rather than checked per iteration.

Accesses the analysis proves in-bounds need no instrumentation; for the rest, the framework emits optimized runtime checks, preserving WASM’s determinism guarantees.

Results

The framework was evaluated on real-world computation kernels, demonstrating that a large share of naive bounds checks can be eliminated while preserving full memory safety. The full report has the details; the slide deck gives a condensed overview.