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:
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@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk



--
    Cheers,
    --MarkM
_______________________________________________
cap-talk mailing list
cap-talk@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk
Ken is an Independent Consultant in South Florida for secure cloud-based software and mobile access software. Graduated in the UK, developed the first Capability-Based Computers (PP-250), became a Charted Engineer, and awarded a Fellowship of the IEE (London). Partnered on a dozen patents developing Object Engineering fundamentals while working in UK, USA, Germany, and Belgium. Invitation speaker at conferences on Operating Systems and Communications.

Comments

Post a Comment