A Program Logic for First-Order Encapsulated WebAssembly
A Program Logic for First-Order Encapsulated WebAssembly
复制标题
一阶封装 WebAssembly 的程序逻辑
DOI：
10.4230/lipics.ecoop.2019.9
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Philippa Gardner
中科院分区：
文献类型：
--
作者：
Conrad Watt;P. Maksimovic;N. Krishnaswami;Philippa Gardner
我们介绍 Wasm Logic，这是一种用于一阶封装 WebAssembly 的健全程序逻辑。我们设计了一种新颖的断言语法，专门针对 WebAssembly 基于堆栈的语义和 WebAssembly 类型系统提供的强有力的保证，并展示了如何以原则性的方式适应标准分离逻辑三元组和证明规则，以捕获 WebAssembly 不常见的结构化控制流。使用 Wasm Logic，我们指定并验证一个简单的 WebAssembly B 树库，提供独立于底层实现的抽象规范。我们在 Isabelle/HOL 中完整地机械化了 Wasm Logic 及其健全性证明。作为健全性证明的一部分，我们形式化并完全机械化了一种新颖的 WebAssembly 大步语义，我们证明它在传递闭包之前与原始 WebAssembly 小步语义是等价的。 Wasm Logic 是 WebAssembly 的第一个程序逻辑，代表着为 WebAssembly 创建静态分析工具迈出了第一步。
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.
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
低级代码的机械化、组合验证
DOI：
10.1007/978-3-319-06200-6_8
发表时间：
2014
期刊：
影响因子：
--
作者：
Björn Bartels;Nils Jähnig
通讯作者：
Nils Jähnig
JaVerT 2.0：JavaScript 的组合符号执行
影响因子：
--
作者：
Fragoso Santos J
通讯作者：
Fragoso Santos J