The L4 verification pilot project
L4 is a small and flexible high-performance micro kernel. The core aim of NICTA's Embedded, Real-Time, and Operating Systems program (ERTOS) is to increase the reliability and decrease the cost of embedded software using this kernel.
Ultimately, trustworthiness can only be established by mathematical rigour. For this reason, central long-term goals are the development of a formal model of the kernel, suitable for formal reasoning about software components to be built on top, as well as a formal verification of the implementation of the kernel itself. We have been exploring the feasibility of this goal, based on capabilities existing in the ERTOS and Formal Methods programs in Sydney, and the Logic and Computation program in Canberra.
While L4 is small and simple compared to most other operating systems kernels, it is large and complex compared to most software systems that have been verified at this level of detail in the past. The goal of the pilot project was to develop a better understanding of the problems and risks involved and to identify areas where resources and efforts should be concentrated.
The pilot project consisted of:- a comprehensive literature survey, identifying and formally capturing the exact properties the verified kernel should possess;
- an in-depth feasibility study on the virtual memory subsystem of L4;
- first, abstract formal model of the applications programming interface (API) of the kernel.