Aussies Claim to have Developed 'Bug Free' OS for Mobile Platforms

Once again, our friends at sister brand Dr. Dobbs have provided me with yet more interesting blog fodder. In his editor's note in the daily Dr. Dobbs Update email, editorial director Jonathan Erickson discusses a breakthrough by Australian researchers who claimed to have developed the first "bug free" embedded software.Erickson notes that it's great to say you'd like to have bug free applications, but what happens when the underlying operating system is infested with bad code? Windows XP consists of approximately 40 million lines of code. Try finding the error in that tangle!

To solve this problem, researchers at Open Kernel Labs (OK Labs) and Australia's National Information and Communications Technology Research Centre (NICTA) examined the correctness, reliability and security of the microkernel technology underlying OKL4, OK Labs' virtualization platform for mobile devices. Erickson says their approach was to "create a mathematical method for proving the correctness of the underlying source code, using formal logic and programmatic theorem checking. The verification process eliminated a wide range of exploitable errors, such as design flaws and common code-based errors, buffer overflows, null-point dereferences, memory leaks, arithmetic overflows, and exceptions."

Once the work was done, OK Labs claimed it created "the world's first 100 percent verified 'bug free' embedded software." The researches said this helped establish a new level of software security and reliability for mission-critical applications, such as aerospace and defense. Additionally, this same verification process can be applied to business-critical applications in mobile telephony, business intelligence, and even mobile financial transactions.

Erickson drills down a bit deeper:

"All in all, the researchers verified approximately 7,500 lines of source code, proving over 10,000 intermediate theorems in over 200,000 lines of formal proof. The verified code base-the seL4 kernel (short for 'secure embedded L4')-is a third-generation microkernel, comprising 8,700 lines of C code and 600 lines of assembler, that runs on ARMv6 and x86 platforms. According to OK Labs, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel. In this case, 'functional correctness' means that the implementation always strictly follows a high-level abstract specification of kernel behavior. This includes traditional design and implementation safety properties (such as the kernel will never crash, and it will never perform an unsafe operation). It also proves that programmers can predict precisely how the kernel will behave in every possible situation."

I'm not pretending to understand the minutia of programming, but the implications of these findings seem to indicate a potential for greater reliability in mobile payments systems. OKL4 is OK Lab's virtualization application for mobile platforms. It sounds like virtualization for mobile is in its early stages, from what the company's website says, but still presents an interesting case for how mobile applications will evolve. OK Labs claims OKL4 enables mobile OEMs and semiconductor suppliers to incorporate "must-have features" into new mobile designs more quickly and less expensively. The idea is to reduce costs through hardware consolidation, allowing device manufacturers to "create smartphones at featurephone prices."

So I decided to contact OK Labs and see exactly how this would help m-financial services.

According to Rob McCammon, the VP of product management, Open Kernel Labs, the main benefit will come from strong security for the mobile channel. The operating system tends to be the most attractive target to hackers in any computerized system. They exploit certain software bugs that can compromise the security of the OS, he says. Once the operating system is compromised the rest of the software in the system is made vulnerable.

"Mobile financial transactions require and benefit from strong security," he says. "Stronger security can lower the risk of financial loss from fraud or theft. Additionally, confident users of systems can lead to higher (and more secure) transactions."

He concludes, "The completion of this research demonstrates that it is possible to create an operating system kernel or hypervisor that is free of a wide range of bugs. The presence of bugs in a system opens the door to attacks on a mobile phone's privileged mode software. The research shows that a higher level of security and confidence can be provided than was previously thought possible."

The company hopes to bring this secure and verified "Microvisor" to market in its virtualization platforms for mobile OEMs, mobile network operators, and IT managers building mobile-to-enterprise applications.

Since mobile financial services is still in its early stages (certainly in the U.S.), there haven't been many reports of exploits outside of eavesdropping on NFC signals in contactless payment transactions. This research, if broadly embraced, might help financial institutions start off on the right foot when developing mobile applications-with the security baked in from the start.