seL4 will go open source on 29 July

Gernot Heiser gernot at cse.unsw.edu.au
Thu Jun 5 05:48:43 CEST 2014


… via the portal http://sel4.systems. This site will start accumulating info through the next few weeks, please check there for updates (or subscribe to the mailing list).

For those who haven’t heard about seL4: 
- it’s the latest L4 microkernel developed by NICTA. 
- according to the performance figures on http://l4hq.org, it’s the fastest L4 kernel around (let me know if you have performance data to contribute)
- it’s the world’s first and only OS kernel with a formal security proof, extending from high-level statements of confidentiality and integrity enforcement all the way down to the binary
- it’s proved functionally correct (i.e. bug-free implementation of the spec)
- it’s the first and only protected-mode OS with a complete and sound timing analysis, and as such the only credible platform on which to do hard real-time in protected mode
- it’s the foundation for DARPA’s high-assurance UAV project (http://trustworthy.systems/projects/TS/SMACCM/)

… and it will soon be free!

Gernot
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://os.inf.tu-dresden.de/pipermail/l4-hackers/attachments/20140605/b70c6728/attachment.html>


More information about the l4-hackers mailing list