A Formally Correct Operating System Kernel 

The L4.verified project asks the following basic research question: is it possible, feasible and economically viable to create software that is proven to be free of errors?

This project will show that it is possible for designers of small core applications or operating system kernels to produce software that is 100% free of implementation errors.

It is known that this can be achieved for simple programs in theory. The problem we are solving is how to apply the same degree of mathematical rigour to complex systems and achieve the same level of ultimate proof for the L4 microkernel environment.

L4.verified is a joint effort of NICTA’s Formal Methods (FM) program, the Embedded, Real-Time and Operating Systems (ERTOS) program, and the Logic & Computation program. The purpose of our research agenda is to reduce the cost and improve the reliability and trustworthiness of embedded systems software.

The project is expected to finish within the next few months.

See also:

Technical Overview
Publications
L4 microkernel
Secure Embedded L4

What will this research achieve?

Users of embedded processors and devices cannot rely on 'eating the pudding' to prove the reliability of software. For some systems like cars and planes, we would like to have proof that the software works before it is ever deployed. Formal proof eliminates a whole category of risk associated with the development of applications. As a consequence, development time is accelerated, costs are reduced and consumer safety is increased.

We use mathematics and machine-assisted proofs. Just as Pythagoras’ theorem is proved in mathematics, we use theorem proving technology to confirm without doubt that a program will behave exactly as its specification promises – no surprises. Not only is this proof executed in rigorous mathematics, it is also machine-checked in the mechanical proof assistant Isabelle/HOL.

Who will benefit?

The research is targeted at developers of software, researchers developing applications and system components in the microkernel environment and certification authorities.

Limitations and Assumptions

A computer program such as the microkernel investigated in the L4.verified project is in its ideal form a construct of logic. About this construct of logic, we can make predictions with the full rigour of mathematics. We can prove that the kernel will never crash, that it will always enforce the selected security policy, and that it can never be subverted by a client program.

Just as is the case in Physics itself, it is when the program is run by a physical machine that the mathematical prediction might diverge from reality. It is important to understand that while absolute predictions can be made about the logic of the program, the same is not true about the physical machine. The main limitations of formal verification are possible behaviours of the computer that are not captured in its formal description. Hardware that malfunctions due to overheating for example, will not be covered by the proof. These limitations are inherent in the problem and are shared by other verification methods such as testing. The L4.verified project uses a very detailed machine model for hardware interaction, and a precise model of the C language to limit such effects, but they cannot be excluded completely. We currently also assume that the compiler produces correct machine code. Although this means that the proof is not absolute, the level of assurance the verification achieves are higher by far than any software certification standard currently used in industry or governments (e.g. Common Criterial EAL7).

Publications/Research team

Please see the technical overview.

Contact

Gerwin Klein