Emma Sudo

Verus WebAssembly Rust
Automatic Proof Instability Repair in Verus

During my summer at CMU, I began working on Morpho, a tool that automatically fixes proof instability in Verus. Proof instability is when semantically meaningless changes cause the Verus proof to suddenly fail. Instability is one of the most signficant challenges in verifying in real systems. Morpho is a continuation of Yi Zhou and Amar Shah's Cazamariposas tool. Cazamariposas finds instability fixes on the SMT level, and Morpho lifts those fixes to the Verus source level to repair instability without developer involvement. So far, this work has fixed almost half of the instability in Verita, a collection of projects that use Verus.

CMU REUSE Poster

Morpho
WasmBounds: Eliminating Memory Bounds Checks in WebAssembly

WasmBounds is a tool that elides redundant memory bounds checks in WebAssembly (Wasm) using abstract interpretation. Although runtimes for Wasm 1.0 on systems with virtual memory have been able to avoid bounds checks by using hardware guard pages, the presence of newer Wasm features (64-bit memories and single-byte page sizes) or an embedded environment generally requires software bounds checks for memory accesses, at the cost of runtime efficiency. WasmBounds shifts this runtime cost to a one-time static analysis phase. The key insight behind WasmBounds is that safe languages such as Rust and Zig already enforce bounds checks on accesses to container types. Although these safety guarantees are not immediately apparent in the compiled Wasm binary, WasmBounds can recover this information with abstract interpretation. By reasoning over a strided, sign-agnostic interval domain, WasmBounds infers the range of each memory access address and determines whether accesses are provably in bounds. Eliminating these redundant checks yields a roughly 1.2x speedup in our preliminary microbenchmark.

Wasm Research Day Slides · OSDI Poster · CS191W Paper

WasmBounds
wBPF: Safe Kernel Extensibility with WebAssembly

wBPF is a tool that I made with Max Cura, Haibib Kerim, and Ari Reid that makes programs written in arbitrary languages “safe” by using WebAssembly as an intermediary and hybridizing static analysis with dynamic instrumentation. Even after making the necessary modifications, wBPF programs run at near native speeds.

CS244C Paper

wBPF pipeline wBPF results
Ferr-OS: Rust Kernel for Safely Running WebAssembly on the Raspberry Pi

I used Rust to make a simple Raspberry Pi kernel that can run WebAssembly binaries using wasm2c and a WASI layer.

GitHub

Ferr-OS
Codillon: A Structure Editor for WebAssembly

While participating in CURIS 2025, I helped to develop a text editor for WebAssembly where every incomplete program is executable and errors are closely isolated to their origin. Codillon is currently being used to teach introductory computer science to students in CS10N. I also use Codillon on a daily basis while working on my other WebAssembly projects.

Try it out! · Poster · GitHub

Codillon