High-security microkernel goes on release

Australian researchers have delivered an SeL4 microkernel with pared-down code that promises a higher guarantee against bugs than provided by Windows, Linux and Mac OS

Australian researchers have released a microkernel that aims to all but guarantee software security.

The idea behind it is the Formal Methods mathematical theorem, which ensures the secure embedded L4 (SeL4) microkernel always installs exactly as specified. The theory is defined by Carnegie Mellon University as a technique to model complex systems as mathematical entities. This makes it possible to verify a system's properties in a more thorough fashion than through empirical testing.

The creation of the microkernel takes aim at the world's most popular operating systems (Microsoft Windows, Linux and Mac OS), which SeL4 lead designer Gerwin Klein sees as bloated with code, with features overruling form.

By comparison, SeL4 has about 10,000 lines of code, all verified using Formal Methods, meaning it is possible to "prove the code" and guarantee against bugs, Klein said. The microkernel is being released under the OKL4 brand name by Open Kernel Labs, Australia's Information and Communications Technology Centre of Excellence (Nicta), a private-sector research organisation, said on Thursday.

For more on this ZDNet UK-selected story, see Aussie microkernel sets security in stone on CNET News.

Get the latest technology news and analysis, blogs and reviews delivered directly to your inbox with ZDNet UK's newsletters.