Skip to main content


Improving the trustworthiness of commodity hardware with software


Kevin Elphinstone and Yanyan Shen




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

    author           = {Elphinstone, Kevin and Shen, Yanyan},
    month            = jun,
    year             = {2013},
    keywords         = {multicore; kernel; reliability},
    title            = {Improving the Trustworthiness of Commodity Hardware with Software},
    booktitle        = {Workshop on Dependability of Clouds, Data Centers and Virtual Machine Technology (DCDV)},
    pages            = {6},
    address          = {Budapest, Hungary }


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.