This raises concerns about the reliability and trustworthiness of such systems. In the past, mission- and life-critical embedded systems consisted mostly of simple microcontrollers running a very small amount of software, which could be validated with traditional (informal) means. The strong growth in functionality (and consequently complexity) of these devices makes such validation methods less and less satisfactory. In a nutshell, software complexity is increasing much faster than the power of techniques for ensuring software reliability, leading to an overall degradation of reliability.

This problem of software reliability must be addressed at all levels of the software stack, and with a combination of approaches. In particular, the operating system must be a core part of the approach. Any guarantee of application-software correctness is useless if the application runs on top of a faulty operating system, which can interfere in arbitrary ways with the operation of the application software.

We argue that microkernels form the basis of the only feasible approach with a chance of delivering truly trustworthy computer systems in the foreseeable future. This is the core of the operatingsystems research agenda at NICTA, Australia’s centre of excellence in ICT research. In this paper we present the NICTA OS research vision, an overview of the research agenda that aims to deliver on this vision, and discuss the progress to date and the steps taken to deploy the research outputs for real-world use.

The remainder of this paper is structured as follows. Section 2 presents microkernels, and specifically L4, as a basis for trustworthy embedded systems. This is followed by an overview of the NICTA OS research and commercialisation agenda in Section 3. In particular we focus on four core projects: seL4, L4.verified, Potoroo, and CAmkES. Section 4 compares this research agenda to current related work. We note that while there is activity elsewhere on various subsets of our agenda, none is as comprehensive and ambitious as our projects. Finally Section 5 closes with a summary and conclusions.