Top secret trials for NICTA's kernel breakthrough

The development of the world's first formally proved general purpose operating system by Australian researchers has garnered interest from within the intelligence community as a potential solution to long held limitations to secure data storage.

The Secure Embedded L4 (seL4) microkernel, developed by engineers at NICTA (National ICT Australia), is the world's first general purpose microkernel that is not only formally specified (mathematically described), but also formally verified - meaning that mathematicians have proven that every line in the kernel is consistent with this specification.

Applying formal methods of mathematics to "prove" the microkernel has taken NICTA boffins some five years - requiring a team of crack mathematicians and an open source verification tool called Isabelle, developed at the Technical University of Munich, Germany.

Developers of systems based on the microkernel will now be able to mathematically prove their software is free from most errors. The kernel is impervious to, among other vulnerabilities, buffer overflow attacks.

Professor Gernot Heiser, a professor in operating systems at the University of NSW and leader of the NICTA project, said the operating system is likely to be used to solve what he calls the "high paranoia effect" - any system in which people are worried about security and safety.

"It will be used in devices with high stakes, life and death stakes, such as medical, automotive or aerospace," he said.

Heiser said the microkernel was used in a demonstrator system that was intended for use.

He said the secure operating system was under review by an unnamed national security agency.

"It is being used in a device that deals with the storage of information in which file are of different classifications and thus need to be kept clearly distinct," he said.

Traditionally, 'military spec' computing with data of a sensitive or nature have been kept on separate, discrete computers [PDF - see section on Abstraction of System Description] from information classified at a lower or higher level. In extreme cases, classified materials were stored on purpose-built hardware devices that can only be connected to a network under strict conditions.

The secure microkernel developed by NICTA, on the other hand, can be deployed in a virtual computing environment - whereby materials of different classification can be securely stored in software on the same piece of hardware, on separate but logically and securely separated virtual machines.

"The intelligence community will be able to move from physical separation to logical separation, guaranteed to be secure by our kernel," Heiser said. "It's a case of virtualisation, with guaranteed isolation."