ERTOS News

We have released one of the main C verification tools in the L4.verified project under BSD license. The C-to-Isabelle parser reads C99 files into the theorem prover Isabelle/HOL and provides the basis for their formal verification.

Download the C parser here.

NICTA and German IT security specialist secunet Security Networks AG have entered a strategic research collaboration to develop high-security information technology (IT) products for the defence and government sectors. The research will combine secunet's experience in designing and building high-security devices with NICTA's expertise in formal verification and secure microkernel technology.

Download the full press release here.

ERTOS students Etienne Le Sueur, Bernard Blackham, Martin Pflauminger and Aaron Carroll have won the 2011 Lantronix XPort Pro Design Contest with their e⁴Meter.

NICTA and OK Labs have announced the first joint public release of the formally verified seL4 microkernel (branded OKL4 Verified). The release, for non-commercial and evaluation use, contains seL4 kernel binaries for ARM and x86, documentation, user level examples, x86 Linux on top of seL4, and the formal specification of the kernel for the ARM platform.

NICTA press release
Download seL4
L4.verified project

OK Labs has announced that OKL4, derived from NICTA's L4-embedded microkernel, has now shipped in more than 1.1 billion mobile phones. This makes OKL4 one of the most widely-deployed OS kernels ever.

NICTA press release

We have released a snapshot of the vNUMA source for download.

A paper titled Improved device driver reliability through hardware verification reuse has been accepted for publication in the 16^th ASPLOS Conference. The paper is the result of a collaboration with Intel (Hillsboro, OR) lead by ERTOS researcher Leonid Ryzhyk.

ERTOS leader Gernot Heiser has won the Innovation Hero Award of Sydney University's Warren Centre for Advanced Engineering.

Four years after co-founding Open Kernel Labs, Gernot Heiser has quit his position as Chief Technology Officer with the company to return to full-time research in NICTA. Gernot continues to serve on the Board of OK Labs and remains available to the company as a consultant.

