Open Kernel Labs Developed First Ever Hack Free Software

Open Kernel Labs (OK Labs), that develops microkernel-based hypervisors and operating systems for embedded systems developed ‘seL4’ microkernel – first ever hack free software in the world. It is developed by a team led by Australia’s ICT Research Centre of OK Labs. OK Labs announced availability for download of OKL4 Verified (project name seL4) on 26th January 2011.

It is a fully verified, bug-free secure microkernel for business-critical and mission-critical applications in mobile/wireless devices. 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.

‘seL4’ microkernel is a small operating system kernel which regulates access to a computer’s hardware. It has been mathematically proven to operate correctly, enabling it to separate trusted from untrusted software, protecting critical services from a failure or a malicious attack, say the scientists.

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, they say.

In future applications, seL4 could ensure that trusted financial transaction software from secure sources like banks or stock exchanges can operate securely on a customer’s mobile phone alongside “untrusted” software, such as games downloaded from the Internet.[advt]

Key Facts

• OKL4 Verified is the only operating system in existence today whose source code has been mathematically proven to implement its specification correctly
• OK Labs OKL4 Verified (project name seL4) is the result of more than four years work with NICTA and the University of New South Wales to verify the microkernel as correct and bug-free
• Device manufacturers, developers, researchers, and other interested parties can now download, run and test the OKL4 Verified microkernel for real-world applications
• The OKL4 Verified shares underlying technology with the OKL4 Microvisor and the OK Labs mobile virtualization solution, and represents a key part of OK Labs investment in secure mobile communications
• The download includes bootable images for x86 and ARM11, user-space libraries and other code needed for building applications, paravirtualized Linux running on OKL4 Verified, user documentation, and the formal specification

Steve Subar, Founder and CEO, OK Labs said:

A fully verified, 100% bug-free OS kernel meets pressing needs for greater security in mobile/wireless and other embedded applications. 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.

Lead scientist of the reaserch team, Gerwin Klein said,

Our seL4 microkernel 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.[source]