Computer Science Colloquium
Friday, March 01
2:35pm in Wege (TCL 123)
Lightweight, Modular Verification for Systems Compilers
Language-level system guarantees—like runtime isolation for WebAssembly modules—are only as strong as the compiler that produces a native-machine-specific executable. Subtle wrong-code bugs in the compiler can introduce serious security flaws. In this talk, I’ll describe Crocus, our system for lightweight, modular verification of instruction-lowering rules in Cranelift, an industry WebAssembly compiler. Crocus reproduces known bugs (including a 9.9/10 severity security bug) and identifies previously-unknown bugs and underspecified compiler invariants. More broadly, I’ll discuss how integrating lightweight formal methods can free systems engineers from having to choose between prioritizing efficiency and correctness.
Alexa VanHattum is an Assistant Professor of Computer Science at Wellesley College. Her research sits at the intersection of programming languages and systems, with a focus on applying lightweight formal methods to the compiler stack. She recently received her PhD from Cornell University, where she was an NSF Graduate Research Fellow. She holds a BS from Brown University and has previously worked on Rust verification at AWS and health software at Apple.