Events

Preserving Language-level Security in Real Systems

Promises are cheap. Software vendors routinely describe their offerings as “secure”, but few are based on designs that can guarantee even the most basic security properties. To address this problem, services like Cloudflare, Android, and Firefox are increasingly relying on languages like Rust and WebAssembly to provide safety by design. But these promises too can fall short: any vulnerability in the execution stack—compiler, runtime, OS, or hardware—can undermine language-level security.

In this talk, Evan Johnson presents his research towards delivering on the promise of language-level security by building an execution stack that guarantees that these security properties are preserved. In particular, Johnson will describe how two of his systems, VeriWasm and WaVe, guarantee safety of the compiler and language runtime respectively. Johnson will focus on how the designs of these systems provide formal guarantees while still adhering to production constraints that allow them to be deployed in real systems used by millions of users. Johnson will conclude by discussing some future directions for this work, such as retrofitting formal safety guarantees to safety-critical embedded systems and clean-slate OS design using language-level isolation.