Two mechanisations of WebAssembly 1.0
| Autor: | Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner |
|---|---|
| Přispěvatelé: | Engineering & Physical Science Research Council (E, University of Cambridge [UK] (CAM), Imperial College London, Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA) |
| Rok vydání: | 2021 |
| Předmět: |
WasmCert
Technology Science & Technology Type soundness Mechanised specification 020207 software engineering 0102 computer and information sciences 02 engineering and technology Isabelle/HOL 01 natural sciences [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] VERIFICATION 010201 computation theory & mathematics Computer Science Theory & Methods TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS SEMANTICS Computer Science Coq formalization 0202 electrical engineering electronic engineering information engineering Computer Science Interdisciplinary Applications Artificial Intelligence & Image Processing JAVA |
| Zdroj: | 24th international symposium of Formal Methods (FM21) Formal Methods ISBN: 9783030908690 FM 2021-Formal Methods FM 2021-Formal Methods, Nov 2021, Beijing, China. pp.1-19 Lecture Notes in Computer Science Lecture Notes in Computer Science-Formal Methods |
| ISSN: | 0302-9743 1611-3349 |
| Popis: | International audience; 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, with an associated mechanised specification in Isabelle/HOL published by Watt that found bugs in the original specification, fixed before its publication. The first official W3C standard, WebAssembly 1.0, was published in 2019. 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 ongoing work towards a more ambitious end-to-end verified interpreter which does not require an OCaml harness like WasmCert-Isabelle. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|