seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement" originally developed (as far as I know) at UNSW, further developed at NICTA.
This is excellent. While I'm still unsure about the seL4 model being the best for a secure system (a topic for another day), it's wonderful to see this development.
I hope "someone" will port this to RISC-V (32- or 64-bit).
Is http://ssrg.nicta.com.au/software/TS/seL4 out of date or is the license really not open source (OPEN KERNEL LABS and National ICT Australia Limited (Licensors) NON-COMMERCIAL LICENSE AGREEMENT)?
"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.
What's being released?
It includes all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All is under standard open-source licensing terms — either GPL version 2, or the 2-clause BSD licence.
When is it happening?
The release happened at noon of Tuesday, 29 July 2014 AEST (UTC+10), in celebration of International Proof Day (the fifth aniversary of the completion of seL4's functional correctness proof)."
EDIT: The original link should probably be updated to http://sel4.systems/ as it has the link to the Github page prominently displayed there.
The fundamental issue is that, IMhO, security classification needs to be attached to the data at the lowest level -- OS level is simply to coarse. Take for example an encrypted channel. At the OS level the channel is treated opaquely whereas at the programming language level, after decryption the authenticated data can be assigned both a different level of secrecy and trust, and it can be data dependent. Strong type systems can ensure that secret data is never accidentally leaked, nor untrusted data used in a trusted context. (For a real-life simple subset of this, see tperl).
It may be possible to build such a system on top of seL4, but seL4 isn't sufficient.
I do intend on working on this eventually. Incidentally, D. J. Bernstein recently shared a similar complaint about the state of security - the models we use have practically not advanced since the 1950es.
I'm not sure who submitted the link (I don't think it was anyone from the seL4 team), but I inserted the http://sel4.systems/ link into the repo's README file, which will hopefully help a little.
The original project home page is at http://ssrg.nicta.com.au/projects/seL4/ and the new page is at http://sel4.systems/
Downloads at http://ssrg.nicta.com.au/software/TS/seL4/