Generating Trustworthy I²C Stacks Across Software and Hardware

Abstract

Modern computers increasingly offload low-level management to baseboard management controllers (BMCs). While the research community is actively working toward a trustworthy BMC firmware stack, writing efficient and highly-assured device drivers remains a challenge. One such example is creating I²C drivers to accommodate devices that implement non-compatible variations of the communication protocol. Prior research proposes a model-checked I²C specification, from which device drivers can be generated. While the viability of this approach has been demonstrated, there remain several limitations preventing the generated drivers from being useful in real-world applications. In this work, we present Efeu, a framework to synthesize assured and practical drivers from model-checked specifications. Advancing beyond the previous effort, Efeu can generate combined software-hardware drivers, with users freely selecting split points between components and Efeu handling the interface generation. Evaluations on real devices validate the generated I²C stacks. Compared with manually crafted drivers, the generated stacks have a reasonable overhead in performance and resource utilization, while featuring the assurance gained from model checking.