CSE Colloquium – Flux: Refinement Types for Verified Rust Systems

Presenter: Ranjit Jhala, UCSD

Abstract: Rust has risen as a language of choice for new systems code — from OS kernels to hypervisors, firmware and run-times — as it is memory safe and provides the sort of abstractions needed for efficient low-level systems implementation. We present Flux, a refinement type checker for Rust that shows how logical refinements can work in tandem with Rust’s ownership mechanisms to yield ergonomic type-based verification of low-level systems code. We then present a case study showing how Flux was used to formally verify process isolation in Tock: a microcontroller OS used in security-critical systems like the Google Security Chip (GSC) and Microsoft’s Pluton security processor. Our verification effort unearthed multiple subtle bugs that broke isolation, allowing malicious applications to compromise the OS to potentially steal sensitive data or brick or take control of the OS. We describe how Flux helped design and implement a new granular process abstraction that is both simpler, more efficient, and yields formally verified security guarantees.

Ranjit Jhala is a professor of Computer Science and Engineering at the University of California, San Diego. He works on algorithms and tools that help engineer reliable computer systems. His work draws from and contributes to the areas of Model Checking, Program Analysis, and Automated Deduction, and Type Systems. He helped create several influential and award winning systems including the BLAST software model checker and Liquid Types, received ACM SIGPLAN’s Robin Milner Young Researcher Award, and is a Fellow of the ACM.

Hosted by: Professor Mohsen Lesani

Location: Engineering 2, Room E2-180

*Refreshments such as coffee and pastries will be provided.