Fwd: [cap-talk] Fwd: seL4 is going open source

Sent from my iPhone

Begin forwarded message:

From: "Mark S. Miller" <erights@google.com>
Date: June 5, 2014 at 8:58:24 EDT
To: "General discussions concerning capability systems." <cap-talk@mail.eros-os.org>
Subject: Re: [cap-talk] Fwd: seL4 is going open source
Reply-To: "General discussions concerning capability systems." <cap-talk@mail.eros-os.org>

Toby, this is great news! Congratulations!

Why the 54 day delay? Why not open source what you have now? If the reason is only to celebrate the anniversary, that seems a silly reason for maintaining the threat of legal action for activities you now intend to allow. Today, as it happens, is also Reset The Net day <https://www.resetthenet.org/>. Perhaps that could serve as a good enough reason to make the announcement today rather than in 54 days?

In any case, this is awesome news. It may very well change the world. Thanks for this work and this gift to the world!

On Thu, Jun 5, 2014 at 4:24 AM, Toby Murray <tobycmurray@googlemail.com> wrote:

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


cap-talk mailing list

cap-talk mailing list