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

A single mismatched bit-width in one of the tiny rules that turn WebAssembly into machine code let a sandboxed program read and write memory tens of gigabytes outside its box, a 9.9-out-of-10 security hole, and such lowering rules are error-prone even for experts; this work from Cornell, CMU, and the Bytecode Alliance builds Crocus, which checks each rule in the production Cranelift compiler by asking an SMT solver whether the rule's two sides always compute the same value, catching known CVEs in under a second and finding new bugs, while engineers write short semantic annotations right beside the rules they already maintain.

Why this problem is worth solving

The bug that motivates this work lived in the compiler’s very last step, and it helps to understand what that step is and why it is so treacherous.

The reason such a slip becomes a security emergency, rather than merely a wrong answer, is the trust model of the language being compiled.

What people did before, and where it broke

• Test and fuzz the compiler. Run large test suites and fuzzers over the compiler and compare outputs, the standard industrial safety net for a code generator. Where it broke. Fuzzers had not found the rule bugs Crocus catches — to the authors’ knowledge no other means, fuzzers included, had discovered new bugs in the rules Crocus verifies — because these faults hide in rare width-and-sign corner cases that random inputs seldom hit.
• Verify a compiler foundationally. Build a compiler with a proof assistant so the whole thing is proved correct end to end, as CompCert and CakeML do. Where it broke. That takes experts years and forbids the aggressive optimizations a production compiler like Cranelift depends on, so it is simply not how a fast, constantly-changing code generator gets built.
• Verify rules with a solver, assuming fixed semantics. Lighter tools such as Alive for LLVM peephole rules and Jitterbug for a BPF just-in-time compiler hand a solver the before-and-after and check equivalence, over a fixed, known instruction set. Where it broke. ISLE is not fixed — engineers define new operators inside the lowering language itself, with meaning only in external Rust, and lowerings can be many-to-many — so a tool built around a baked-in instruction set has nothing to stand on.
• Formalize the instruction set once, separately. Efforts like SAIL and the K framework write down precise semantics for an ISA that tools can reuse. Where it broke. Those cover the target ISA but not Cranelift’s own intermediate representation or its external Rust helper terms, and they are not co-maintained with the rules, so on their own they cannot verify a lowering rule that mixes all three.
• The gap. One camp had airtight proofs but could not keep up with a fast optimizing compiler; another had cheap solver checks but assumed a fixed instruction set that ISLE flatly violates; and the ISA formalizations described the target but not the compiler’s own moving parts. What was missing was a lightweight, per-rule check whose semantics could stretch to cover operators the engineers invent and evolve — exactly the setting a production WebAssembly backend lives in.

How Crocus works

The idea

Ask a solver whether a rule’s two sides are the same, one rule at a time. The core of Crocus is deliberately modest. It does not try to prove the whole compiler correct; it takes a single instruction-lowering rule — a left-hand pattern and the right-hand machine code meant to replace it — and asks an SMT solver a single sharp question: for every possible input, do these two sides compute exactly the same value? If the answer is yes, that rule is faithful. If the answer is no, the solver produces a concrete input on which they disagree. This is a lightweight, per-rule discipline rather than a heavyweight whole-program proof, which is precisely what lets it ride along with a compiler that changes every week. Bringing a solver directly into the compiler so that a rewrite is guaranteed sound rather than merely tested is the same instinct the solver-aided compiler work covered elsewhere on this site follows, letting the compiler lean on an automated reasoner to certify that a transformation preserves meaning instead of hoping a test suite would notice if it did not.

Let engineers write the semantics right next to the rules they already own. The obstacle to reasoning about Cranelift is that its lowering language, ISLE, is open-ended — engineers routinely invent new operators whose meaning lives only in hand-written Rust, so there is no fixed instruction set a verifier could bake in. Crocus’s answer is an annotation language: beside each term, a developer writes a short specification, a provide clause for what the term computes and a require clause for the precondition under which it applies. Because ISLE rules only fire when every matched term is defined, treating terms as partial functions and handling require clauses in the Hoare-logic way — assumed when a term appears on the left, checked when it appears on the right — mirrors the matching semantics exactly. The annotations sit in the same source files as the rules and are co-maintained with them, so the specification does not rot away from the code. Splitting one intractable whole-system proof into small, local specifications that live beside the design and compose into a guarantee is the same modular discipline the scalable hardware-invariant-learning work covered elsewhere on this site is built on, replacing a single monolithic proof obligation with many small local ones that a solver can actually discharge.

Make every failure a concrete, actionable counterexample. A verifier that only announced pass or fail would leave an engineer to hunt for what went wrong. Crocus instead hands back the exact operand bits on which a rule’s two sides diverge, so a bug is not merely flagged but localized: here is the 32-bit value, shifted by this amount, that makes the emitted code reach outside the sandbox. That specificity is what let the tool not only reproduce known CVEs in under a second but also root-cause a mid-end optimization bug — a rewrite turning false into true — faster than the compiler’s own engineers could by hand, and even surface a bug just from the act of writing an annotation that had no consistent answer. Turning a vague sense that something is wrong into a specific, minimal input that reliably triggers the fault is the same payoff the compiler differential-testing work covered elsewhere on this site delivers, driving the compiler until two runs disagree and surfacing the precise program that exposes the miscompilation.

Following the reasoning through Crocus

The matched pattern is a 64-bit extension of a 32-bit shift by a constant; an if-guard checked the shift amount was at most 3.

Why it works

