Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection

Alexa VanHattum, Monica Pardeshi, Chris Fallin, Adrian Sampson, Fraser Brown

2024

1 reference

Abstract

Language-level guarantees---like module runtime isolation for WebAssembly (Wasm)---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 Crocus, a system for lightweight, modular verification of instruction-lowering rules within Cranelift, a production retargetable Wasm native code generator. We use Crocus to verify lowering rules that cover WebAssembly 1.0 support for integer operations in the ARM aarch64 backend. We show that Crocus 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.

View Paper PDF DOI

🔄 Interpreters & VMs

1 repository

1 reference

Code References

▶ bytecodealliance/wasmtime

1 file

▶ cranelift/isle/veri/README.md

This directory contains Crocus, a tool for verifying instruction lowering and transformation rules written in ISLE. Crocus uses an underlying SMT solver to model values in ISLE rules in as logical bitvectors, searching over all possible inputs to find potential soundness counterexamples. The motivation and context project are described in detail in our ASPLOS 2024 paper: [Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection](https://dl.acm.org/doi/10.1145/3617232.3624862).

Link copied to clipboard!