National ICT Australia (NICTA), in association with Open Kernel Labs (OK Labs), has released a new security software, seL4 microkernel.
The company said the OS kernel that can protect computer hardware from failure or hackers is aimed at researchers, developers and manufacturers.
The seL4 microkernel regulates access to a computer’s hardware and can distinguish between trusted and untrusted software, claims the company.
Moreover, the company said, the software 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 medical devices from hackers.
NICTA principal researcher Gerwin Klein said a team of researchers from the University of New South Wales completed the first formal machine-checked proof of a general-purpose operating system kernel.
Klein said, "Our seL4 microkernel is the subject of last year’s proof."
Klein added, "It is the only operating system kernel in existence whose source code has been mathematically proven to implement its specification correctly."
NICTA’s leader of embedded operating systems research and co-founder of OK Labs, Gernot Heiser said, "Verification of operating-system kernels has been attempted since the 1970s, we pulled it off."
