CS Talk
Leonid Ryzhyk
Title: Rigorous OS Design: an Idea Whose Time Has Come
Hosts: Zhong Shao and Ruzica Piskac
Abstract: Modern operating systems consist of millions lines of low-level code, which is hard to understand, maintain, and validate. In this talk I will advocate the rigorous approach to OS design as a way to overcome the problem. I argue that the time has come to re-think the OS design based on a solid mathematical foundation. This long-sought vision is finally becoming feasible due to recent advances in programming languages, model checking, and interactive theorem proving. I will outline a high-level methodology for rigorous OS design, consisting of three components: (1) a theoretical foundation for formal reasoning about OS behavior at a level of abstraction much higher than C code, (2) a software ecosystem, consisting of domain-specific languages and tools that provide a programmer-friendly interface to the theory, (3) OS implementation, built and verified on top of this ecosystem.
As a concrete instantiation of this methodology, I will present the Termite project, which has developed the first tool for automatic synthesis of correct-by-construction device drivers. In Termite, the driver behavior is formalized in terms of the discrete control theory and is automatically synthesized using controller synthesis techniques. I will show how the connection to the control theory enables efficient formal reasoning about complex low-level software. The talk will conclude with a brief demo of Termite.
Bio: Leonid Ryzhyk is a postdoctoral researcher in the Carnegie Mellon University School of Computer Science. Leonid’s research focuses on operating systems and in particular using formal methods to build better operating systems. He received his PhD from the University of New South Wales in 2010. Prior to joining CMU, Leonid worked as a researcher at NICTA and a postdoctoral fellow at the University of Toronto.