Putting out the hardware dumpster fire

The immense hardware complexity of modern computers, both mobile phones and datacenter servers, is a seemingly endless source of bugs and vulnerabilities in system software. Classical OSes cannot address this, since they only run on a small subset of the machine. The issue is interactions within the entire ensemble of firmware blobs, co-processors, and CPUs that we term the de facto OS. The current "whaca-mole" approach will not solve this problem, nor will cleanslate redesign: it is simply not possible to replace some firmware components and the engineering effort is too great. Our response, instead, is to build a high-level model of exactly what a given real hardware and software platform consists of, and captures for the first time the necessary and assumed trust relationships between the software contexts executing on different components (CPUs, devices, etc.). This principled but pragmatic approach allows us to make rigorous statements about the hodgepodge of soft- and firmware at the heart of modern computers. We expect these statements to be, at first, depressingly weak, but it may be the only way to identify changes that provably increase the trustworthiness of a real system, and quantify the benefits of these changes.