[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