"Proven security" claimed for NICTA spin-off OK Labs' mobile OS

Stuart Corner
Thursday, 27 January 2011 14:50

Business IT - Security

NICTA spin-off Open Kernel Labs (OK Labs) has released a version of its microkernel mobile operating system that, it says, will enable devices to run mission-critical applications with guaranteed and mathematically proven security in parallel with the device's normal insecure applications.

"Security-conscious device manufacturers (OEMs), mobile network operators (MNOs), application developers, researchers, and other interested parties can now download, run, and test OKL4 Verified on embedded ARM11 platforms," OK Labs says.

"With general availability for download, interested parties can now employ OKL4 Verified for evaluation and prototyping, using available user program libraries and/or a paravirtualised Linux kernel."

OK Labs claims that "OKL4 Verified is the only operating system in existence today whose source code has been mathematically proven to implement its specification correctly" and is "the result of more than four years work with NICTA and the University of NSW to verify the microkernel as correct and bug-free."

According to NICTA, "In future applications, seL4 [project name for OKL4 Verified] could ensure that trusted financial transaction software from secure sources such as banks or stock exchanges can operate securely on a customer's mobile phone alongside 'untrusted' software, such as games downloaded from the Internet.

"It could also provide a secure and reliable environment for mission-critical defence data, operating on the same platform as everyday applications like email. Or, it could protect the life-supporting functions of an implanted medical device, such as a pacemaker, from hacking attacks."

According to NICTA "The microkernel is the result of a world-first research achievement announced by NICTA last year, in which a team led by NICTA principal researcher Gerwin Klein, and including researchers from the University of NSW, completed the first formal machine-checked proof of a general-purpose operating system kernel: seL4."

According to Klein "[OKL4 Verified] is the only operating system kernel in existence whose source code has been mathematically proven to implement its specification correctly. Under the assumptions of the proof, the seL4 kernel for ARM11 will always do precisely what its specification says it will do."

Steve Subar, founder and CEO of OK Labs, said: "The confidence and reliability conferred by OKL4 Verified and its underlying technology enable an array of highly secure and certifiable applications on mobile/wireless devices, and represent the best path forward for secure mobile communications."

According to Gernot Heiser, cofounder of OK Labs, leader of Trustworthy Embedded Systems at NICTA and John Lions Professor at UNSW. "The completion of OKL4 Verified has created enormous interest in our unique verification technology. As the first operating system kernel proved to never operate out-of-spec, OKL4 Verified presents a truly trustworthy base for security- and safety-critical applications across a wide range of application domains."

According to NICTA, OK Labs software has already been deployed in more than one million cellphones http://www.itwire.com/it-industry-news/development/42934.