Skip to main content
Add to Calendar
2024-05-16 12:00:00
2024-05-16 13:00:00
America/New_York
Building principled and practical secure systems using Wasm
In this talk I'm going to talk about our adventures (ab)using WebAssembly tobuild more secure systems. Wasm---at least in my view---is a secure compilationintermediate representation. It makes it possible for us to compile(potentially unsafe) code to a single IR, where we enforce different securityproperties, and compile this retrofitted code to native code, where it runssecurely (e.g., isolated from every other piece of code). I'll start with ourwork sandboxing third-party C libraries in Firefox, our work speeding up andverifying Wasm compilers and runtimes, and our most recent work designinghardware extensions (and abusing existing ones) to both speed up Wasm andaddress different classes of attacks on Wasm especially as used by hyperscalers.
D463 (Star)
Add to Calendar
2024-05-17 11:00:00
2024-05-17 12:00:00
America/New_York
Seminar: Modern Verification for a Rust-Centric World
Abstract: Over the past several years, we have authored and verified large amounts of systems code through the Low* toolchain, which compiles a subset of F* to C. HACL*, a verified cryptographic library, is our flagship project, and compiles 100,000 lines of Low* to 80,000 lines of fast, verified C code. Parts of HACL* have made it into Python, Firefox or the Linux kernel. However, C is no longer the target of choice. The White House, large companies (e.g. Microsoft) and the software community at large all have embraced Rust as a new, safe language that the whole community should transition to. In that new Rusty world, how does one modernize our verification tools to leverage this new ecosystem? In this talk, I will describe three evolutions of our toolchain that bring us into the new Rust-centric world. • A new Low* -> Rust transition pipeline allows us to compile existing code, such as HACL*, directly to Rust. This allows us to avoid rewriting old code.• A new verification toolchain, Aeneas, takes unsafe-free Rust programs and converts them to a pure equivalent, that can then be reasoned upon in various theorem provers, such as F*, Lean, or Coq. This is our new way of verifying Rust programs and allows us to author fresh code directly in Rust.• A new compiler from Rust to C provides a backwards-compatibility story for the transition period where new verified software is authored in Rust directly, but engineering constraints preclude immediate adoption of the Rust toolchain.
Add to Calendar
2024-05-23 12:00:00
2024-05-23 13:00:00
America/New_York
Modular Verification of Non-Leakage for Hardware Security Modules with K2
K2 is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by its functional specification. K2's proof covers the software and the hardware of an HSM, which enables it to catch all bugs above the cycle-level digital circuit abstraction, including timing side channels. K2's key contribution is a novel approach to proving non-leakage in a modular fashion, using transitive information-preserving refinement. This enables K2 to use different techniques for verifying different layers (software and hardware), reuse existing verified components, and largely automate several parts of the proof, while still providing a single top-to-bottom combined theorem. We use K2 to develop several HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. K2 provides a strong guarantee for these HSMs; for instance, it proves that the ECDSA-on-Ibex HSM implementation (2,300 lines of code and 13,500 lines of Verilog) leaks nothing more than what is allowed by a 50-line specification of its behavior.
D463 (Star)
Add to Calendar
2024-06-07 9:00:00
2024-06-07 18:00:00
America/New_York
CSAIL + Imagination in Action Symposium 2024
The symposium will showcase the extraordinary and substantive contributions CSAIL research groups have made, and highlight the remarkable impacts of our work.
Kirsch Auditorium