Security

13 papers selected. Empowering WebAssembly with Thin Kernel Interfaces Arjun Ramesh, Tianshu Huang, Ben L. Titzer, Anthony Rowe 0001 TL;DR — A new OS interface design exposes thin, capability-based kernel primitives directly to WebAssembly modules, eliminating the POSIX translation layer. Why notable — WebAssembly is increasingly used beyond the browser as a portable, sandboxed compute substrate; this work shows that rethinking the system interface from scratch yields significantly lower overhead and better safety properties than layering Wasm on top of POSIX. ...

13 papers selected. Verus: A Practical Foundation for Systems Verification Andrea Lattuada 0001, Travis Hance, Jay Bosamiya, Matthias Brun 0002 et al. TL;DR — Verus is a Rust-based verification framework that makes formal proofs of low-level systems code tractable at scale, covering memory safety, functional correctness, and concurrency. Why notable — Formal verification of real systems code has long been impractical; Verus closes the usability gap by integrating SMT-based proofs directly into a systems programming language, making it the most broadly applicable verification tool for the OS community to date. ...