The ERTOS paper entitled seL4: Formal verification of a microkernel has won a Best-Paper award at the 22nd Symposium on Operating Systems Principles (SOSP'09).

ERTOS group leader Gernot Heiser has won the Engineering, Mathematics and Computer Sciences Category of the New South Wales State Government's NSW Scientist of the Year 2009 Award.

NICTA press release

The ERTOS team has achieved a true world's first: The formal proof of functional correctness of a complete, general-purpose operating-system kernel, the seL4 microkernel developed by the group. This achievement redefines the state of the art in OS verification, and opens the way towards truly trustworthy computing systems. Details are published in this year's SOSP conference.

Full NICTA press release

Background brief: The L4.verified Story

The CAmkES framework for OKL4 has been released as open source under a BSD licence. CAmkES is a component-based software development framework for OKL4 that significantly simplifies development of complete multiserver systems on OKL4. It is the result of research work performed at NICTA by the ERTOS and ESE groups.

More information and download

A team made up of ERTOS staff John Judge and Peter Chubb, ERTOS/UNSW student Mark Sheahan, and staff and students from UNSW's Physics and Mechanical & Manufacturing Engineering won the second Artemis Orchestra competition, where an embedded system plays a regular, unmodified music instrument. Our team plays a clarinet. It was also the only entrant using a real embedded platform (a Gumstix) rather than a standard PC.

Full NICTA press release

NICTA spinout Open Kernel Labs (OK Labs) has won a grant worth $2.5M under the Australian Government's highly-competitive Commercial Ready scheme. The funding will be used to commercialise the outcomes of ERTOS research projects, specifically seL4 and L4.verified.

Full OK Labs press release

NICTA spinout Open Kernel Labs (OK Labs) has announced that OKL4, its microkernel based on NICTA technology, will be deployed in Internet-TV settop boxes from Headplay. OKL4 will protect Headplay's proprietary code from piracy and reverse engineering.

Full OK Labs press release

NICTA spinout Open Kernel Labs (OK Labs) has released version 2.1 of OKL4, its microkernel based on NICTA technology. This release introduces capability-based access control, and as such represents a major step towards commercial implementation of the microkernel API developed by NICTA's seL4 project.

OKL4 download site

NICTA spinout Open Kernel Labs (OK Labs) has announced that OKL4, its microkernel based on NICTA's L4 technology, runs on a number of 3G phones produced by HTC and others. These phones are now available in many countries around the world.

Full OK Labs press release

Open Kernel Labs (OK), the company spun out from NICTA's ERTOS group to commercialise its microkernel technology, has announced that an L4-based mobile phone manufactured by Toshiba has been on sale in Japan since late last year.

This represents the first publicly-known end-user deployment of ERTOS-developed microkernel technology.

Full OK press release

Open Kernel Labs (OK), the company spun out from NICTA's ERTOS group to commercialise its microkernel technology, has won the prestigious iAward of the Australian Information Industry Association (AIIA).

OK won the Applications and Infrastucture Tools category for its OKL4 embedded operating-system and virtualisation technology. The OK entry had also been short-listed in the Communications Applications category.

Full press release  

Open Kernel Labs (OK), the company spun out from NICTA's ERTOS group to commercialise its microkernel technology, has been established in the US. Most of the ERTOS development team working on the commercialisation of the technology has joined OK. OK has released its first L4 version, called OKL4. Based on NICTA::Pistachio-embedded, OKL4 is still open source, under a BSD license, but is now professionally supported.

The existing research projects seL4, L4.verified, Potoroo and CAmkES are continuing in NICTA, their outcomes will be commercialised by OK as they are ready. OKL co-founder Gernot Heiser is now splitting his time between serving as OK's CTO and continuing his role as leader of ERTOS.

Press release on OK launch
Press release on OKL4 release

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

“NICTA has four research projects ready for commercialisation in 2006. Some of these projects already have revenue streams and strong commercial interest, whilst others have received some seed funding from NICTA,” said NICTA Chairman Mr Neville Stevens at NICTA's annual technology showcase.

Open Kernel Labs formed out of the Embedded, Real-time and Operating Systems Program based at the ‘Neville Roach Laboratory’ in Kensington, NSW has already generated revenue from its service-based operating systems business. The research team has developed ways to make embedded systems more secure and reliable, thereby reducing the risk of attack by hackers or viruses. Open Kernel Labs is due for spin out later this year.

Full press release

... you must be running Wombat with Iguana on top of the L4 microkernel!

Wombat, NICTA's architecture-independent para-virtualised Linux for L4-embedded, can be faster than native Linux on the same hardware. Specifically on popular ARM v4 or v5 processors, such as ARM9 cores or the XScale, Wombat benefits from the fast address-space switch (FASS) technology implemented in L4-embedded, while this is not supported in native Linux distributions.

The result is that context-switching costs of virtualised Linux are up to thirty times less than in native Linux. This confirms, yet again, L4/Iguana as the leading high-performance embedded operating system and virtualisation platform for ARM processors. L4/Iguana and Wombat are also supported on x86 and MIPS platforms.

Details of the benchmarks can be found at the L4 performance page. How does your OS compare?

ERTOS will be demoing L4/Iguana and PLEB 2 hardware at CeBit Australia from May 9-11 2006. The ERTOS demos will be located in the Linux and Open Source Demo Zone in the Open Source Parc area.

A first draft of the seL4 API has been released. seL4 is NICTA's next-generation microkernel API aimed at embedded systems with high security requirements.

NICTA [...] today announced a collaborative effort with QUALCOMM Incorporated to use NICTA versions of the L4 Microkernel and the Iguana operating system together with select versions of QUALCOMM's Mobile Station^TM chipsets. [Full press release...]

The NICTA ERTOS team is pleased to announce the fist official release of its embedded OS framework, consisting of:

• NICTA::Pistachio-embedded, the first kernel conforming to the L4-embedded API. NICTA::Pistachio is based on L4Ka::Pistachio;
• Iguana, an L4-based OS personality developed specifically for embedded systems;
• Kenge, a set of packages for building microkernel-based systems;
• Wombat, a de-privileged (para-virtualised) Linux server running on top of L4/Iguana.

Presently the full package works on ARM and x86 platforms. MIPS64 is fully supported except for Wombat (which is due for release shortly) and an Alpha version is not far behind. See also the NICTA press release.

NICTA and the L4Ka Team are pleased to announce the release of the L4-embedded API. It is based on the L4Ka X.2 API of the L4 microkernel and aims to provide better support for embedded systems. Specifically, it aims to reduce complexity and memory overhead on architectures with limited resources, while keeping the API small, clean, and mostly compatible to X.2.

A reference manual and a rudimentary user manual for the new API are available. A release of a first compliant kernel is planned for later this month.

NICTA is pleased to announce the initial release of the Magpie interface compiler for L4-based systems.

Magpie joins the existing L4 interface compilers IDL4 and DICE. Its primary advantage over these compilers is its support for rapid, templated generation of new output modes.

Magpie currently supports the L4 V4 interface, with both generic and ARM-optimised output. Additional output modes, such as component orientation and C++ support, are in development.