National ICT Australia (NICTA), in conjunction with Open Kernel Labs (OK Labs), has released new software aimed at researchers, developers and manufacturers that has the ability to protect computer hardware from failure or being attacked.
The seL4 microkernel is a small operating system kernel which regulates access to a computer’s hardware and is able to distinguish between trusted and untrusted software.
NICTA principal researcher, Gerwin Klein, said the microkernel is the result of a research project announced in 2010 in which a team of researchers from the University of New South Wales (UNSW) completed the first formal machine-checked proof of a general-purpose operating system kernel, the seL4.
“Our seL4 microkernel is the subject of last year’s proof,” Klein said in a statement. “It 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.”
NICTA’s leader of embedded operating systems research and co-founder of OK Labs, Gernot Heiser, the microkernel is the product of seven years of research at NICTA, which followed around eight years of research at the University of New South Wales.
"Verification of operating-system kernels has been attempted since the 1970s, we pulled it off," Heiser said.
According to NICTA, the seL4 has the ability to keep trusted financial transaction software secure while running alongside “untrusted” software. In addition, it has the potential to provide a secure and reliable environment for mission-critical defence data, operating on the same platform as everyday applications like email, or protect the life-supporting functions of an implanted medical device, from hackers.
As reported by Computerworld Australia, the research organisation recently entered into a partnership with Microsoft alongside the Australian National University (ANU) and the Commonwealth Scientific and Industrial Research Organisation (CSIRO), that aims to provide researchers with Cloud computing resources and support.
The organisation’s principal research leader, Anna Liu, told Computerworld Australia at the time, that Australia’s research and development industry must look to Cloud computing technology in the future in order to successfully handle the “explosion” of data and the need for computation.