“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.”
LinuxToday is a trusted, contributor-driven news resource supporting all types of Linux users. Our thriving international community engages with us through social media and frequent content contributions aimed at solving problems ranging from personal computing to enterprise-level IT operations. LinuxToday serves as a home for a community that struggles to find comparable information elsewhere on the web.
Property of TechnologyAdvice. © 2025 TechnologyAdvice. All Rights Reserved
Advertiser Disclosure: Some of the products that appear on this site are from companies from which TechnologyAdvice receives compensation. This compensation may impact how and where products appear on this site including, for example, the order in which they appear. TechnologyAdvice does not include all companies or all types of products available in the marketplace.