Repository logo
 

A Program Logic for First-Order Encapsulated WebAssembly

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Maksimovic, Petar 
Krishnaswami, Neelakantan R 
Gardner, Philippa 

Abstract

We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly's stack-based semantics and the strong guarantees given by WebAssembly's type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly's uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.

Description

Keywords

cs.PL, cs.PL

Journal Title

33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Conference Name

European Conference on Object-Oriented Programming (ECOOP)

Journal ISSN

1868-8969

Volume Title

134

Publisher

Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik
Sponsorship
Engineering and Physical Sciences Research Council (EP/N02706X/2)
EPSRC Programme Grant “Semantic Foundations for Interact- ive Programs” (EP/N02706X/2)