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 I²C. The specifications are model-checked for consistency and we can then generate both software and hardware implementations for an I²C 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.

Background

Most modern computing platforms are so complex that they need a separate embedded system to manage them and Enzian is no exception. 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). This makes them the root of trust in such systems. Although BMCs have absolute power over modern computing platforms they are not engineered in the rigorous way that warrants the implicit trust that we put in them. In the Trustworthy BMC project we investigate how to design the software stack for BMCs from the ground up with trustworthiness as the principal goal.

Migration Strategy

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 managed by the BMC. We propose an architecture with at its heart seL4 as a separation kernel. In a 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 task that are strongly isolated from the untrusted, non-critical components.

People

1. Daniel Schwyn

   

2. Zikai Liu

   

3. Ben Fiedler

   

4. David Cock

   

5. Timothy Roscoe

   

Publications

1. Generating Trustworthy I²C Stacks Across Software and Hardware
   1. Zikai Liu
   Master's Thesis, ETH Zürich, September 2023
   PDF DOI
2. Enzian Firmware Resource Interface
   1. Pengcheng Xu
   Semester Project, ETH Zürich, February 2023
   PDF DOI
3. Declarative Dynamic Power Management
   1. Roman Meier
   Master's Thesis, ETH Zürich, September 2022
   PDF DOI
4. Declarative Power Sequencing using a CPLD
   1. Manuel Hässig
   Bachelor's Thesis, ETH Zürich, February 2022
   PDF DOI
5. Generating Power Management Code from Declarative Descriptions
   1. Linus Vogel
   Bachelor's Thesis, ETH Zürich, October 2021
   PDF DOI
6. Optimizing Declarative Power Sequencing
   1. Moritz Knüsel
   Master's Thesis, ETH Zürich, September 2021
   PDF DOI
7. Declarative Power Sequencing
   1. Jasmin Schult
   2. Daniel Schwyn
   3. Michael Giardino
   4. David Cock
   5. Reto Achermann
   6. Timothy Roscoe
   ACM Transactions on Embedded Computing Systems, Volume: 20, Issue: 5s, September 2021
   PDF Talk DOI
8. Characterization of Interrupt Handling in Board Management Controllers
   1. Tobias Oberdörfer
   Bachelor's Thesis, ETH Zürich, September 2021
   PDF DOI
9. Towards Trustworthy BMC Software on Modern Hardware
   1. Ben Fiedler
   Master's Thesis, ETH Zürich, August 2021
   PDF
10. A Model-Checked I²C Specification
    1. Lukas Humbel
    2. Daniel Schwyn
    3. Nora Hossle
    4. Roni Haecki
    5. Melissa Licciardello
    6. Jan Schaer
    7. David Cock
    8. Michael Giardino
    9. Timothy Roscoe
    27th International Symposium on Model Checking Software (SPIN 2021), August 2021
    PDF DOI
11. Real-time Board Management using an FPGA
    1. Sarah Tröndle
    Bachelor's Thesis, ETH Zürich, April 2021
    PDF DOI
12. Towards high-assurance Board Management Controller software
    1. Cedric Heimhofer
    Master's Thesis, ETH Zürich, March 2021
    PDF DOI
13. A model-based approach to platform-level power and clock management
    1. Jasmin Schult
    Bachelor's Thesis, ETH Zürich, August 2020
    PDF DOI