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.
Thread beginning with comment 378552
To read all comments associated with this story, please click here.
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 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 Parent Score: 1