[prev in list] [next in list] [prev in thread] [next in thread] 

List:       cap-talk
Subject:    [cap-talk] Public Release of seL4: a formally verified
From:       Toby Murray <toby.murray () comlab ! ox ! ac ! uk>
Date:       2011-02-23 3:49:23
Message-ID: AANLkTi=seBZ224eFZ7peXORVF+y2SM5yGBjgMyUppBQV () mail ! gmail ! com
[Download RAW message or body]

Members of this mailing list may be interested in the announcement
below, from Gernot Heiser.

Begin forwarded message:
> From: Gernot Heiser <gernot <at> cse.unsw.edu.au>
> Date: 2 February 2011 17:09:11 AET
> To: l4-hackers <at> os.inf.tu-dresden.de
> Subject: Public release of seL4
> 
> 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. 
> 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. 
> More about seL4: http://ertos.nicta.com.au/research/sel4/
> NICTA download site: http://ertos.nicta.com.au/software/seL4/home.pyl
> 
> Gernot

I should point out that seL4 is capability-based, and research at
NICTA is now focusing on how seL4, and its proof of correctness, can
be used to build truly trustworthy systems with proofs of their
security, see e.g.
http://ertos.nicta.com.au/publications/papers/Klein_10.abstract

[Full disclosure: I am a NICTA employee, working on part of the
research agenda outlined in the linked paper above. I was not involved
in the development of seL4 or its proof of functional correctness-- I
joined NICTA after that work had been completed.]

_______________________________________________
cap-talk mailing list
cap-talk@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk


[prev in list] [next in list] [prev in thread] [next in thread]