The University of New South Wales

Trustworthy COTS Hardware

Achievements

The project has uccessfully created a version of seL4 that provides redundant co-execution (RCoE) of an seL4-based system on COTS multicore, i.e. without any non-standard hardware support. It can run in dual or triple modular redundancy (DMR or TMR) configuration.

The replication and fault-tolerance implementation is done at the kernel level, meaning that the whole system is replicated, except for the minimal interfaces to non-replicated devices (mostly device register reads and writes). Our RCoE implementation is the first system that achieves such maximal replication on COTS hardware.

Our RCoE setup comes in two versions:

Both versions are share the following properties:

Status

Having demonstrated the above, the projectis concluded for now. We will be happy to revive it should there be commercial interest.

Artifact downloads

Coming soon!

People

Past

Publications

Abstract PDF Yanyan Shen, Gernot Heiser and Kevin Elphinstone
Fault tolerance through redundant execution on COTS multicores: Exploring trade-offs
International Conference on Dependable Systems and Networks (DSN), pp. 188-200, Portland, Oregon, USA, June, 2019
Abstract PDF Yanyan Shen
Microkernel mechanisms for improving the trustworthiness of commodity hardware
PhD Thesis, UNSW, Sydney, Australia, March, 2019
Abstract PDF Yanyan Shen and Kevin Elphinstone
Microkernel mechanisms for improving the trustworthiness of commodity hardware
European Dependable Computing Conference, pp. 12, Paris, France, September, 2015
Abstract PDF 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