Trustworthy Systems

Mixed-criticality support in a high-assurance, general-purpose microkernel


Anna Lyons and Gernot Heiser




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 general- purpose 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.

BibTeX Entry

    address          = {Rome, Italy},
    author           = {Lyons, Anna and Heiser, Gernot},
    booktitle        = {Workshop on Mixed Criticality Systems},
    editor           = {{Rob Davis and Liliana Cucu-Grosjean}},
    keywords         = {mixed criticality, real time, microkernels, sel4, scheduling},
    month            = dec,
    pages            = {9--14},
    paperurl         = {},
    slides           = {},
    title            = {Mixed-Criticality Support in a High-Assurance, General-Purpose Microkernel},
    year             = {2014}