Talk: Timothy Roscoe – A pragmatic but formal approach to building OSes for real computers

Abstract. Modern computers, from mobile phones to servers, rack-scale appliances, and entire data centers, bear almost no resemblance to the DEC PDP-11-derived architecture shown even in modern OS textbooks -- instead, they are complex networks of heterogeneous devices and cores. However, modern OSes (even research systems) are still written to this fictional model from the 1970s, ignoring most of the cores and "system software" running on the machine. This makes the security guarantees the OS tries to provide mostly meaningless, and makes resource allocation across the machine much less efficient. However, replacing these "ad-hoc operating systems" with a clean-slate multikernel design is neither practical (due to the need to support too many devices and existing APIs) nor realistic (since many cores run proprietary system software that cannot be changed). We are exploring a different approach to assembling an OS for a real machine, based on a rigorous model of each particular underlying hardware platform, expressed in a specification language. Above this model we can formally derive the trust relationships between execution contexts, both physical and virtual, and program protection hardware in a provably correct way. This allows us to reuse existing OS components, even if we do not trust its guarantees, and still make strong statements about the security of the OS as a whole. It can also deploy kernels verified for single-core, PDP-11-like architectures and recover properties on real hardware. I'll talk about the kind of OS that comes out of this process, and our early results building such OSes for real computers.

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 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 Enzian, a powerful hybrid CPU/FPGA machine designed for research into systems software.