DARPA has made awards to 6 seL4-based projects under the SBIR scheme. The projects are targeting safety- or security-critical use cases in civilian (eg SCADA) and military domains, one is targeting components for spacecraft. The award recipients plan to release their contributions to the seL4 ecosystem as open source.
In July 2015, the Boeing Unmanned Little Bird, an optionally-piloted helicopter, conducted its first test flight with the mission computer running on seL4. Boeing has now released a video showing the flight.
DARPA, the US Defence Advanced Research Projects Agency, has issued a SBIR call titled “Secure Software Components Leveraging the seL4 Microkernel”
The SBIR program funds “small” enterprises (that's <500 employees in US speak) that are majority US-owned.
The central theme of Genode version 14.08 is a new GUI architecture that maintains strong security yet scales to highly flexible and dynamic GUIs. Furthermore, the release features OpenVPN, networking for VirtualBox (on top of NOVA), SMP support for the Seoul virtual-machine monitor, DDE Linux updated to version 3.14.5, and vastly improved performance of Genode's custom base-hw kernel. Genode can be used on top of most members of the L4 family. Read more about the new version in the comprehensive release documentation.
Free as in speech, not beer, that is.
The seL4 source code, proofs and related userland and tools were open-sourced today by and General Dynamics C4 Systems. The kernel and proofs are under GPL v2, user libraries under the 2-clause BSD license. Details, including download links, at seL4.systems.
and General Dynamics C4 Systems are open-sourcing seL4 and its formal verification artifacts. Details to be announced soon.
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.
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.
and have announced a joint public release of the formally-verified seL4 microkernel. The release, for non-commercial and evaluation use, contains 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
announced that has now shipped in more than a billion devices. This makes L4 one of the most widely-deployed OS kernel ever.
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.
A few days ago announced that it has completed the
verification of the kernel. This makes
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.
Details of the announcement
CAmkES is a component-based software development framework for developed by . It provides tools and and an environment that significantly simplify development of complete multiserver systems on OKL4. It is released under a BSD licence.
, the commercial L4 system from (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) has just released 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 project, which has designed a high-security API and an implementation that will be formally verified in the project.
In late 2007 NICTA researchers in the 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.
Following its deployment in CDMA phones in Asian markets in 2006, 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.
(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]
(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]
NICTA spinout company (OK) announced last week that it is open for business. OK develops and globally distributes and supports , a commercial-strength version of L4. 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 .
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 on commercialising the research of NICTA's program, which includes a provably correct version of L4 able to satisfy the highest security requirements.
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]