Subscribe to the mailing list for updates.
Trustworthy Board Management Controllers
Like any other modern server, Enzian has a Board Management Controller (BMC). We are conducting research into making these systems more trustworthy. Our research follows two main avenues:
- Produce trustworthy BMC components by modeling the aspects of the hardware platform they manage.
- Harden the system to keep these components isolated from less trusted components.
In the first avenue, we are investigating the following:
- We developed a model for the power and clock distribution topology for modern servers, from which we can synthesize correct power sequences for platforms. We are working on using the model at runtime for fault recovery.
- We are developing a specification language for chip-to-chip protocols like I2C. The specifications are model-checked for consistency and we can then generate both software and hardware implementations for an I2C controller from the specifications.
- We are also rethinking the interfaces between various pieces of firmware on the platform.
For the second avenue, we propose an architecture that offers strong isolation between components so that untrusted components like a webserver cannot interfere with the critical components. Our current prototype uses seL4 as a separation kernel. The trusted components we produce with the above methodology run as native components while the rest of the stack runs in a VM. In the case of Enzian, this is OpenBMC but can be any existing BMC stack in principle. For more information about our Trustworthy BMC architecture, check out the talk we gave at the seL4 Summit 2022.
Board Management Controller (BMC)
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 access and firmware updates). They are the hidden centerpiece behind the scene. Although BMCs have absolute power over modern computing platforms, they are not engineered in a rigorous way that warrants the implicit trust that we put in them.
Migration Strategy (Cyber-Retrofit)
Currently, the Enzian BMC is running OpenBMC. While being open source, this still means that any bug in the Linux kernel is now a bug in the root of trust of the server. We propose an architecture with at its heart seL4 as a separation kernel. In the first step, we virtualize OpenBMC on top of seL4. While not offering additional safety or security, this provides us with a migration path: We can now start to reimplement critical components like the power management as native seL4 tasks that are strongly isolated from the untrusted, non-critical components.
Generating Trustworthy Drivers
When we migrate the BMC stack from Linux-based OpenBMC to seL4, a challenge that arises is the lack of drivers. More specifically, we are in lack of trustworthy drivers. To address this issue, we are currently working on a more holistic approach. We specify the entirety of the system—including the driver and parts of the peripherals—and ensure correctness and interoperability of the system at multiple levels through model checking.
We develop Efeu, a framework that allows developers to specify drivers once and to generate both a model and executable drivers from that single specification. The model, after being combined with additional verification code, can be supplied to the SPIN model checker to verify the properties required by the developers at various abstraction levels. As for the executable drivers, Efeu can generate not only one type but two—both software drivers (in C) and hardware drivers (in HDL, Hardware Description Language). Furthermore, Efeu can generate combined software-hardware drivers. Developers specify the split points between the software and the hardware parts, while Efeu generates the interface in between. This enables efficient exploration of trade-offs in driver design space.
We start using Efeu to generate trustworthy I2C drivers. I2C is a low-level communication protocol widely used for communication between BMCs and peripheral devices. Enzian is no exception. However many devices implement their non-standard variations of the I2C protocol.
Publications
-
Generating Trustworthy I2C Stacks Across Software and HardwareMaster's Thesis, ETH Zürich, September 2023
-
Enzian Firmware Resource InterfaceSemester Project, ETH Zürich, February 2023
-
Declarative Dynamic Power ManagementMaster's Thesis, ETH Zürich, September 2022
-
Declarative Power Sequencing using a CPLDBachelor's Thesis, ETH Zürich, February 2022
-
Generating Power Management Code from Declarative DescriptionsBachelor's Thesis, ETH Zürich, October 2021
-
Optimizing Declarative Power SequencingMaster's Thesis, ETH Zürich, September 2021
-
Declarative Power SequencingACM Transactions on Embedded Computing Systems, Volume: 20, Issue: 5s, September 2021
-
Characterization of Interrupt Handling in Board Management ControllersBachelor's Thesis, ETH Zürich, September 2021
-
Towards Trustworthy BMC Software on Modern HardwareMaster's Thesis, ETH Zürich, August 2021
-
A Model-Checked I2C Specification27th International Symposium on Model Checking Software (SPIN 2021), August 2021
-
Real-time Board Management using an FPGABachelor's Thesis, ETH Zürich, April 2021
-
Towards high-assurance Board Management Controller softwareMaster's Thesis, ETH Zürich, March 2021
-
A model-based approach to platform-level power and clock managementBachelor's Thesis, ETH Zürich, August 2020