Trustworthy Systems

Towards high-assurance multiprocessor virtualisation

Authors

Michael von Tessin

NICTA

UNSW

Abstract

Virtualisation is increasingly being used in security-critical systems to provide isolation between system components. Being the foundation of any virtualised system, hypervisors need to provide a high degree of assurance with regards to correctness and isolation. Microkernels, such as seL4, can be used as hypervisors. Functional correctness of seL4's uniprocessor C implementation has been formally verified. The framework employed to verify seL4 is tailored to facilitate reasoning about sequential programs. However, we want to be able to use the full power of multiprocessor/multicore systems, and at the same time, leverage the high assurance seL4 already gives us for uniprocessors.

This work-in-progress paper explores possible multiprocessor designs of seL4 and their amenability to verification. For the chosen design, it contributes a formal multiprocessor execution model to lift seL4's uniprocessor model and proofs into a multiprocessor context using only minor modifications. The theorems proving the validity of the lift operation are machine-checked in Isabelle/HOL and walked-through in the paper.

BibTeX Entry

  @inproceedings{vonTessin_10,
    address          = {Edinburgh, UK},
    author           = {von Tessin, Michael},
    booktitle        = {6th International Verification Workshop},
    editor           = {{Markus Aderhold, Serge Autexier and Heiko Mantel}},
    issn             = {2040-557X},
    keywords         = {formal verification, multiprocessor, microkernel, virtualisation, sel4, isabelle/hol},
    month            = jul,
    pages            = {110--125},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/3849.pdf},
    publisher        = {EasyChair},
    slides           = {https://trustworthy.systems/publications/nicta_slides/3849.pdf},
    title            = {Towards High-Assurance Multiprocessor Virtualisation},
    year             = {2010}
  }

Download