2026-07-23T18:19:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10801 2024-03-06T10:46:40Z ddc:004 open_access

A Program Logic for First-Order Encapsulated WebAssembly Watt, Conrad Maksimović, Petar Krishnaswami, Neelakantan R. Gardner, Philippa WebAssembly program logic separation logic soundness mechanisation We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strong guarantees given by WebAssembly’s type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly’s uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Conrad Watt and Petar Maksimović and Neelakantan R. Krishnaswami and Philippa Gardner 2019 Is Part Of LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2019.9 urn:nbn:de:0030-drops-108011 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.9 eng https://creativecommons.org/licenses/by/3.0/legalcode