After 7 years of research, Australian NICTA, a spin-out company Open Kernel Labs (OK Labs) have released what they call the Sel4 microkernel, which is is a small operating system kernel which regulates access to a computer’s hardware.
Its unique feature is that it has been mathematically proven to operate correctly, enabling it to separate trusted from untrusted software, protecting critical services from failure or malicious attack.
“In a future where everything from cars to hospital operating theatres will depend on the flawless performance of sophisticated computer systems, the availability of completely reliable hardware and software will be vital.
Up until now, the tools to guarantee this level of reliability have not existed, but with today’s release of software based on breakthrough NICTA research, all this has changed.”
The microkernel is available now for download and execution on:
- Select ARM11-based evaluation and product boards, including the KZM-ARM11-01 from Kyoto Microcomputer (contact OK Labs for a complete list)
- x86/PC-AT hardware, as a stand-alone OS
- x86/PC-AT hardware, hosting execution of para-virtualized Linux
According to the researchers, a mathematically proven operating system was trying to be built since the seventies, but it is only now that they have with Sel4 succeeded.
About Danny Bisaerts
