Public release of seL4
Gernot Heiser <[email protected]> Wed, 2 Feb 2011 17:12:35 +1100
| Newsgroups | gmane.comp.micro-kernel.l4.l4ka.general |
|---|---|
| Message-ID | <[email protected]> |
--Apple-Mail-15-492375556 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii Members of this mailing list may be interested in the below = announcement... Begin forwarded message: > From: Gernot Heiser <[email protected]> > Date: 2 February 2011 17:09:11 AET > To: [email protected] > Subject: Public release of seL4 >=20 > NICTA and Open Kernel Labs have jointly released seL4. For those not = aware of seL4, it is an L4 microkernel which is formally verified = (meaning that the implementation is mathematically proven to conform to = the specification). It is the world's first (and only) OS kernel that is = formally verified in this strict sense. >=20 > The public release includes the formal specification of the kernel = (ARM version), kernel binaries for x86 and ARM, and a para-virtualized = Linux running on top of seL4/x86. >=20 > More about seL4: http://ertos.nicta.com.au/research/sel4/ > NICTA download site: http://ertos.nicta.com.au/software/seL4/home.pyl >=20 > Gernot --Apple-Mail-15-492375556 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii <html><head></head><body style=3D"word-wrap: break-word; = -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; = ">Members of this mailing list may be interested in the below = announcement...<br><div> </div> <div><br><div>Begin forwarded message:</div><br = class=3D"Apple-interchange-newline"><blockquote type=3D"cite"><div = style=3D"margin-top: 0px; margin-right: 0px; margin-bottom: 0px; = margin-left: 0px;"><span style=3D"font-family:'Helvetica'; = font-size:medium; color:rgba(0, 0, 0, 1);"><b>From: </b></span><span = style=3D"font-family:'Helvetica'; font-size:medium;">Gernot Heiser = <<a = href=3D"mailto:[email protected]">[email protected]</a>><br><= /span></div><div style=3D"margin-top: 0px; margin-right: 0px; = margin-bottom: 0px; margin-left: 0px;"><span = style=3D"font-family:'Helvetica'; font-size:medium; color:rgba(0, 0, 0, = 1);"><b>Date: </b></span><span style=3D"font-family:'Helvetica'; = font-size:medium;">2 February 2011 17:09:11 AET<br></span></div><div = style=3D"margin-top: 0px; margin-right: 0px; margin-bottom: 0px; = margin-left: 0px;"><span style=3D"font-family:'Helvetica'; = font-size:medium; color:rgba(0, 0, 0, 1);"><b>To: </b></span><span = style=3D"font-family:'Helvetica'; font-size:medium;"><a = href=3D"mailto:[email protected]">[email protected]= en.de</a><br></span></div><div style=3D"margin-top: 0px; margin-right: = 0px; margin-bottom: 0px; margin-left: 0px;"><span = style=3D"font-family:'Helvetica'; font-size:medium; color:rgba(0, 0, 0, = 1);"><b>Subject: </b></span><span style=3D"font-family:'Helvetica'; = font-size:medium;"><b>Public release of = seL4</b><br></span></div><br><div>NICTA and Open Kernel Labs have = jointly released seL4. For those not aware of seL4, it is an L4 = microkernel which is formally verified (meaning that the implementation = is mathematically proven to conform to the specification). It is the = world's first (and only) OS kernel that is formally verified in this = strict sense.<br><br>The public release includes the formal = specification of the kernel (ARM version), kernel binaries for x86 and = ARM, and a para-virtualized Linux running on top of = seL4/x86.<br><br>More about seL4: <a = href=3D"http://ertos.nicta.com.au/research/sel4/">http://ertos.nicta.com.a= u/research/sel4/</a><br>NICTA download site: <a = href=3D"http://ertos.nicta.com.au/software/seL4/home.pyl">http://ertos.nic= ta.com.au/software/seL4/home.pyl</a><br><br>Gernot<br></div></blockquote><= /div><br></body></html>= --Apple-Mail-15-492375556--