Generating Trustworthy Hardware/Software I2C Drivers for Board Management Controllers - Zikai Liu

Generating Trustworthy Hardware/Software I2C Drivers for Board Management Controllers - Zikai Liu

At the heart of every modern server platform sits an embedded system called the board management controller (BMC) that is responsible for the low-level functioning of the platform. Despite their critical nature, they are generally not built as trustworthy systems. We have embarked on a journey to cyber-retrofit BMC firmware with seL4 as the kernel. In this talk, we present an update on our efforts -- generate trustworthy hardware/software I2C drivers. I2C is a low-level protocol used by BMCs to communicate with many peripherals(e.g. the power regulators). Unlike memory-mapped devices with one-to-one interfaces with the BMC, multiple I2C devices may share the same bus. Quirks of one device can influence the whole assemblage. Therefore, to produce a correct driver for I2C (and other bus-based protocols), we need to consider the specifications of not only the controller but all devices on the bus.

We present Efeu, a framework that allows us to specify both the host-side driver and the peripherals. The specifications are composed of layers, which enable efficient modeling of different devices (including those with quirks). The entire system is then model-checked using SPIN to ensure interoperability. From that, Efeu generates trustworthy drivers in software and hardware. The software implementations target seL4, but could also address other operating systems. Furthermore, when I2C communication speed or CPU usage is a concern, Efeu allows generating hybrid hardware/software drivers, where the hardware part can be materialized on programmable hardware such as Field Programmable Gate Arrays (FPGAs). We evaluated Efeu-generated I2C stacks on a Zynq MPSoC and show that model-checking the whole system and generating the full stack is not only practical but that the resulting implementations can saturate the I2C bus and achieve competitive performance with off-the-shelf solutions.