
Open access
Author
Date
2021Type
- Master Thesis
ETH Bibliography
yes
Altmetrics
Abstract
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. Show more
Permanent link
https://doi.org/10.3929/ethz-b-000490635Publication status
publishedPublisher
ETH ZurichOrganisational unit
03757 - Roscoe, Timothy / Roscoe, Timothy
More
Show all metadata
ETH Bibliography
yes
Altmetrics