Research and Reflections

Publications

2023

Rao, Xiaojia*; Georges, Aïna Linn* (Shared First Authors); Legoupil, Maxime; Watt, Conrad; Pichon-Pharabod, Jean; Gardner, Philippa; Birkedal, Lars

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs Journal Article

In: Proc. ACM Program. Lang., vol. 7, no. PLDI, 2023.

Abstract | Links | BibTeX

2021

Watt, Conrad; Rao, Xiaojia; Pichon-Pharabod, Jean; Bodin, Martin; Gardner, Philippa

Two Mechanisations of WebAssembly 1.0 Proceedings Article

In: Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings, pp. 61–79, Springer-Verlag, Berlin, Heidelberg, 2021, ISBN: 978-3-030-90869-0.

Abstract | Links | BibTeX

@inproceedings{10.1007/978-3-030-90870-6_4,

title = {Two Mechanisations of WebAssembly 1.0},

author = {Conrad Watt and Xiaojia Rao and Jean Pichon-Pharabod and Martin Bodin and Philippa Gardner},

url = {https://doi.org/10.1007/978-3-030-90870-6_4},

doi = {10.1007/978-3-030-90870-6_4},

isbn = {978-3-030-90869-0},

year  = {2021},

date = {2021-01-01},

booktitle = {Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings},

pages = {61–79},

publisher = {Springer-Verlag},

address = {Berlin, Heidelberg},

abstract = {WebAssembly (Wasm) is a new bytecode language supported by all major Web browsers, designed primarily to be an efficient compilation target for low-level languages such as C/C++ and Rust. It is unusual in that it is officially specified through a formal semantics. An initial draft specification was published in 2017 [14], with an associated mechanised specification in Isabelle/HOL published by Watt that found bugs in the original specification, fixed before its publication [37].The first official W3C standard, WebAssembly 1.0, was published in 2019 [45]. Building on Watt’s original mechanisation, we introduce two mechanised specifications of the WebAssembly 1.0 semantics, written in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. Wasm’s compact design and official formal semantics enable our mechanisations to be particularly complete and close to the published language standard. We present a high-level description of the language’s updated type soundness result, referencing both mechanisations. We also describe the current state of the mechanisation of language features not previously supported: WasmCert-Isabelle includes a verified executable definition of the instantiation phase as part of an executable verified interpreter; WasmCert-Coq includes executable parsing and numeric definitions as on-going work towards a more ambitious end-to-end verified interpreter which does not require an OCaml harness like WasmCert-Isabelle.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

Self-Reflection

My research has mostly been on WasmCert-Coq, a Coq mechanisation of the WebAssembly language specification, which I am actively maintaining on Github. In addition to the interest in the development of the specific language itself, I’m also keen on:

implementing a long-term maintainable mechanisation of an industrial language standard: some existing mechanisations projects can be implemented in a done-and-forgot approach, because the underlying theory is not subject to any change. However, this often leads to unmaintainable mechanisation artefact. There is a lot to be said on good ‘mechanisation engineering practices’, and I only come across them when I regret about a particular choice I have made in hindsight.

studying the foundations of proof assistants through active usage and experiments, in the hope of finding something useful for other usages. Eventually, it would be cool to do real mathematical researches using a proof assistant as a tool which can actually assist in coming up with the proofs, instead of just for verifying the existing ones.