ABSTRACT

We present a case study formally verifying process isolation in the Tock production microcontroller OS kernel. Tock combines hardware memory protection units and language-level techniques—by writing the kernel in Rust—to enforce isolation between user and kernel code. Our effort to verify Tock's process abstraction unearthed multiple, subtle bugs that broke isolation—many allowing malicious applications to compromise the whole OS. We describe this effort and TickTock, our fork of the Tock operating system kernel that eliminates isolation bugs by construction. TickTock uses Flux, an SMT-based Rust verifier, to formally specify and verify process isolation for all ARMv7-M platforms Tock supports and for three RISC-V 32-bit platforms. Our verification-guided design and implementation led to a new, granular process abstraction that is simpler than Tock's, has formal security guarantees (that are verified in half a minute), and outperforms Tock on certain critical code paths.

BIO

Vivien Rindisbacher is a PhD student in the Programming Systems Group at the University of California, San Diego, where they are advised by Deian Stefan and Ranjit Jhala.

Their research lies at the intersection of programming languages and security, with a focus on pragmatic verification. Ultimately, they want their work to meaningfully reduce the number of bugs that exist in code.

Prior to joining UC San Diego, Vivien worked as a Software Engineer at Dimensional Fund Advisors. They completed their undergraduate studies at Boston University, where they worked on formally verifying algorithms for differential privacy with Professor Marco Gaboardi (Boston University) and Professor Arthur Azevedo de Amorim (Rochester Institute of Technology).