Skip to main content


Microkernel mechanisms for improving the trustworthiness of commodity hardware


Yanyan Shen and Kevin Elphinstone




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

    author           = {Shen, Yanyan and Elphinstone, Kevin},
    month            = sep,
    year             = {2015},
    keywords         = {multicore; kernel; reliability},
    title            = {Microkernel Mechanisms for Improving the Trustworthiness of Commodity Hardware},
    booktitle        = {European Dependable Computing Conference},
    pages            = {12},
    address          = {Paris, France}


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