Mixed-Criticality Support in a High-Assurance, General-Purpose Microkernel
Anna Lyons, Gernot Heiser · 2014
We explore a model for mixed-criticality support in seL4, a high-assurance microkernel designed for real-world use. Specifically we investigate how the seL4 model can be extended without compromising its security properties and its generalpurpose nature, including high average-case performance. The proposed model introduces reservations, with admission control performed at user level, similar to how seL4 handles spatial resources.