[cap-talk] Public Release of seL4: a formally verified capability-based microkernel

[David-Sarah Hopwood]

On 2011-02-23 09:15, Matej Kosik wrote:
> On 02/23/2011 04:49 AM, Toby Murray wrote:
>> 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.
> 
> Hi Toby,
> 
> I have always wanted to ask about a this strange thing: does NICTA distinguish between the terms:
> - microkernel
> - (OS) kernel
> - operating system
> ?
> 
> This is strange carelessness compared to rigorousness required for formal verification.

Isn't it perfectly clear what is verified? The download page says:

# The proof applies to the kernel code only, not to any of the provided
# user-level stubs, libraries, applications, or sample code.

"seL4" means the kernel. The OS is called "Linux on seL4". So the message
from Gernot Heiser has not made the error you claim.

I'd like to congratulate the NICTA and OKL researchers for this achievement.
I would be even more enthusiastic if the release were open-source rather than
for "non-commercial use only", but it's a start.

-- 
David-Sarah Hopwood  ⚥  http://davidsarah.livejournal.com

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 292 bytes
Desc: OpenPGP digital signature
Url : http://www.eros-os.org/pipermail/cap-talk/attachments/20110301/2fbd22a1/attachment.bin