Embedded virtualization vendor Open Kernel Labs (OK Labs) announced the completion of a four-year research project aimed at developing a highly secure, “100 percent bug-free” hypervisor for mobile phones. The “seL4” project developed a formal mathematical proof of the correctness of the microkernel used by OK Labs' Linux-compatible OKL4, the company says.

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 Linux-ready OKL4 hypervisor, which is primarily designed at 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 LINTand 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, as well as 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)

The Linux-ready OKL4 version 3.0 is available in 300 million handsets and other mobile and embedded devices, including 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 Linux, Windows Mobile, Windows CE, Symbian, and/or other guest OSes. It 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 Linux, Android, Symbian, and Windows Mobile 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.

In June, OK Labs announced an Android version of OKL4. OK:Android is billed as an off-the-shelf, paravirtualized version of Android that enables Android to run as a guest OS in a secure "hypercell" alongside another phone OS.

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."

---

This article was originally published on LinuxDevices.com and has been donated to the open source community by QuinStreet Inc. Please visit LinuxToday.com for up-to-date news and articles about Linux and open source.