NICTA Wins Race to Secure L4
Linked by Thom Holwerda on Thu 13th Aug 2009 15:08 UTC, submitted by Inkslinger
OSNews, Generic OSes Australian research organisation NICTA claims to be the world's first to develop a formal machine-checked proof of a general-purpose operating system kernel, the Secure Embedded L4 (seL4). The organisation "beat" several other larger and better funded organisations to claim this achievement, according to a spokesperson.
E-mail Print r 4   3 Comment(s) http://osne.ws/gys
Order by: Score:
Add Comment Post a Comment
Awesome
by waid0004 on Fri 14th Aug 2009 22:59 UTC
waid0004
Member since:
2009-06-19

This is really quite an awesome achievement. The ability to formally verify so much code is needed with software's increasing real world applications. My only hesitation is that the code doesn't seem to be available under an open license.

Reply Score: 1

RE: Awesome
by shaunehunter on Tue 18th Aug 2009 06:29 UTC in reply to "Awesome"
shaunehunter Member since:
2007-02-12

It's a little baffling that the first L4 implementation certified is also the first closed source one (as far as I can see and I've been paying attention).

Do you think this may be another example of a collaborative effort shanghaied by a business once it reaches a milestone? (think darwin or webkit)

It's why I don't like open source licenses that don't require reciprocation. Such as L4's original BSD license.

Reply Score: 1

What matters now..
by fithisux on Tue 18th Aug 2009 07:07 UTC
fithisux
Member since:
2006-01-22

is to see OSes using L4. L4Linux/GenodeOS make steps. However real OSes like Syllable and Hurd must make the switch.

Reply Score: 2

Add Comment Post a Comment