LONDON Open Kernel Labs has completed long-term research and development to provide formal mathematical proof of the correctness of the microkernel technology underlying OKL4, the company's mobile virtualisation platform.
This project involved National ICT Australia Ltd (NICTA), the company's incubator and investor, OK Labs (Chicago, IL) staff, researchers from the University of New South Wales (UNSW), Australia, and other institutions.
The project entailed four years of work by NICTA and UNSW researchers. The joint team verified 7,500 lines of source code, proving over 10,000 intermediate theorems in over 200,000 lines of formal proof. The verified code base, the seL4 kernel ('secure embedded L4'), derived from the globally developed and deployed open source L4 project (as did OKL4, the OK Labs mobile virtualisation platform).
The outcome of the project ” the seL4 code, theorems, and testing framework ” will be transferred from NICTA to OK Labs as part of the ongoing relationship between the two entities. For its part, OK Labs plans to use the NICTA intellectual property for comparable verification of OKL4, for a fully-verified future commercial product.
As the commercialisation partner for NICTA, OK Labs will bring the results of the project to market in future generations of mobile virtualisation products.
The project centred on the need to assure extremely high levels of reliability and security in mission-critical domains that include aerospace and transportation. By mathematically proving the correctness of underlying kernel functioning, NICTA and OK Labs are paving the way for validating and deploying mobile virtualisation under certification and security regimes like common criteria for business-critical applications in mobile telephony, business intelligence, and mobile financial transactions.
Existing certification regimes centre on software processes and conformance to specifications of models of software. By contrast, says OK Labs, the NICTA project actually proves the correctness of the code itself, using formal logic and programmatic theorem-checking.
The combination results in reliability and security and the verification eliminates a range of exploitable errors in the kernel, including design flaws and code-based errors like buffer overflows, null pointer dereference and other point errors, memory leaks and arithmetic overflows, and exceptions.
Related links and articles:
The paper on this research can be found here.