LeanWasm: An Intrinsically-Typed Interpreter for WebAssembly

Abstract

WebAssembly is a new low-level programming language and portable bytecode format designed with the goal of increasing interoperability and security across the software ecosystem.

In order to ensure correctness and adherence to the official specification, some WebAssembly implementations use formally verified interpreters as testing oracles. This thesis explores a novel approach to defining verified interpreters, by using an intrinsically-typed representation of the WebAssembly abstract syntax.

The main contributions of this thesis include an intrinsically-typed WebAssembly interpreter that closely follows the official reference interpreter, and an optimized interpreter based on an improved representation of control-flow. The interpreters are implemented in the Lean 4 theorem prover, leveraging its support for dependent typing and functional-but-in-place programming.