Skip to main content


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

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


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.