NICTA’s recent Techfest in Sydney saw a flurry of news around the announcement of a significant research achievement- the formal verification of the seL4 microkernel. The team developed a mathematical proof of the functional correctness of the microkernel down to the level of the C source code.
The achievement is important for two reasons. Firstly, it makes it possible to prove code-level functional correctness of whole computer systems based on the L4 microkernel. This means computer systems can carry a new kind of assurance, supporting strong arguments for safety and security for high-integrity software systems.
Secondly, it makes the creation of these proofs more feasible in practice. It should now be possible to formally verify properties of whole systems where only the key parts of the system are formally verified. This is critical for the practical application of formal verification. The verification of the L4 microkernel took more than 20 person years of effort to verify just 7500 lines of C source code. Modern embedded computer systems can have millions of lines of source – it’s not practical to formally verify all the code in such systems at these levels of productivity.
However, you don’t need to verify all the code! L4 provides rigorous separation between processes running in the microkernel, and that separation is guaranteed by the recent proof. If you can isolate the safety-critical or security-critical parts of an entire system to one small formally verified component running in an L4 process, it should be possible to lift the guarantees for that component to the whole system, even if the other components in the system haven’t been verified.
That is the challenge for a new project at NICTA – Trustworthy Embedded Systems. The plan is to develop technologies to support the creation and verification of entire systems running on top of the microkernel. This is a large project involving several NICTA labs and researchers from many disciplines (operating systems, formal methods, software architecture). I’m part-allocated to the project for the next few years. My PhD was in formal methods, and this is really the first time I’ve dipped my toe back into that area for the last decade. However, I won’t be doing too much theorem proving myself – my focus in the project will instead largely be on other software engineering issues in this context, such as configuration management, and how to use the component architecture to support product line development.