Towards high-assurance Board Management Controller software
OPEN ACCESS
Loading...
Author / Producer
Date
2021
Publication Type
Master Thesis
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Editor
Contributors
Book title
Journal / series
Volume
Pages / Article No.
Publisher
ETH Zurich
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03757 - Roscoe, Timothy / Roscoe, Timothy