Publications
2025
Rao, Xiaojia; Radziuk, Stefan; Watt, Conrad; Gardner, Philippa
Progressful Interpreters for Efficient WebAssembly Mechanisation Conference
PACMPL, vol. 9, no. 22, POPL 2025.
@conference{ProgressfulInterpreter,
title = {Progressful Interpreters for Efficient WebAssembly Mechanisation},
author = {Xiaojia Rao and Stefan Radziuk and Conrad Watt and Philippa Gardner},
url = {https://www.raoxiaojia.com/wp-content/uploads/2024/11/Progressful_Interpreters_CR.pdf},
doi = {10.1145/3704858},
year = {2025},
date = {2025-01-01},
urldate = {2025-01-01},
booktitle = {PACMPL},
volume = {9},
number = {22},
series = {POPL},
abstract = {Mechanisations of programming language specifications are now increasingly common, providing machine-checked modelling of the specification and verification of desired properties such as type safety. However it is challenging to maintain these mechanisations, particularly in the face of an evolving specification. Existing mechanisations of the W3C WebAssembly (Wasm) standard have so far been able to keep pace as the standard evolves, helped enormously by the W3C Wasm standard's choice to state the language's semantics in terms of a fully formal specification. However a substantial incoming extension to Wasm, the 2.0 feature set, motivates the investigation of strategies for more efficient production of the core verification artefacts currently associated with the WasmCert-Coq mechanisation of Wasm.
In the classic formalisation of a typed operational semantics as followed by the W3C Wasm standard, both the type system and runtime operational semantics are defined as inductive relations, with associated type soundness properties (progress and preservation) and an independent sound interpreter. We investigate two more efficient strategies for producing these artefacts, which are currently all separately defined by WasmCert-Coq. First, the approach of Kokke, Siek, and Wadler for deriving a sound interpreter from a constructive progress proof --- we show that this approach scales to the W3C Wasm 1.0 standard, but results in an inefficient interpreter in our setting. Second, inspired by results from intrinsically-typed languages, we define a progressful interpreter which uses Coq's dependent types to certify not only its own soundness, but also the progress property. We show that this interpreter can implement several performance optimisations while maintaining these certifications, which are fully erasable when the interpreter is extracted from Coq. Using this approach, we extend the WasmCert-Coq mechanisation to the significantly larger Wasm 2.0 feature set, discovering and correcting several errors in the expanded specification's type system.},
keywords = {},
pubstate = {published},
tppubtype = {conference}
}
Mechanisations of programming language specifications are now increasingly common, providing machine-checked modelling of the specification and verification of desired properties such as type safety. However it is challenging to maintain these mechanisations, particularly in the face of an evolving specification. Existing mechanisations of the W3C WebAssembly (Wasm) standard have so far been able to keep pace as the standard evolves, helped enormously by the W3C Wasm standard’s choice to state the language’s semantics in terms of a fully formal specification. However a substantial incoming extension to Wasm, the 2.0 feature set, motivates the investigation of strategies for more efficient production of the core verification artefacts currently associated with the WasmCert-Coq mechanisation of Wasm.
In the classic formalisation of a typed operational semantics as followed by the W3C Wasm standard, both the type system and runtime operational semantics are defined as inductive relations, with associated type soundness properties (progress and preservation) and an independent sound interpreter. We investigate two more efficient strategies for producing these artefacts, which are currently all separately defined by WasmCert-Coq. First, the approach of Kokke, Siek, and Wadler for deriving a sound interpreter from a constructive progress proof — we show that this approach scales to the W3C Wasm 1.0 standard, but results in an inefficient interpreter in our setting. Second, inspired by results from intrinsically-typed languages, we define a progressful interpreter which uses Coq’s dependent types to certify not only its own soundness, but also the progress property. We show that this interpreter can implement several performance optimisations while maintaining these certifications, which are fully erasable when the interpreter is extracted from Coq. Using this approach, we extend the WasmCert-Coq mechanisation to the significantly larger Wasm 2.0 feature set, discovering and correcting several errors in the expanded specification’s type system.
In the classic formalisation of a typed operational semantics as followed by the W3C Wasm standard, both the type system and runtime operational semantics are defined as inductive relations, with associated type soundness properties (progress and preservation) and an independent sound interpreter. We investigate two more efficient strategies for producing these artefacts, which are currently all separately defined by WasmCert-Coq. First, the approach of Kokke, Siek, and Wadler for deriving a sound interpreter from a constructive progress proof — we show that this approach scales to the W3C Wasm 1.0 standard, but results in an inefficient interpreter in our setting. Second, inspired by results from intrinsically-typed languages, we define a progressful interpreter which uses Coq’s dependent types to certify not only its own soundness, but also the progress property. We show that this interpreter can implement several performance optimisations while maintaining these certifications, which are fully erasable when the interpreter is extracted from Coq. Using this approach, we extend the WasmCert-Coq mechanisation to the significantly larger Wasm 2.0 feature set, discovering and correcting several errors in the expanded specification’s type system.
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.
@article{10.1145/3591265,
title = {Iris-Wasm: Robust and Modular Verification of WebAssembly Programs},
author = {Xiaojia* Rao and Aïna Linn* (Shared First Authors) Georges and Maxime Legoupil and Conrad Watt and Jean Pichon-Pharabod and Philippa Gardner and Lars Birkedal},
url = {https://doi.org/10.1145/3591265},
doi = {10.1145/3591265},
year = {2023},
date = {2023-06-01},
urldate = {2023-06-01},
journal = {Proc. ACM Program. Lang.},
volume = {7},
number = {PLDI},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
abstract = {WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher- order modular programming. We present Iris-Wasm, a mechanized higher-order separation logic building on a specification of Wasm 1.0 mechanized in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby demonstrating that WebAssembly enforces strong isolation between modules.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher- order modular programming. We present Iris-Wasm, a mechanized higher-order separation logic building on a specification of Wasm 1.0 mechanized in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby demonstrating that WebAssembly enforces strong isolation between modules.
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.
@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}
}
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.
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.