October 23, 2023
- 08:30 - 08:35 Opening remarks
- 08:35 - 09:35 Keynote by Chris Hawblitzel (Microsoft). Verus: Fast Formal Verification of Rust Programs Using Ownership and Automated Theorem Proving.
Session 1: Operating Systems
-
09:35 - 09:55 Leveraging Rust for Lightweight OS Correctness. Ramla Ijaz (Yale University), Kevin Boos (Theseus Systems), Lin Zhong (Yale University)
-
09:55 - 10:15 Atmosphere: Towards Practical Verified Kernels in Rust. Xiangdong Chen (University of Utah), Zhaofeng Li (University of Utah), Vikram Narayanan (University of Utah), Anton Burtsev (University of Utah)
10:15 - 10:40 Coffee break
Session 2: Hardware
-
10:40 - 11:00 Specifying the de-facto OS of a production SoC. Ben Fiedler (ETH Zurich), Roman Meier (ETH Zurich), Jasmin Schult (ETH Zurich), Daniel Schwyn (ETH Zurich), Timothy Roscoe (ETH Zurich)
-
11:00 - 11:20 The K2 Architecture for Modular Hardware Security Modules. Anish Athalye (MIT), Frans Kaashoek (MIT), Nickolai Zeldovich (MIT), Joseph Tassarotti (New York University)
Session 3: Secure Interfaces
-
11:20 - 11:40 CIVSCOPE: Analyzing Potential Memory Corruption Bugs in Compartment Interfaces by Establishing Lower Bound and Upper Bound. Yi Chien (Rice University), Vlad-Andrei Bădoiu (University Politehnica of Bucharest), Yudi Yang (Rice University), Yuqian Huo (Rice University), Kelly Kaoudis (Trail of Bits), Hugo Lefeuvre (The University of Manchester), Pierre Olivier (The University of Manchester), Nathan Dautenhahn (Rice University)
-
11:40 - 12:00 Encapsulated Functions: Fortifying Rust’s FFI in Embedded Systems. Leon Schuermann (Princeton University), Amit Levy (Princeton University), Arun Thomas (zeroRISC Inc.)