An Exploration of ARM TrustZone Technology (Posted by Norman, 10 April 2014)
In their latest article and an accompanied demo video, the developers behind Genode share their hands-on experience with ARM TrustZone technology. The article covers a variety of topics ranging from platform enablement, over the rationale behind a custom kernel design, to the exploration of two actual platforms, namely ARM Versatile Express and FreeScale i.MX53.
Performance overview (Posted by Gernot, 19 Feb 2014)
I have added an overview of L4 kernel performance across 20 years of processor architectures and kernel versions. It is an extended version of the table that appeared in our SOSP paper last year. If anyone has other performance figures to contribute let me know.
Public release of seL4 (Posted by Gernot, 2 Feb 2011)
NICTA and Open Kernel Labs have announced a joint public release of the formally-verified seL4 microkernel. The release, for non-commercial and evaluation use, contains seL4 kernel binaries for ARM and x86, documentation, user-level example code, x86 Linux on top of seL4, and the formal specification of the kernel for the ARM platform.
NICTA download site
Over One Billion L4-based Phones (Posted by Gernot, 4 Nov 2010)
seL4 Verification article in New Scientist (Posted by gernot, 24 Sep 2009)
It is pretty unusual for New Scientist to report on developments in computer science, but it has just happened, with this article on the formal verification on seL4.
NICTA has formally verified the seL4 kernel (Posted by Gernot, 17 August 2009)
A few days ago NICTA announced that it has completed the
verification of the seL4 kernel. This makes
seL4 the world's first general-purpose OS kernel with a formal mathematical
proof that the implementation does what the specification says.
The proof is machine-checked and one of the largest ever done.
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.
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)
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)[News Archive]
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]