Abstract

A modern computer system, be a scale-up server or a phone, is a complex mixture of heterogeneous cores, firmware images, management processors, etc. The "de facto" operating system of such a machine, therefore, is itself a large ad-hoc collection of components (of which Linux or MacOS is only one) that have no explicit correctness conditions and in many cases place unwarranted trust in each other. A stream of real-world bugs and vulnerabilities shows that trusting a modern machine is a leap of faith at best. Moreover, the traditional Unix OS abstractions, well-suited to a PDP-11 from 1970, don't match modern hardware at all.

I'll talk about trying to fix this by specifying the hardware/software boundary of entire machines, and then creating something deeply unfashionable since the 1990s: a reference model for OSes that allows us to reason about the correctness of the whole de facto OS with its multiple trust domains. Along the way, I'll mention some side-quests, like finding hardware bugs by using symbolic execution on hardware reference manuals, and the challenge of building a secure board management controller for our own research servers. I'll finish with a roadmap for a new OS architecture, which can incorporate components like Linux but which might actually be trustworthy on real hardware.

Bio: Timothy Roscoe is a Full Professor in the Systems Group of the Computer Science Department at ETH Zurich, where he works on operating systems, networks, and distributed systems.

Mothy received a PhD in 1995 from the Computer Laboratory of the University of Cambridge, where he was a principal designer and builder of the Nemesis OS. After three years working on web-based collaboration systems at a startup in North Carolina, he joined Sprint's Advanced Technology Lab in Burlingame, California in 1998, working on cloud computing and network monitoring. He joined Intel Research at Berkeley in April 2002 as a principal architect of PlanetLab, an open, shared platform for developing and deploying planetary-scale services. Mothy joined the Computer Science Department at ETH Zurich in January 2007, and was named Fellow of the ACM in 2013 for contributions to operating systems and networking research.

His work at ETH has included the Barrelfish multikernel research OS, as well as work on distributed stream processors, and using formal specifications to describe the hardware/software interfaces of modern computer systems. Mothy's current research centers on foundational methodologies for OS design and implementation, and Enzian, a powerful hybrid CPU/FPGA machine designed for research into systems software.