Trustworthy Systems

Microkernel mechanisms for improving the trustworthiness of commodity hardware

Authors

Yanyan Shen and Kevin Elphinstone

NICTA

UNSW

Abstract

Trustworthy isolation is required to consolidate safety and security critical software systems on a single hardware platform. Recent advances in formally verifying isolation properties of a microkernel provides a high degree of assurance that mutually distrusting software can co-exist on the same platform. However, commodity hardware is susceptible to transient faults triggered by cosmic rays, alpha particle strikes, temperature variation, and thus may invalidate the isolation guarantees. To increase trustworthiness of commodity hardware, we apply redundant execution techniques from the dependability community to a modern microkernel, to leverage the hardware redundancy provided by multicore processors to perform transient fault detection for applications and for the kernel itself. This paper presents the mechanisms and framework for microkernel-based systems to implement redundant execution for improved trustworthiness. It evaluates the performance of the resulting system on intel and ARM platforms.

BibTeX Entry

  @inproceedings{Shen_Elphinstone_15,
    address          = {Paris, France},
    author           = {Shen, Yanyan and Elphinstone, Kevin},
    booktitle        = {European Dependable Computing Conference},
    keywords         = {multicore; kernel; reliability},
    month            = sep,
    pages            = {12},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8680.pdf},
    title            = {Microkernel Mechanisms for Improving the Trustworthiness of Commodity Hardware},
    year             = {2015}
  }

Download