[Cryptography] Yet more formal methods news: seL4 to go open source

Perry E. Metzger perry at piermont.com
Sun Jun 8 17:56:17 EDT 2014


seL4 is is a fully verified microkernel which, unfortunately, has
been closed source until now. It appears that's about to change,
though the details are still sketchy.

Perry

Begin Forwarded Message:

From: Toby Murray <tobycmurray at googlemail.com>
Date: Thu, Jun 5, 2014 at 7:24 AM
Subject: [cap-talk] Fwd: seL4 is going open source
To: "General discussions concerning capability systems."
<cap-talk at mail.eros-os.org>


cap-talkers:

seL4, a capability-based microkernel whose implementation has been
comprehensively formally verified, is soon to be open source along
with its formal proofs and associated tools.

If you're interested, you can find out more at http://sel4.systems

For those who like academic papers, an overview of seL4 and its
verification is described in the following paper (which I can assure
you is readable without a strong background in formal methods):

Comprehensive formal verification of an OS microkernel
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas
Sewell, Rafal Kolanski and Gernot Heiser
ACM Transactions on Computer Systems, vol. 32, no. 1, pp. 2:1--2:70,
Feb. 2014
http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml

Cheers

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


More information about the cryptography mailing list