Trustworthy Systems

Kernel design for isolation and assurance of physical memory

Authors

Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone

NICTA

UNSW

Abstract

Embedded systems are evolving into increasingly complex software systems. One approach to managing this software complexity is to divide the system into smaller, tractable components and provide strong isolation guarantees between them. This paper focuses on one aspect of the system’s behaviour that is critical to any such guarantee: management of physical memory resources.

We present the design of a kernel that has formally demonstrated the ability to make strong isolation guarantees of physical memory. We also present the macro-level performance characteristics of a kernel implementing the proposed design.

BibTeX Entry

  @inproceedings{Elkaduwe_DE_08,
    address          = {Glasgow, UK},
    author           = {Elkaduwe, Dhammika and Derrin, Philip and Elphinstone, Kevin},
    booktitle        = {Workshop on Isolation and Integration in Embedded Systems},
    isbn             = {978-1-60558-126-2},
    keywords         = {isolation, sel4, memory management, embedded systems, microkernels},
    month            = apr,
    pages            = {35--40},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/848.pdf},
    publisher        = {ACM},
    title            = {Kernel design for isolation and assurance of physical memory},
    year             = {2008}
  }

Download