The project involved NICTA (National Information and Communications Technology Australia), OK Labs' incubator and investor, as well as researchers from the University of New South Wales (UNSW) in Australia, and "other prestigious institutions," says the company. The project's goal was to assure extremely high levels of reliability and security in mission-critical domains that include aerospace and transportation, says OK Labs.
By mathematically proving the correctness of underlying kernel functioning of the microkernel used in the firm's Windows Mobile-ready OKL4 hypervisor, which is primarily designed for mobile phones, the project "paves the way for validating and deploying mobile virtualization under certification and security regimes," says the company. Secure regimes that could use the technology are said to include Common Criteria for business-critical applications in mobile telephony, business intelligence, and mobile financial transactions.
NICTA's verified code base, called the seL4 kernel (secure embedded L4), was derived from the same open source L4 project that spawned OKL4. OK Labs will bring the results of the project, including NICTA's seL4, to market "in future generations of mobile virtualization products."
The proof is in the proof
According to OK Labs, existing certification regimes for hypervisors conform to specifications of models of software, but cannot look into the algorithms to formally prove reliability. These traditional approaches combine code quality tools and certification regimes. The former include tools such as LINT and Coverity, which automatically parse source code, and apply rules and filters, but have no knowledge of underlying algorithms, says OK Labs (see diagram below).
Typical code analysis workflow
Typical certification regimes for safety, security, and standards compliance are human-driven, with computer assistance, says the company. Such regimes tend to use software processes and conformance to written (textual) specifications (see diagram below).
Typical certification regime workflow
The NICTA project, on the other hand, is said to go a step further by proving the correctness of the code itself, using formal logic and programmatic theorem-checking (see diagram below). The verification eliminates exploitable errors in the kernel, including design flaws and code-based errors, says the company. The latter are said to include buffer overflows, null pointer de-reference and other point errors, memory leaks and arithmetic overflows, and exceptions.
NICTA/OK Labs seL4 verification workflow
(Click to enlarge)
Over the last four years, NICTA and UNSW researchers on the project verified 7,500 lines of source code, proving over 10,000 intermediate theorems in over 200,000 lines of formal proof, says OK Labs. The seL4-verified code base, plus the related theorems and testing framework, are being transferred from NICTA to OK Labs as part of their ongoing partnership. OK Labs plans to use these components for comparable verification of OKL4, with the aim of developing a fully-verified commercial successor to OKL4.
OKL4 background
Motorola
Evoke QA4
(Click for details) |
OKL4 version 3.0 can run on 300 million handsets and other mobile and embedded devices, and is available already installed on the Linux-based
Motorola Evoke QA4 (pictured), says OK Labs. OKL4's microkernel OS runs almost everything in userspace, and includes a thin hardware abstraction layer that can support Windows Mobile, Windows CE, Linux, Symbian, and other guest OSes. The OS also includes a minimal POSIX-compliant execution environment, enabling multiple applications and device drivers to run in separate, isolated partitions.
OKL4 provides for decreased BOM (bill of materials), as well as the separation of GPL and proprietary software code as required by companies' intellectual property policies, claims OK Labs. The hypervisor provides sufficient CPU performance to support a Linux environment with a rich GUI in one virtualized compartment, while concurrently supporting real-time phone modem processing software in a separate compartment, says the company.
For example, the Motorola Evoke QA-4 shown above uses OKL4 to deploy two simultaneously running OSes. The phone is said to be the first commercially available handset to offer a virtualization solution that enables Linux and a real-time operating system (RTOS) to run simultaneously on a single ARM processor.
OKL4 3.0 architecture
Last December, OK Labs announced that
OKL4 would support devices using ARM Cortex-A8 and Cortex-A9 MP Core multi-core CPUs.
In early May,
OK Labs and Citrix announced they would deliver the "Citrix Receiver" virtualization client on OKL4. The partnership should let smartphones running Windows Mobile, Linux, Android, and Symbian display secure, virtualized Windows desktop images by the end of the year. The OKL4 version of Citrix Receiver will be targeted primarily at corporate IT departments and their users, who want to access secure corporate data on consumer smartphones, says OK Labs.
Stated Gernot Heiser, OK Labs CTO and John Lions Chair of Operating Systems at UNSW, "The NICTA team has achieved a landmark result which will be a game changer for security- and safety-critical software. The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake."
Stated Steve Subar, president and CEO, OK Labs, "NICTA's groundbreaking research promises to deliver huge benefits to embedded design. We look forward to bringing a secure and verified Microvisor to market in OK Labs virtualization platforms for mobile OEMs, mobile network operators (MNOs), and IT managers building mobile-to-enterprise applications."
Related stories:
