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.
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.
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.
is to see OSes using L4. L4Linux/GenodeOS make steps. However real OSes like Syllable and Hurd must make the switch.