SOURCE: Open Kernel Labs

January 26, 2011 06:01 ET

Open Kernel Labs Provides OKL4 Verified for Download and Prototyping

Security-Conscious OEMs, Developers, and Researchers Can Now Evaluate the Fully Verified, Bug-Free Kernel for Certified and Secure Mobile/Wireless Applications

CHICAGO, IL--(Marketwire - January 26, 2011) - Open Kernel Labs (OK Labs), the leading provider of embedded virtualization software for mobile phones and broadband internet devices, today announced availability for download of OKL4 Verified (project name seL4), a fully verified, bug-free secure microkernel for business-critical and mission-critical applications in mobile/wireless devices. Security-conscious device manufacturers (OEMs), mobile network operators (MNOs), application developers, researchers, and other interested parties can now download, run, and test OKL4 Verified on embedded ARM11 platforms.

OK Labs previously announced the completion of groundbreaking research by OK Labs, NICTA, and researchers at the University of New South Wales (UNSW), to provide formal mathematical proof of the correctness of the kernel. The verification process used with OKL4 Verified eliminates a wide range of exploitable errors in the kernel, including design flaws and code-based errors like buffer overflows, null pointer dereference, and other pointer errors, memory leaks, and arithmetic overflows and exceptions.

With general availability for download, interested parties can now employ OKL4 Verified for evaluation and prototyping, using available user program libraries and/or a paravirtualized Linux kernel.

"A fully verified, 100% bug-free OS kernel meets pressing needs for greater security in mobile/wireless and other embedded applications," said Steve Subar, Founder and CEO, OK Labs. "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, and represent the best path forward for secure mobile communications."

"The completion of OKL4 Verified has created enormous interest in our unique verification technology," noted Gernot Heiser, Cofounder of Open Kernel 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."

Key Facts

  • OKL4 Verified is the only operating system in existence today whose source code has been mathematically proven to implement its specification correctly
  • OK Labs OKL4 Verified (project name seL4) is the result of more than four years work with NICTA and the University of New South Wales to verify the microkernel as correct and bug-free
  • Device manufacturers, developers, researchers, and other interested parties can now download, run and test the OKL4 Verified microkernel for real-world applications
  • The OKL4 Verified shares underlying technology with the OKL4 Microvisor and the OK Labs mobile virtualization solution, and represents a key part of OK Labs investment in secure mobile communications
  • The download includes bootable images for x86 and ARM11, user-space libraries and other code needed for building applications, paravirtualized Linux running on OKL4 Verified, user documentation, and the formal specification (in Isabelle format and as human-readable PDF)


The OKL4 Verified microkernel is available TODAY for download and execution on:

  • Select ARM11-based evaluation and product boards, including the KZM-ARM11-01 from Kyoto Microcomputer (contact OK Labs for a complete list)
  • X86/PC-AT hardware, as a stand-alone OS
  • X86/PC-AT hardware, hosting execution of paravirtualized Linux

Note: OKL4 Verified is licensed for non-commercial use only. To download OKL4 Verified visit To discuss commercial deployment and to learn more about OKL4 Verified, OKL4, and OK Labs mobile virtualization solutions, visit

About Open Kernel Labs
OK Labs is the global leader in virtualization software for mobile/wireless devices and embedded systems. OK Labs software is deployed on more than 1.1 billion mobile phones worldwide. Semiconductor suppliers, mobile OEMs, and mobile network operators depend on OK Labs to deliver high performance solutions that decrease BOM cost, reduce complexity, and speed time-to-market.

National ICT Australia Ltd (NICTA), Australia's Information and Communications Technology (ICT) Research Centre of Excellence, is developing technologies which will meet the current and future needs of the community in fields which will lead to large economic, social and environmental benefits for Australia. NICTA has five laboratories around the country. Since NICTA was founded in 2002, it has created five new companies, developed a substantial technology and intellectual property portfolio and continues to supply new talent to the ICT industry through the NICTA-enhanced PhD program.

NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program. In addition to federal funding NICTA is also funded and supported by the Australian Capital Territory, New South Wales, Queensland and Victorian Governments, The Australian National University, Griffith University, University of Melbourne, University of New South Wales, University of Queensland, Queensland University of Technology and The University of Sydney.


Download OKL4 Verified:
Verification White Paper:
Open Kernel Labs Blog:
OK Community Portal:
Developer Mailing List:
NICTA Home Page:
UNSW Home Page:

Open Kernel Labs, OK Labs, and Secure HyperCell are trademarks or registered trademarks of Open Kernel Labs or its affiliates in the U.S. and other countries. Other names may be trademarks of their respective owners.

Contact Information