[LINK] New seL4 microkernel 'crash/hacker proof'

[stephen at melbpc.org.au]

 <http://ertos.nicta.com.au/research/sel4?

This new sel4 Aussie operating system microkernel is being claimed to
be crash & hacker proof. It's also been included in the "MIT Technology 
Review 2011 TR10", which is MIT's annual list of the world’s ten most 
important emerging technologies ..

Download seL4 here:  http://ertos.nicta.com.au/software/seL4/home.pyl

MIT: <http://www.technologyreview.com/tr10>

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.

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.

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.

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." 

"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. 

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.



Message sent using MelbPC WebMail Server