The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is going open source.
Time until release:
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.
It will include all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All will be under standard open-source licensing terms. More details will be posted here closer to the release date.
The release will happen 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).
Meanwhile, if you're interested in learning more about seL4, please check out about seL4, or the NICTA seL4 project site. More generally, you can find out about NICTA's trustworthy systems activities.
If you would like to learn more about the construction of trusted systems using kernels related to seL4, find out about the widely-deployed OKL4 Microvisor.
If you can't wait and would like to talk to the experts about using seL4 and associated technology to construct trusted systems, please contact GD.