Towards high-assurance Board Management Controller software

Traditional software running on (base)board management controllers (BMC) is not highassurance. It provides no guarantees about security properties or correctness. This is in stark contrast to the high sensitivity and criticality of many tasks it performs. To this end, we built BMC system software for Enzian, a research platform developed by the Systems Group of ETH Zurich, based on the formally verified microkernel seL4: We designed a statically configured system using CAmkES with which we implemented power management for the main Enzian board. This entailed writing drivers for some devices and replaying bus traffic that was captured ahead of time to configure additional devices. We bring up a selected subset of the power and clock tree and put emergency procedures in place. We evaluated the emergency procedures under different types of synthetic workloads. Good end-to-end response times and sufficient isolation of real-time tasks were observed. The major contribution to the execution time of the emergency procedures was found to come from bus operations. With this work we made the first step towards high-assurance BMC software and demonstrated that seL4 is a viable alternative, offering not only strong guarantees, but also good performance