A modern computer system\, be a scale-up server or a phone\ , is a complex mixture of heterogeneous cores\, firmware images\, manageme nt processors\, etc. The "de facto" operating system of such a machine\, therefore\, is itself a large ad-hoc collection of components (of which Li nux 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-wo rld bugs and vulnerabilities shows that trusting a modern machine is a lea p of faith at best. Moreover\, the traditional Unix OS abstractions\, wel l-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 t o 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 findi ng 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 archite cture\, which can incorporate components like Linux but which might actual ly be trustworthy on real hardware.
Bio: Timothy Roscoe i s a Full Professor in the Systems Group of the Computer Science Department at ETH Zurich\, where he works on operating systems\, networks\, and dist ributed systems.
Mothy received a PhD in 1995 from the C omputer Laboratory of the University of Cambridge\, where he was a princip al designer and builder of the Nemesis OS. After three years working on w eb-based collaboration systems at a startup in North Carolina\, he joined Sprint's Advanced Technology Lab in Burlingame\, California in 1998\, work ing on cloud computing and network monitoring. He joined Intel Research a t Berkeley in April 2002 as a principal architect of PlanetLab\, an open\, shared platform for developing and deploying planetary-scale services. M othy joined the Computer Science Department at ETH Zurich in January 2007\ , and was named Fellow of the ACM in 2013 for contributions to operating s ystems and networking research.
His work at ETH has inclu ded the Barrelfish multikernel research OS\, as well as work on distribute d stream processors\, and using formal specifications to describe the hard ware/software interfaces of modern computer systems. Mothy's current rese arch centers on foundational methodologies for OS design and implementatio n\, and Enzian\, a powerful hybrid CPU/FPGA machine designed for research into systems software.