World's first hack free software

Tweet

it could provide a secure and reliable environment for mission-critical defence data, operating on the same platform as everyday applications like email MELBOURNE: Scientists have developed what they claim is the world's first hack-free software which can protect systems from failure or malicious attacks. The 'seL4' microkernel has been developed by a team led by Australia's ICT Research Centre of Excellence's spinout company -- Open Kernel Labs (OK Labs). It is a small operating system kernel which regulates access to a computer's hardware. Its unique feature is that 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. 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, according to its developers. 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. "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," lead scientist Gerwin Klein said. Added another scientist Gernot Heiser, "Verification of operating-system kernels has been attempted since the 1970s -- we pulled it off!'

it could provide a secure and reliable
environment for mission-critical defence data,
operating on the same platform as everyday
applications like email
MELBOURNE: Scientists have developed what
they claim is the world's first hack-free software which can protect systems from
failure or malicious attacks.
The 'seL4' microkernel has been developed by a
team led by Australia's ICT Research Centre of
Excellence's spinout company -- Open Kernel
Labs (OK Labs). It is a small operating system kernel which regulates access to a computer's
hardware.
Its unique feature is that 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.
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, according
to its developers.
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.
"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," lead scientist
Gerwin Klein said.
Added another scientist Gernot Heiser, "Verification of operating-system kernels has
been attempted since the 1970s -- we pulled it
off!'