Enzian at the seL4 Summit 2022

The seL4 Summit took place earlier this month in Munich, and the Enzian team was represented by Daniel Schwyn, giving a talk about Trustworthy BMCs (recording available here).

Why trustworthy BMCs?

Most modern computing platforms are so complex that they need a separate embedded system to manage them. These systems are referred to as (Base-)Board Management Controllers or BMCs. BMCs handle power and clock distribution and sequencing, firmware for other components on the board, and usually offer remote management capabilities (e.g. console and firmware updates). This makes them the root of trust in such systems.

The Enzian servers also have a BMC, which we have previously written about here and here. Our current BMC stack runs what was once intended to be a Python-based prototype for controlling the various voltage and current regulators on the board, on top of OpenBMC, an “embedded” Linux distribution for management devices. Open-source board management controller software already represents a significant improvement over the prior state-of-the-art, which can be summarized as the board manufacturer going “here’s a binary blob that runs at the highest privilege level in your system.”

Thus, we looked into using the formally verified, high-assurance seL4 as a basis for a new BMC design that deserves the trust we put in it. We apply the cyber-retrofit technique used in other seL4-based projects. Using the existing virtual machine manager support present in seL4, we start out by running our existing OpenBMC Linux in a VM. From here, we can pull out critical components one-by-one, reliably isolating them from the rest running in the Linux VM.

There are many ways to make components we break out trustworthy: hardware models for power sequencing increase the safety of our power-on and power-off sequences, we can generate driver code for I2C device-tuned models, or write the code ourselves and verify it using the same tools as the seL4 team.

If you are interested in more details, check out our talk, our associated publications, and get in touch with us.