Master's Thesis: A Verified, Analysis-Focused Interpreter for WebAssembly

My master’s thesis about WebAssembly is now available under Publications.

Abstract

WebAssembly is a standardized general-purpose bytecode language that primarily targets usage as part of web applications. Next to an English prose specification, it also has an official formal specification that describes the language semantics unambiguously in a natural deduction style. This motivates the development of verified tools for static analysis and optimization, since the formal specification can be used as a direct basis to verify against. However, this specification of execution by means of reduction rules has certain inconvenient properties such as mixing data and code, as well as not having any notion of addresses in a program. This makes the application of techniques such as Abstract Interpretation impossible in the sense that information should be determined and stored for specific program points. We overcome these limitations by developing a new interpreter that uses an explicit call stack and value stack, in addition to explicitly tracking a program counter on top of immutable code. This interpreter is developed directly on top of the WebAssembly mechanization developed by Conrad Watt in Isabelle/HOL, a generic theorem proving and logic system. We then present a proof for completeness of our interpreter, showing that it can indeed represent any execution allowed by the WebAssembly specification, which makes it a suitable basis for static analysis. As a side effect of this, we also show that real-world interpreters taking a similar approach using explicit stacks and program counters can also cover the entire WebAssembly language. In addition to the interpreter, we extend the mechanization by formalizing the specification of integer types and operations, as this part had still been missing. We also supply executable implementations for these integer operations and verify them against the specification.