Computer Science 5th Years Master's Thesis Presentation

— 12:00pm

Location:
In Person and Virtual - ET - Gates Hillman 9115 and Zoom

Speaker:
MONICA PARDESHI , Master's Candidate, Computer Science Department, Carnegie Mellon University

VeriISLE: Verifying Instruction Selection in Cranelift

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.

Thesis Committee:

Fraser Brown (Chair)
Bryan Parno

Additional Information

In Person and Zoom Participation. See announcement.

Add event to Google
Add event to iCal