Towards Trustworthy Computing Systems: Taking Microkernels to the Next Level", Operating Systems Review

As computer systems become increasingly mission-critical, used in life-critical situations, and relied upon to protect intellectual prop-erty, operating-system reliability is becoming an ever growing con-cern. In the past, mission- and life-critical embedded systems con-sisted of simple microcontrollers running a small amount of soft-ware that could be validated using traditional and informal tech-niques. However, with the growth of software complexity, tradi-tional techniques for ensuring software reliability have not been able to keep up, leading to an overall degradation of reliability. This paper argues that microkernels are the best approach for deliv-ering truly trustworthy computer systems in the foreseeable future. It presents the NICTA operating-systems research vision, centred around the L4 microkernel and based on four core projects. The seL4 project is designing an improved API for a secure microker-nel, L4.verified will produce a full formal verification of the micro-kernel, Potoroo combines execution-time measurements with static analysis to determine the worst case execution profiles of the ker-nel, and CAmkES provides a component architecture for building systems that use the microkernel. Through close collaboration with Open Kernel Labs (a NICTA spinoff) the research output of these projects will make its way into products over the next few years. 1