Latest News

NICTA releases CAmkES framework as open source (Posted by Gernot, 9 December 2008)

CAmkES is a component-based software development framework for OKL4 developed by NICTA. It provides tools and and an environment that significantly simplify development of complete multiserver systems on OKL4. It is released under a BSD licence.

Download CAmkES

OKL4 to secure IP-TV settop boxes (Posted by Gernot, 24 May 2008)

OKL4, the commercial L4 system from Open Kernel Labs (OK Labs), will be deployed in high-definition internet-television settop boxes to be shipped to Asia by Headplay. OKL4 will protect Headplay's proprietary code from reverse engineering. [Full press release]

OK Labs releases L4 kernel with Caps (Posted by gernot, 21 Apr 2008)

Open Kernel Labs (OK Labs) has just released OKL4 2.1 which is the first L4 kernel that introduces capability-based access control. At present capabilities are used for accessing threads (and thus controlling IPC), but will eventually control access to all resources in an OKL4-based system. This presents the first step in commercialising the outcomes of NICTA's seL4 project, which has designed a high-security API and an implementation that will be formally verified in the L4.verified project.

NICTA completes first refinement of L4 verification (Posted by gernot, 21 Apr 2008)

In late 2007 NICTA researchers in the L4.verified project completed the first refinement proof of the implementation of their L4 kernel. The proof shows the correspondence between the formal API and a formalised Haskell implementation, which corresponds to a “low-level design” in Common Criteria language. The second refinement, down to the actual C/assembler implementation, is scheduled for completion on 2008.

L4-powered smartphones now near you (Posted by gernot, 21 Apr 2008)

Following its deployment in CDMA phones in Asian markets in 2006, OKL4 started shipping last year in a range of 3G smartphones based on the Qualcomm MSM7200 chip. These include phones by HTC, LG and Toshiba. These phones have been selling since 2007 in Europe, the US, Australia and other countries.

Japanese consumers talk on L4 phones (Posted by Gernot, 6 July 2007)

Open Kernel Labs (OK) has announced that a Toshiba-manufactured mobile phone powered by its OKL4 microkernel has been on sale in Japan since late last year. [Full press release]

OKL4 wins industry award (Posted by Gernot, 6 June 2007)

Open Kernel Labs (OK) has won the Australian Information Industry Association's iAward in the category of Applications and Infrastructure Tools. The award is for the company's OKL4 embedded operating system and virtualisation technology. OKL4 was also a finalist in the Communications Applications category.

As an AIIA award winner, OK will be one of three Australian representatives at the prestigious Asia Pacific ICT Awards (APICTA) program in Singapore in November of 2007. [Full press release]

Open Kernel Labs Launched (Posted by Gernot, 21 April 2007)

NICTA spinout company Open Kernel Labs (OK) announced last week that it is open for business. OK develops and globally distributes and supports OKL4, a commercial-strength version of L4. OKL4 is designed to provide high-performance and secure OS and virtualisation technology especially for use in embedded systems. It is a descendant of NICTA::Pistachio-embedded, itself a descendant of L4Ka::Pistachio.

The creation of a company dedicated to developing and marketing L4 technology clearly opens a new chapter in the history of the L4 microkernel. Furthermore, OK is collaborating with NICTA on commercialising the research of NICTA's ERTOS program, which includes a provably correct version of L4 able to satisfy the highest security requirements.

NICTA and Ericsson announce L4-based research (Posted by Gernot, 22 Aug 2006)

National ICT Australia (NICTA) and Ericsson today announced a three-year umbrella agreement for research into next-generation mobile networks to develop technology that will optimise connectivity for the consumer. The agreement is with Ericsson's global research arm and is initially valued at AUD$2.7 million with scope for expansion...

A second project under the agreement will research secure real-time operating systems. It will explore the use of NICTA's microkernel-based operating-system and virtualisation technology and formal-verification research to greatly enhance the security of data and communications on mobile-phone handsets. This project will be lead by Professor Gernot Heiser, who heads the Embedded, Real-Time and Operating Systems research program at NICTA's Neville Roach Laboratory... [Full press release]