The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement 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.
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.
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).
Check our FAQ.
Read the white paper, Mathematically Verified Software Kernels: Raising the Bar for High Assurance Implementations.
To stay informed, sign up for the Announcements mailing list. To participate in discussions, ask technical questions etc, sign up for the Developers mailing list.
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 how to build a system on seL4, you might want to follow the lectures and especially the seL4-based project of UNSW's Advanced Operating Systems course.
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.
联系客服
