Language-level guarantees–like runtime isolation for WebAssembly (Wasm) modules–are only as strong as the compiler that produces a final, native-machine-specific executable. The process of lowering language-level constructions to ISA-specific instructions can introduce subtle bugs that violate security guarantees. In this paper, we present VeriISLE, a system for lightweight, modular verification of instruction-lowering rules within Cranelift, a production retargetable Wasm code generator. We use VeriISLE to verify lowering rules that cover WebAssembly 1.0 support for integer operations in the ARM aarch64 backend. We show that VeriISLE can reproduce 3 known bugs (including a 9.9/10 severity CVE), identify 2 previously-unknown bugs and an underspecified compiler invariant, and help analyze the root causes of a new bug.

33 pages

Thesis Committee:
Fraser Brown (Advisor)
Bryan Parno

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu