• About

• Leadership Team
• Press Releases
• Press Articles
• Events
• Awards
• Careers
• Contact

Open Kernel Labs Provides OKL4 Verified for Download and Prototyping

• Share:
• Email
• Print
• Twitter
• Facebook

January 26, 2011

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

Chicago – January 26, 2011 - Open Kernel Labs (Open Kernel 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.

Open Kernel Labs previously announced the completion of groundbreaking research by Open Kernel 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, Open Kernel 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, co-founder of Open Kernel Labs, Leader of Trustworthy Embedded Systems at NICTA, and Scientia Professor and John Lions Chair 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
• Open Kernel 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 Open Kernel Labs mobile virtualization solution, and represents a key part of Open Kernel 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)

Availability

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 Open Kernel 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 http://www.ok-labs.com/registrations/software-EULA. To discuss commercial deployment and to learn more about OKL4 Verified, OKL4, and Open Kernel Labs mobile virtualization solutions, visit http://www.ok-labs.com.
**OKL4 Verified Updated on January 28, 2011**

About Open Kernel Labs

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

About NICTA

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.

Links

Download OKL4 Verified: http://www.ok-labs.com/registrations/software-EULA
Verification White Paper: http://www.ok-labs.com/whitepapers/sample/sel4-formal-verification-of-an-os-kernel
Open Kernel Labs Blog: http://www.ok-labs.com/community/company-blog 
OK Community Portal: http://www.ok-labs.com/community/community-portal 
Developer Mailing List: http://www.ok-labs.com/community/mailing-list-signup 
NICTA Home Page: http://www.nicta.com.au 
UNSW Home Page: http://www.unsw.edu.au/ 

Open Kernel Labs, Open Kernel 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. All other trademarks and registered trademarks are property of their respective owners.

CONTACT:
Trish Colby    
LinuxPundit.com    
+1 408 828 2861    
trish@linuxpundit.com

« View All Press Releases