OK Labs announced the availability of a verified, “bug-free secure microkernel” version of its Linux-compatible OKL4 hypervisor. Currently downloadable free for non-commercial evaluation on embedded ARM11 or x86 platforms, the “OKL4 Verified” microkernel is designed for business-critical and mission-critical applications in mobile/wireless devices, says the company.

In August 2009, OK Labs (Open Kernel Labs) announced the completion of a "sel4" research project, intended to provide formal mathematical proof of the correctness of the microkernel used in the firm's Linux-ready OKL4 hypervisor. The research was conducted with 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.

NICTA's verified code base, now called OKL4 Verified, was derived from the same open source L4 project that spawned OKL4, says OK Labs. The verification process used with OKL4 Verified eliminates a wide range of exploitable errors in the kernel, says the company. These are said to include design flaws and code-based errors like buffer overflows, null pointer dereference, and other pointer errors, memory leaks, and arithmetic overflows and exceptions.

The proven microkernel enables the validation and deployment of mobile virtualization schemes under certification and security regimes, says OK Labs. Secure regimes might include Common Criteria for business-critical applications in mobile telephony, business intelligence, and mobile financial transactions.

OKL4 Verified is now available for download, using available user program libraries and/or a paravirtualized Linux kernel, says OK Labs. The download includes bootable images for x86 and ARM11, user-space libraries, and other code needed for building applications. Also included is a paravirtualized Linux distribution running on OKL4 Verified, as well as user documentation, and the formal specification. 

OK Labs offers an approved list of ARM11-based evaluation and product boards, but appears to recommend the Kyoto Microcomputer KZM-ARM11-01 (pictured), which runs Linux 2.6 on an ARM11 i.MX31 from Freescale Semiconductor.

For x86 evaluation, OKL4 Verified can run as a standalone OS on X86/PC-AT hardware, as a stand-alone OS in paravirtualized Linux mode, says the company.

OKL4 background

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.

In October, OK Labs announced an "ObamaBerry"-like smartphone security solution for open source mobile platforms, based on the company's OKL4 mobile virtualization technology. Available initially for Android, SecureIT Mobile combines software and services that will let governmental agencies, contractors, integrators, and OEMs build secure devices using commercial off-the-shelf hardware and software, said the company.

Stated Steve Subar, founder and CEO, OK Labs, "A fully verified, 100% bug-free OS kernel meets pressing needs for greater security in mobile/wireless and other embedded applications. The confidence and reliability conferred by OKL4 Verified and its underlying technology enable an array of highly secure and certifiable applications on mobile/wireless devices."

Stated Gernot Heiser, co-founder of OK Labs, leader of Trustworthy Embedded Systems at NICTA, and John Lions Professor at UNSW, "As the first operating system kernel proved to never operate out-of-spec, OKL4 Verified presents a truly trustworthy base for security- and safety-critical applications across a wide range of application domains."

Availability

The OKL4 Verified microkernel is now available for free download for non-commercial use only. (Contact OK Labs for commercial deployment terms.) Downloads may be found on OK Labs' OKL4 Verified page. A white paper on OKL4 Verified may be found in this PDF.

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.