The organization Nicta and General Dynamics C4 Systems released the SeL4 microkernel as open source software this week. This includes complete kernel code, tools, libraries, and sample programs.
SeL4, in full the Secure Embedded L4 microkernel, hit the headlines five years ago after years of extensive testing based on the analysis of mathematical calculations. This showed that the relatively small kernel was free of bugs, which, according to Nicta, is still the case today. In support of the claim, it has also released the “evidence” to the community.
According to the SeL4 developers, the microkernel withstands several common attacks, such as stack smashing, exploit exploits and return-oriented programming. “SeL4 takes software reliability to a new level and will support the development of truly reliable systems,” said Nicta.
The organization says that important software today has fundamental flaws. According to Nicta, software where this is the case are applications in industry and in vehicles, such as cars and aircraft. “What has been released is not only the breakthrough Nicta achieved in 2009, but also the complete work that has been added in the years since.”