Trustworthy Systems

Improving the trustworthiness of commodity hardware with software

Authors

Kevin Elphinstone and Yanyan Shen

NICTA

UNSW

Abstract

Abstract—Advances in formal software verification has pro- duced an operating system that is guaranteed mathematically to be correct and enforce access isolation. Such an operating system could potentially consolidate safety and security critical software on a single device where previously multiple devices were used. One of the barriers to consolidation on commodity hardware is the lack of hardware dependability features. A hardware fault triggered by cosmic rays, alpha particle strikes, etc. potentially invalidates the strong mathematical guarantees. This paper discusses improving the trustworthiness of com- modity hardware to enable a verified microkernel to be used in some situations previously needing separate computers. We explore leveraging multicore processors to provide redundancy, and report the results of our initial performance investigation.

BibTeX Entry

  @inproceedings{Elphinstone_Shen_13,
    address          = {Budapest, Hungary },
    author           = {Elphinstone, Kevin and Shen, Yanyan},
    booktitle        = {Workshop on Dependability of Clouds, Data Centers and Virtual Machine Technology (DCDV)},
    keywords         = {multicore; kernel; reliability},
    month            = jun,
    pages            = {6},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6840.pdf},
    title            = {Improving the Trustworthiness of Commodity Hardware with Software},
    year             = {2013}
  }

Download