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

Re:Don't tell HURD

[slashdot_commentator]

seL4 is probably a subset of MACH. It wouldn't be an insurmountable problem to port HURD to run on top of seL4. What might be exceptionally difficult would be to rewrite HURD to take advantage of seL4's design, to produce a more "correct" version of a microkernel based OS.

IIRC, the HURD effort to replace MACH with L4 had nothing to do with difficulty salvaging HURD code to run on top of L4. It had to do with known security flaws with inter process communications in MACH and the original L4 implementation. There was a grad student looking to replace MACH with a prototype secure variant of L4 called coyotos, which was eventually abandoned.

Fuck HURD. HURD was a failure. HURD was a vanity project Richard Stallman wanted implemented to undercut the popularity of the fledgling linux OS. He abandoned his cheerleading effort for it over a decade ago. (I doubt Stallman even contributed code to the original HURD implementation.) Since then, its been whored out to every grad student looking to use it as a platform for their thesis. The whole academic drive towards microkernel OS is obsolete research, like using PROLOG to implement AI systems. Microkernels have been supplanted by hypervisors and secure ipc implementations. Really, if HURD worked, what would it be doing that would make it uniquely valuable when compared to all current operating systems?

Personally, I wish I could avert my eyes from this collision between two behemoth machines trapped in an event horizon.