A Program Logic for First-Order Encapsulated WebAssembly (ECOOP 2019)

Who

Conrad Watt, Petar Maksimović, Neel Krishnaswami, Philippa Gardner

Track

ECOOP 2019 Research Papers

Time Zone

The program is currently displayed in (GMT+01:00) Belfast.

Use conference time zone: (GMT+01:00) BelfastSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Wed 17 Jul 2019 16:00 - 16:20 at Mancy - Program Analysis 1 Chair(s): Yannis Smaragdakis

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.

DOI

https://doi.org/10.4230/LIPIcs.ECOOP.2019.9

Conrad Watt

University of Cambridge

Petar Maksimović

Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia

United Kingdom

Neel Krishnaswami

Computer Laboratory, University of Cambridge

Philippa Gardner

Imperial College London