61 citations · 98 across the 6 of their papers we have counts for
7 papers
Wasm SpecTec: Engineering a Formal Language Standard
Joachim Breitner, Philippa Gardner, Jaehyun Lee +8
WebAssembly (Wasm) is a low-level bytecode language and virtual machine, intended as a compilation target for a wide range of programming languages, which is seeing increasing adop…
Capstone: A Capability-based Foundation for Trustless Secure Memory Access (Extended Version)
Jason Zhijingcheng Yu, Conrad Watt, Aditya Badole +2
Capability-based memory isolation is a promising new architectural primitive. Software can access low-level memory only via capability handles rather than raw pointers, which provi…
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya +7
Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm -- and a…
Isolation Without Taxation: Near Zero Cost Transitions for SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson +5
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to hard…
Repairing and Mechanising the JavaScript Relaxed Memory Model
Conrad Watt, Christopher Pulte, Anton Podkopaev +5
Modern JavaScript includes the SharedArrayBuffer feature, which provides access to true shared memory concurrency. SharedArrayBuffers are simple linear buffers of bytes, and the Ja…
A Program Logic for First-Order Encapsulated WebAssembly
Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami +1
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 th…