Trustworthy Board Management Controllers

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 principle goal.

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 it’s 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 managment as native seL4 task that are strongly isolated from the untrusted, non-critical components. For more information about our Trustworthy BMC architecture, check out the talk we gave at the seL4 summit 2022.

Trustworthy BMC architecture with different trust levels for components
Trustworthy BMC architecture with different trust levels for components

Our current research focuses on modelling hardware to be able to make strong statements about the behaviour of the software managing it. This reaches from managing the power and clock distribution network to interfaces between components on the board like the CPU and the BMC. Furthermore we are interested in the security of BMCs and how our hardware models enable us to give stronger guarantees than existing designs.


  1. Declarative Dynamic Power Management
    1. Roman Meier
    Master's Thesis, ETH Zürich, September 2022
  2. Declarative Power Sequencing using a CPLD
    1. Manuel Hässig
    Bachelor's Thesis, ETH Zürich, February 2022
  3. Generating Power Management Code from Declarative Descriptions
    1. Linus Vogel
    Bachelor's Thesis, ETH Zürich, October 2021
  4. Optimizing Declarative Power Sequencing
    1. Moritz Knüsel
    Master's Thesis, ETH Zürich, September 2021
  5. 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
  6. Characterization of Interrupt Handling in Board Management Controllers
    1. Tobias Oberdörfer
    Bachelor's Thesis, ETH Zürich, September 2021
  7. Towards Trustworthy BMC Software on Modern Hardware
    1. Ben Fiedler
    Master's Thesis, ETH Zürich, August 2021
  8. A Model-Checked I2C 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
  9. Real-time Board Management using an FPGA
    1. Sarah Tröndle
    Bachelor's Thesis, ETH Zürich, April 2021
  10. Towards high-assurance Board Management Controller software
    1. Cedric Heimhofer
    Master's Thesis, ETH Zürich, March 2021
  11. A model-based approach to platform-level power and clock management
    1. Jasmin Schult
    Bachelor's Thesis, ETH Zürich, August 2020