Modern hardware abstractions for firmware

Abstract

Operating systems inevitably make assumptions about the hardware execution environment. These assumptions influence the design of application programming interfaces (APIs), internal data structures, as well as the hardware model in verified operating systems. Due to the growing hardware diversity and complexity, these assumptions get violated often. This leads to hard-to-port operating systems, APIs that leak underlying implementation details and can invalidate the guarantees of verified operating systems. This dissertation revisits the assumptions about two critical, widely used but often overlooked subsystems: The interrupt delivery subsystem and I2C, a low-speed configuration bus, that is used to interact with actors and sensors, including critical ones such as voltage regulators. For both of these subsystems, we propose two new well-specified abstractions built on a formal model. These subsystems have grown in diversity: A general-purpose operating system has to support interrupt controllers from multiple vendors, understand interrupt delivery of many different subsystems and perform configuration of these controllers. Each subsystem offers different ways of delivering interrupts. Hardware virtualization support of device pass-through adds another layer of complexity, as interrupts can be targeted directly to virtual machines. We present a formalization of the interrupt network that includes configurability, a crucial component as controllers vary widely in their configuration options. We refine this model until it is suitable for constraint solving and show its generality by expressing 24 real interrupt controllers in this model. We then use this solver-based approach to configure the interrupt system of a real operating system, Barrelfish. Existing approaches in commodity operating systems, like Linux and FreeBSD, rely on heuristics to configure interrupts. By nature, these approaches will overlook configuration options. Our approach does not rely on heuristics and finds optimal results. Furthermore, it represents the current configuration in a formally defined way. We show that the overhead of solving the configuration problem with a constraint solver is negligible in comparison to driver startup and that the approach scales well in a typical scenario. I2C attached devices are widely used for critical tasks such as controlling voltages, sensing temperatures, and storing persistent device configurations. The standard is written in natural language and leaves ambiguities to device developers. Thus, the bus is plagued with incompatibilities between host interfaces and devices. The few existing formalizations of I2C do not incorporate partially compliant devices. In practice, these hardware controllers are often replaced by an inefficient software-only approach. To tackle this I2C device diversity, we present a modular formalization of I2C and a framework for verifying device driver interactions. We use model-checking to show equivalence to an abstract layer specification. Model-checking was chosen to minimize the developer effort, but the approach is formulated in a tool-agnostic model. Partially compliant devices can be expressed in this framework by interfacing with a different layer. These layers are fine-grained, which enables partially compliant devices to be expressed with little developer effort. Device and driver models are expressed in a custom language that can automatically generate C code, Promela, and Verilog. The generated code results in compact, low-overhead implementations. The code for interacting with a partially compliant device is comparable in complexity to existing approaches, but guarantees correct interaction with a device model, offers automatic code generation, and easier to understand error reporting.