• Per-rule equivalence turns an impossible whole-compiler proof into a tiny tractable one. Verifying an entire optimizing compiler is a years-long, optimization-forbidding effort → but a single lowering rule has a small left side and right side whose equality a solver can decide in well under a second → so the safety-critical rules get real proofs without freezing the compiler that engineers keep changing.
• Functional equivalence is exactly the property that catches these bugs. The CVEs were all cases where the replacement code silently computed a different value than the pattern it replaced → and asking whether the two sides ever disagree on any input is precisely a bitvector-equivalence query → so a mismatched width or a wrong extension shows up as a concrete input on which they diverge.
• Annotations beside the rules give the solver meaning that no fixed semantics could. ISLE lets engineers invent new terms whose meaning lives only in external Rust → but a short provide-and-require annotation next to each term hands the solver that meaning in SMT form → so the tool reasons about a moving target that Alive-style fixed-instruction-set verifiers cannot follow.
• Require and provide clauses model ISLE’s partial-function matching without extra machinery. A rule only fires when every left-side term is defined and its preconditions hold → so treating terms as partial functions, assuming requires on the left and checking them on the right, mirrors matching exactly → which is why annotating a rule sometimes reveals the bug before the solver even runs, as with the divide CVE.
• Counterexamples make each failure actionable instead of merely flagged. A bare not-equivalent verdict would leave engineers hunting → but the solver returns the exact operand bits on which the two sides differ → so a developer sees, for instance, that one 32-bit value shifted by two bits leaks nonzero high bits, and can fix or delete the rule at once.

What it costs (trade-offs and scope)

• The annotations are trusted, not proven. Crocus’s guarantees are only as good as the roughly 136 hand-written annotations, about a thousand lines, that supply the semantics; a wrong annotation could make a buggy rule look fine. The authors cross-reference some from the SAIL-ISLA ISA semantics and point to future work that would derive or check annotations automatically.
• Coverage is a deliberate slice, not the whole backend. The verified rules are the integer operations lowering from WebAssembly to aarch64. Left out for now are 128-bit integers, floating point, SIMD vectors, and side-effecting or control-flow instructions. Measured against a running compiler, the verified rules are 19.8 percent of the unique rules the WebAssembly reference test suite exercises, and 15.8 percent for the Rust-via-Cranelift backend.
• Some rules are too hard for the solver to finish. Rules involving multiplication, division, remainder, and population count on wide bitvectors are notoriously slow for SMT solvers; ten rules time out on some width instantiations. The authors note that injecting a flaw into any of these still yields a counterexample within ten seconds, so the timeouts limit proofs of absence, not bug-finding.
• A handful of failures are not real bugs. Six type instantiations fail a strict bitvector-equality check yet are correct in context, because the surrounding code does not actually require the two sides to be bit-for-bit equal; they verify once given custom verification conditions rather than plain equivalence.
• It verifies rules, not the compiler. This is per-rule functional equivalence between a pattern and its replacement, not end-to-end compiler correctness. Register allocation, instruction scheduling, the mid-end in general, and the interactions between rules are outside what a single equivalence check covers, though the authors show the same tool can reason about some mid-end rewrites too.
• The strongest bug-finding claim is modestly framed. The paper reports two new bugs, one under-specified-semantics issue, and one mid-end root cause, and notes that to its knowledge no other means had found new bugs in the rules Crocus verifies. That is a real result, but it is a present-tense, this-set-of-rules claim, not a proof that the rules are bug-free for all time.
• Writing the specs takes real expertise. Reconciling the compiler’s intermediate types with the target ISA’s types, and pinning down the exact width-and-sign behavior of each term, is careful work; the effort is lightweight compared with foundational verification, but it is not free, and it asks formal-methods care of engineers whose expertise is compilers.

The evaluation

Check yourself

Sources

The paper is “Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection” by Alexa VanHattum, Monica Pardeshi, Chris Fallin, Adrian Sampson, and Fraser Brown, published at ASPLOS 2024, pages 242 to 247, DOI 10.1145/3617232.3624862. The authors are at Cornell University, Carnegie Mellon University, and the Bytecode Alliance. The tool is named Crocus and is built as a fork of the Wasmtime and Cranelift code base.

This explainer is written from the full text of the paper. Everything above comes from the paper’s own sections: the introduction’s account of the 9.9-out-of-10 x86-64 addressing-mode CVE in which a shift on a 32-bit value on the left and a 64-bit value on the right let guest code reach 6 to 34 gigabytes outside its sandbox; the background on instruction selection as pattern-matching over the ISLE term-rewriting language and on SMT-based equivalence checking; the design of Crocus’s annotation language with its provide clauses for semantics and require clauses for Hoare-style preconditions, its treatment of ISLE terms as partial functions, and its extra constructs for bit-width introspection, symbolic rotates, exhaustive switch, variadic concatenation, and custom encodings such as count-leading-sign and subtract-with-flags; and the evaluation, which verifies 98 rules across 377 type instantiations for WebAssembly integer lowering to aarch64 in about 136 annotations and roughly a thousand lines, finishes 349 of 377 instantiations within five minutes on a laptop with ten rules timing out on wide multiply, divide, remainder, and population count, measures coverage at 19.8 percent of the rules exercised by the WebAssembly reference test suite and 15.8 percent for the Rust-via-Cranelift backend, reproduces the x86-64 addressing CVE in under a second along with an aarch64 unsigned-divide CVE and a count-leading-sign bug, and reports two newly found bugs, an under-specified-constant-semantics issue, and a mid-end boolean-rewrite root cause that Crocus diagnosed before the compiler’s engineers did.