Trustworthy COTS Hardware
Aim: develop software approaches to improving the trustworthiness of commercial off-the-shelf (COTS) hardware.
Overview: The formal verification of the seL4 microkernel has produced an operating system that is guaranteed mathematically to be correct and enforce isolation. The seL4 microkernel can consolidate safety and security critical software on a single device where previously multiple devices were used to provide air gap isolation. One of the barriers to wide-spread consolidation on commodity hardware is the lack of hardware dependability features. A hardware fault triggered by cosmic rays, alpha particle strikes, etc. could invalidate the strong mathematical guarantees that are based on the hardware behaving correctly, and pierce the virtual air gap seL4 provides.
This project aims to improve the trustworthiness of commodity hardware to enable a verified microkernel to be used in situations previously needing an air gap. We explore leveraging multicore processors to provide redundancy, and thus increase the trustworthiness of a virtual air gap, and thus systems running on COTS hardware.
The key challenge of the approach is to provide improved trustworthiness in the presence of transient hardware faults that also manifest themselves in operating system itself, while retaining good performance. A typical COTS hardware platform also features non-redundant devices, which creates another challenge of improving trustworthiness in the presence of non-redundant device drivers interacting with a redundant overall system.
Kernel implementation and mechanisms for improved trustworthiness: We are evolving seL4 and its API to support both improved trustworthiness through redundant software execution on multicore processors. The activity includes:
- Modifying seL4 to support redundant execution of itself, including developing techniques to ensure consistency across redundant replicas without sacrificing performance.
- Extending seL4's API to enable consistent redundant execution of trusted applications, while supporting non-redundant drivers and their interaction with the redundant part of the system.
Contact: Kevin Elphinstone, kevin.elphinstone<at>nicta.com.au
|Yanyan Shen and Kevin Elphinstone|
Microkernel mechanisms for improving the trustworthiness of commodity hardware
European Dependable Computing Conference, pp. 12, Paris, France, September, 2015
|Kevin Elphinstone and Yanyan Shen|
Improving the trustworthiness of commodity hardware with software
Workshop on Dependability of Clouds, Data Centers and Virtual Machine Technology (DCDV), pp. 6, Budapest, Hungary , June, 2013