PI: Neel Krishnaswami, Co-Is: Conrad Watt and Jean Pichon, University of Cambridge

  • WebAssembly is the first new programming language to be supported on the Web in over 20 years.
  • We have developed WasmCert-Coq, a new mechanisation of the WebAssembly language in Coq.
  • We mechanise WebAssembly’s linking and allocation phase for the first time.
  • We investigate WebAssembly’s proposed relaxed memory concurrency model.

WebAssembly is a new language supported by all major Web browsers, intended to be an efficient compilation target for low-level languages such as C++ and Rust, with the aim that the resulting compiled program can be executed in the browser with near-native performance.

WebAssembly is unusual in that its standards body maintains a full, normative formal specification for the language, and all features must be fully formalised before they are accepted as extensions to the standard.

WebAssembly was initially single-threaded, but an in-progress extension to the language introduces threads and concurrent memory operations, including atomic accesses. Concurrent access to memory in WebAssembly can give rise to “relaxed memory” behaviours, allowing program results that cannot be explained by considering only naive sequential interleavings of the operations of individual threads. The WebAssembly concurrency proposal includes a formal model of the permitted relaxed memory behaviour.

This project aims to investigate areas of the WebAssembly semantics which interact with the proposed concurrent extension, and develop a Coq mechanisation of the language to complement the existing Isabelle mechanisation, which was based on an earlier draft of the WebAssembly semantics.

We have completed a Coq mechanisation of WebAssembly’s core sequential semantics, and extended both the Coq and Isabelle mechanisations to model “instantiation” for the first time. Instantiation is a linking and allocation phase of the WebAssembly program lifecycle not described in the initially published semantics.

The WebAssembly concurrency proposal does not include a mechanism for thread creation. Instead, WebAssembly is embedded within a “host language” (such as JavaScript on the Web) which is responsible for the creation of threads running WebAssembly code. As an initial step towards mechanising this behaviour, we mechanised an abstract host language which is intended to capture the capabilities of JavaScript’s WebAssembly API. We are currently investigating integration with the Iris framework (Jung et al, ICFP 2016), which facilitates the specification of higher-order concurrent program logics.

We discovered two deficiencies in WebAssembly’s concurrency model. First, WebAssembly and the related JavaScript model were incorrectly specifying the atomic compare-exchange operation, making its synchronisa-tion guarantees too strong in the case that the comparison fails. This issue was corrected in both specifications.

More seriously, we discovered that the intended compilation scheme from concurrent C++11 to WebAssembly is formally unsound due to an issue with the WebAssembly model related to the notorious “out-of-thin-air” problem. Luckily, this issue is primarily theoretical, as no real system is expected to exhibit thin-air executions.

IMPACT. As interest grows around WebAssembly as a bytecode format for smart contracts, we’re excited about WasmCert-Coq and hope to use it in future verification efforts!  – Vilhelm Sjöberg, Research Scientist at CertiK –

With WebAssembly, we strove to design a high-assurance platform, which includes a specification with a formal semantics. Mechanisation is vital both for building confidence in this specification and its proposed extensions and for formal reasoning about WebAssembly programs. I’m very pleased that this work has brought new parts of the WebAssembly semantics into Coq.– Andreas Rossberg, WebAssembly Specification Editor –