seL4 to go open-source on 29 July
Gernot Heiser <[email protected]> Thu, 5 Jun 2014 13:53:39 +1000
| Newsgroups | gmane.comp.micro-kernel.l4.l4ka.general |
|---|---|
| Message-ID | <[email protected]> |
--Apple-Mail=_6B09EB95-5D55-45F1-A53A-9ACC972A067A Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=windows-1252 If you=92re looking for a supported high-performance L4 microkernel, and = the moral successor of L4KA::Pistachio, then seL4 is probably for you. = It will go open-source in less than 2 months 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=92t heard about seL4:=20 - it=92s the latest L4 microkernel developed by NICTA.=20 - according to the performance figures on http://l4hq.org, it=92s the = fastest L4 kernel around (let me know if you have performance data to = contribute) - it=92s the world=92s 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=92s proved functionally correct (i.e. bug-free implementation of = the spec) - it=92s 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=92s the foundation for DARPA=92s high-assurance UAV project = (http://trustworthy.systems/projects/TS/SMACCM/) =85 and it will soon be free! Gernot= --Apple-Mail=_6B09EB95-5D55-45F1-A53A-9ACC972A067A Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=windows-1252 <html><head><meta http-equiv=3D"Content-Type" content=3D"text/html = charset=3Dwindows-1252"></head><body style=3D"word-wrap: break-word; = -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">If = you=92re looking for a supported high-performance L4 microkernel, and = the moral successor of L4KA::Pistachio, then seL4 is probably for you. = It will go open-source in less than 2 months via the portal <a = href=3D"http://sel4.systems">http://sel4.systems</a>. This site will = start accumulating info through the next few weeks, please check = there for updates (or subscribe to the mailing = list).<div><br></div><div>For those who haven=92t heard about = seL4: </div><div>- it=92s the latest L4 microkernel developed by = NICTA. </div><div>- according to the performance figures on <a = href=3D"http://l4hq.org">http://l4hq.org</a>, it=92s the fastest L4 = kernel around (let me know if you have performance data to = contribute)</div><div>- it=92s the world=92s 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</div><div>- it=92s proved functionally correct (i.e. bug-free = implementation of the spec)</div><div>- it=92s 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</div><div>- it=92s the foundation for DARPA=92s high-assurance UAV = project (<a = href=3D"http://trustworthy.systems/projects/TS/SMACCM/">http://trustworthy= .systems/projects/TS/SMACCM/</a>)</div><div><br></div><div>=85 and it = will soon be = free!<br><div><br></div><div>Gernot</div></div></body></html>= --Apple-Mail=_6B09EB95-5D55-45F1-A53A-9ACC972A067A--