An Australian-designed microkernel has been released, which claims to all but guarantee software security.
(Credit: Darren Pauli/ZDNet Australia)
Its secret is the Formal Methods mathematical theorem, which ensures the 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 empirical testing.
The creation of the microkernel takes a swipe at the world's most popular operating systems (Microsoft Windows, Linux and Apple), which SeL4 lead designer Dr Gerwin Klein sees as bloated with code, with features overruling form.
"It is ubiquitous: from high-level Linux, to Microsoft, they are all the same — they are way too big," Klein said.
"They have forgotten what the operating system was meant to be; they have left their past behind."
Klein, an associate professor at the University of NSW and principal researcher at National ICT Australia (NICTA), refers to an era when operating systems had much fewer lines of code and were more secure. Now they are built on millions and millions of lines of code which offers users massive levels of functionality, but opens a swathe of security vulnerabilities, Klein said.
"That's not such a problem for home users, but defence departments … it gets dicey with them."
"And [US President Barack] Obama using a BlackBerry? That device is just not secure enough."
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, according to Klein.
Formal Methods is his chief field of research at the university and NICTA. It is a slow, expensive but sure way to verify the functionality of systems, "at least at a high level", he said.
The system was built from the ground-up by Klein and about seven NICTA researchers over four years. It is based on the German-designed L4 microkernel, which is known to be practical and fast.
It allows software stacks to be isolated, meaning trusted software can run adjacent with untrusted applications.
"For instance, take a mobile phone with a user interface that has all the bling — [SeL4] can completely isolate say financial transaction software so that only communicates with the interface over small channels," Klein said. "Even if the user interface is hacked or crashes, the private information of the financial software can't be accessed."
It is more complex than running adjacent software stacks, because the microkernel has to be designed with a servitude to security.
SeL4 has been demonstrated on mobile phone architectures and its cousin, the OKL4 microkernel-based embedded hypervisor, is already running in about a billion phones.
"Could we run it on an iPhone? … sure it would not really be hard," Klein said, noting it would also readily adapt to Apple Mac architecture.
Open Kernel Labs, a NICTA spin-off that is controlling distribution of SeL4, is already discussing implementation of the microkernel with multiple defence departments.