Need a bug-free system?
Formal, mathematical proof.
Unrecoverable fatal errors, the ones that require you to manually switch off the machine, occur when buggy or malicious code makes a faulty access to a resource. The aim of a microkernel-based system is to reduce the amount of code that has full access to the resources to a minimal core: the microkernel. The rest of the operating system, together with the applications, has to go through the microkernel to access resources. Formal, mathematical proof is the only method that can give us full assurance that the microkernel is not faulty and will never crash.
This is the challenge that was successfully undertaken by Gerwin Klein and his L4.verified team at the National ICT Australia (NICTA), Australia's world-class information and communications technology (ICT) research Centre of Excellence, in which UNSW Australia is a founding partner. The L4.verified project, together with another project called seL4, have built the first high-performance, secure microkernel that is formally verified to the binary code level.
The seL4 (secure embedded L4) microkernel team, headed by Kevin Elphinstone, builds on the strengths of the L4 microkernel architecture (such as its small size and high performance) and extends it with secure access control to resources. The L4.verified verification work provides a mathematical, machine-checked proof that the 8,700 lines of C code in seL4 do exactly what they are intended to do.
This represents an impressive break-through in what can be guaranteed of security and safety-critical software. So far, verification of these systems was done either only on abstract high-level models of the system or on code of very limited size. This project is showing that it is possible, feasible and economically viable to produce software that is 100 percent free of C implementation errors. In 2013, in collaboration with the University of Cambridge, UNSW and NICTA PhD student Thomas Sewell extended this verification to reach from the C code down to the binary level. This means the proof now also provides assurance about the output of the compiler.
In the meantime, the team further extended the proof to cover not only correctness, but also high-level security properties: access control integrity and confidentiality. Together these mean that the kernel can strongly isolate untrusted applications from each other, such that any mistake in one cannot have any effect on any other. This makes seL4 the first OS microkernel in the world that provably enforces such an access control mechanism at the implementation level.
One key aspect to the success of the project is bringing together a team of both Operating System and Formal Methods experts, mainly built through UNSW's Advanced Topics in Software Verification and Advanced Operating Systems courses.
The outcomes of the project are available commercially as the product OKL4:verified from NICTA spin-out Open Kernel Labs. OKL4:verified is the next generation of Open Kernel Labs' current main product OKL4 which is deployed in over 1.5 billion devices around the world. The microkernel itself and its formal specification are available free of charge from Open Kernel Labs for academic research and teaching as well as for evaluation purposes.
The verified microkernel proposed in this project represents a very clear competitive advantage for companies like Open Kernel Labs.