seL4 Verified Microkernel Now Open Source

Back in 2009, OKLabs/NICTA announced the first formally verified microkernel, seL4 (a member of the L4 family). Alas, it was proprietary software. Today, that's no longer the case: seL4 has been released under the GPLv2 (only, no "or later versions clause" unfortunately). An anonymous reader writes OSnews is reporting that the formally verified sel4 microkernel is now open source: "General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world's most highly assured OS." Source is over at Github. It supports ARM and x86 (including the popular Beaglebone ARM board). If you have an x86 with the VT-x and Extended Page Table extensions you can even run Linux atop seL4 (and the seL4 website is served by Linux on seL4).

Comments

More info

[Enry]

http://sel4.systems/FAQ/

Is it really that hard to give more background information?

Knuth said it best

[Anonymous Coward]

It may have been proven correct, but lets wait and see until after it's actually been used if it really is.

(Knuth said (paraphrased): be aware of bugs in the above code. I have only proved it to be correct; I have not tried it.)

Re:You can't choose forever. Once v3 touches it, g

[Immerman]

Yes, it does mean that any code including v3 code can only be legally licensed as v3 - but there's nothing stopping you from later extracting the offending code and reverting to v2+. You don't magically change the 2+ license under which you gained rights to the other code, you just only have the option of redistributing it under v3 so long as any v3-only code is included. So long as you make sure all contributions made in the interim are made under v2+ you don't have a problem (i.e. v3-only licensing can only spread if you let it).