• Two mechanisations of WebAssem...

Treffer: Two mechanisations of WebAssembly 1.0

Title:
Two mechanisations of WebAssembly 1.0
Authors:
Watt, C, Rao, X, Pichon-Pharabod, J, Bodin, M, Gardner, P
Contributors:
Engineering & Physical Science Research Council (E
Source:
24th international symposium of Formal Methods (FM21) ; 79 ; 61
Publisher Information:
Springer Verlag
Publication Year:
2021
Collection:
Imperial College London: Spiral
Subject Terms:
Science & Technology, Technology, Computer Science, Interdisciplinary Applications, Theory & Methods, Mechanised specification, Type soundness, WasmCert, SEMANTICS, JAVA, VERIFICATION, Artificial Intelligence & Image Processing
Subject Geographic:
Beijing, China
Document Type:
Konferenz conference object
Language:
unknown
Relation:
Lecture Notes in Computer Science; http://hdl.handle.net/10044/1/91431; EP/R034567/1
DOI:
10.1007/978-3-030-90870-6_4
Availability:
http://hdl.handle.net/10044/1/91431
https://doi.org/10.1007/978-3-030-90870-6_4
Rights:
© 2021 Springer Nature Switzerland AG. The final publication is available at Springer via https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4
Accession Number:
edsbas.F71F88EB
Database:
BASE

Weitere Informationen

WebAssembly (Wasm) is a new bytecode language supportedby all major Web browsers, designed primarily to be an efficient com-pilation target for low-level languages such as C/C++ and Rust. It isunusual in that it is officially specified through a formal semantics. Aninitial draft specification was published in 2017 [14], with an associatedmechanised specification in Isabelle/HOL published by Watt that foundbugs in the original specification, fixed before its publication [37].The first official W3C standard, WebAssembly 1.0, was published in2019 [45]. Building on Watt’s original mechanisation, we introduce twomechanised specifications of the WebAssembly 1.0 semantics, writtenin different theorem provers: WasmCert-Isabelle and WasmCert-Coq.Wasm’s compact design and official formal semantics enable our mecha-nisations to be particularly complete and close to the published languagestandard. We present a high-level description of the language’s updatedtype soundness result, referencing both mechanisations. We also describethe current state of the mechanisation of language features not previouslysupported: WasmCert-Isabelle includes a verified executable definitionof the instantiation phase as part of an executable verified interpreter;WasmCert-Coq includes executable parsing and numeric definitions ason-going work towards a more ambitious end-to-end verified interpreterwhich does not require an OCaml harness like WasmCert-Isabelle.