A program logic for first-order encapsulated WebAssembly

We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. Wedesign a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strongguarantees given by WebAssembly’s type system, and show how to adapt the standard separationlogic triple and proof rules in a principled way to capture WebAssembly’s uncommon structuredcontrol flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, givingabstract specifications independent of the underlying implementation. We mechanise Wasm Logicand its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formaliseand fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, upto transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the firstprogram logic for WebAssembly, and represents a first step towards the creation of static analysistools for WebAssembly