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

Re:Unfortunately?

[tlhIngan]

How does the "or later" clause hinder use? Licensing under GPLv3 might have (I'm not going to argue that either way), but what does the "or later" clause matter?

Because you cannot mix v2-only code with v3/v3+ code. It's actually incompatible - v3 puts additional "restrictions" (from v2's perspective) on the code, making it incompatible (e.g., anti-TiVoization, etc).

So this means all code in that kernel must be either v2 or v2+ (which means the "+" disappears).

For an embedded systems, they typically want GPLv2 or v2+, avoiding v3 as much as possible. "or later" can hinder since if you're not careful, you might accidentally include v3 code (especially if you pull from an upstream source) when you don't want to. v2-only makes that a license violation, while v2+ turns into v3/v3+. One should be careful when pulling patches to make sure the codebase doesn't unexpectedly turn into v3.