The most widely deployed mobile virtualization solution
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.”
The OKL4 Verified microkernel is available TODAY for download and execution on:
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**
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.
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: 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.
+1 408 828 2861
Open Kernel Labs
+1 312 933 0101