Eight months after National ICT Australia (NICTA) released its secure embedded L4 (seL4) microkernel, it has moved closer to commercialisation with potential developments by the Department of Defence and the mining sector using the software.
The seL4, created in collaboration with Open Kernel Labs (OK Labs), is a small operating system kernel that regulates access to a computer’s hardware and is able to distinguish between trusted and untrusted software.
NICTA’s leader of embedded operating systems research and co-founder of OK Labs, Gernot Heiser, told Computerworld Australia that while there has been no final decisions about the use of the kernel, three “fairly concrete” projects had been designed around the software in areas of national security and mining.
“It is in the evaluation stage for a number of possible deployments but these things inevitably take time,” Heiser said. “One obvious application area is military but typical military projects take years and years especially as the development is architected around our kernel.”
“There’s been no actual decisions because that’s in the nature of these things, people bid for projects and then they do the designs and get them approved,” he said.
“We are in a number of projects that are being designed around us, none of them are guaranteed to go ahead but there are some fairly concrete developments.”
According to Heiser, since the software was made available for free download (not for commercial development use) for researchers, developers and manufacturers, it has experienced more than 1000 downloads on both the NICTA and OK Labs websites.
“There’s certainly strong interest out there and a lot of people were actually waiting to get their hands on it… but these things take some time to gel out.
“It’s not a big number [of downloads] compared to many open-source projects, but for something like this which is really of interest to a special group of experts, it's actually quite good.”
The reason behind the release earlier in the year, Heiser said, was primarily to make it accessible to academics who want to design systems and also for future potential users.
Since its release, NICTA has also proved the system can enforce integrity which, Heiser said was a basic safety property and a necessary component in demonstrating its usability in safety critical systems.
According to Heiser, the microkernel is the product of seven years of research at NICTA, following on from around eight years of research at the University of New South Wales.
"Verification of operating-system kernels has been attempted since the 1970s, we pulled it off," Heiser said at the time.
Techworld Australia feature articles:
Follow Chloe Herrick on Twitter: @chloe_CW
Follow Computerworld Australia on Twitter: @ComputerworldAU