News

• Benjamin Morgan (University of Warwick (GB))
• Michael Bussmann
• Maria Girone (CERN)
• Graeme A Stewart (CERN)
• Stefan Roiser (CERN)

A Formal but Pragmatic Foundation for General-Purpose Operating Systems

• Timothy Roscoe (ETHZ)

The Operating System (OS) is fundamental to the correct working of any non-trivial computer system, and general-purpose OSes like Linux (and Android), Windows, iOS and MacOS are the central component of the infrastructure of modern computing and communications, from mobile phones to cloud providers. Modern AI would not be possible without OS software providing required scaling and communication between distributed tasks. Faults attributable to OS flaws have serious consequences ranging from security breaches to global-scale outages. Despite this, general-purpose OS design and implementation today remains surprisingly ad-hoc, based on a simplistic architecture proposed decades ago for machines designed in 1970s. Since then, system hardware has changed beyond recognition: computers are complex networks of cores, devices, management engines, and accelerators, all running code ignored by the nominal OS. This broad disconnect between hardware reality and OS structure underlies many security and reliability flaws, and will not go away without a radical change in approach. I'll talk about our attempts to put general-purpose OS development on a solid foundation for the first time, based on a formal framework for capturing the software-visible semantics of all the hardware in complete, real computers. Above this, we are working on tooling to assemble an OS for modern heterogeneous servers and systems-on-chip which can incorporate existing drivers, firmware, and application environments, but nevertheless offer strong, formal platform-wide guarantees of application isolation and security. 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.