Trustworthy Systems

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

Authors

Anna Lyons and Gernot Heiser

NICTA

UNSW

Abstract

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

  @inproceedings{Lyons_Heiser_14,
    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         = {https://trustworthy.systems/publications/nicta_full_text/8354.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/8354.pdf},
    title            = {Mixed-Criticality Support in a High-Assurance, General-Purpose Microkernel},
    year             = {2014}
  }

Download