NICTA wins race to secure L4

Australian research organisation, NICTA, claims to be the world's first to develop a formal machine-checked proof of a general-purpose operating system kernel, the Secure Embedded L4 (seL4).

The seL4 microkernel, designed for real-world use, will potentially be used in defense and medical industries as well as any other industry where safety, security and the operation of complex embedded systems is critical.

Formal proofs for specific properties have been done for smaller kernels in the past, but this is the first proof of an entire operating system kernel of such complexity.

The research also found that many kinds of common attacks will not work on the seL4 kernel. For example, the microkernel is impervious to buffer overflows, a common form of software attack where hackers take control of programs by injecting malicious code.

Open Kernel Labs' Chief Technology Officer and leader of NICTA's ERTOS Group, Professor Gernot Heiser, said it is exciting to have done something that many people thought was not going to be possible.

There were several larger and much better funded teams around the world working on similar research, Heiser said, but none have yet succeeded.

The most challenging aspect of this task was to do with scale, according to Heiser.

“Scale is a significant part of the problem. In the past when people were verifying software they would typically need to verify hundreds, or maybe small numbers of thousands, of lines of code. We pushed that to almost 10,000 lines of code,” he said.

“Not only that, the inherent nature of a kernel is much more complex than that of software. It is not as structured as other software and everything interacts with everything.”

NICTA will transfer its intellectual property to Open Kernel Labs (a NICTA spin off), whose embedded hypervisor software operates hundreds of millions of consumer devices worldwide.

Heiser said that, in principle, the seL4 could be a replacement for Open Kernel Labs' OKL4 Microvisor, the company's mircokernel-based hypervisor.

“Whether we will market seL4 as it is or use the IP to verify the existing OKL4 microkernel has not been decided yet. But the plan is definitely to turn it into a product for markets that need high security and reliability, like medical, defence, security and automative markets,” he said.

“We have not made a product decision yet, but we would be looking to have products in those markets by 2011.”

Heiser said one of the primary research objectives was to come up with a kernel that would not only be verified but whose performance would be suitable for use in real-life systems.

“My briefing was that we must not lose more than 10 per cent performance through the verification process. Right from the start, this was not just an academic exercise but something that was for real-world use.”

Heiser points to the medical sector to demonstrate how this technology will be useful in the future.

“In the medical space, the trend is towards more complex systems that will increasingly used by less sophisticated users. That will require devices to have a more friendly user interfaces which typically has a lot of complex programming behind it,” he said.

“So you have a medical device that could potentially kill someone if it misbehaves, combined with complex programming which you can't really trust, which is not so bad if it only interferes with the usability, but if it interferes with the life-critical part of the system, that is not good.”

Basically, said Heiser, you have a growing need for systems that are both critically important, but also have the complexity inherent in creating easy user interfaces. The main requirement is to ensure that the life-critical part of a system is protected from the rest of the system, no matter what happens.

“This is where we are headed with technology like seL4 with which we will ultimately be able to build fully verified systems with meaningful dependability guarantees. We are not there yet, but [with seL4] we now have the core platform that enables this verification.”

• Bookmark this page
• Share this article
  • facebook
  • slashdot
  • digg
  • Reddit
  • stumbleupon
• Got more on this story? Email Computerworld
• Follow Computerworld on twitter

Comments