Why you can’t trust your system software, and how you might.

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 way of constructing system software, which can incorporate components like Linux but which might actually be trustworthy on real, complex hardware.