Re: Fwd: seL4 is going open source

Hi Mark and Jonathan,

Thanks for the kind words.

On 5 June 2014 22:58, Mark S. Miller <[email protected]> wrote:
> Why the 54 day delay?

We're not quite ready yet -- there's a lot of cleanup etc. happening
right now that will take a little longer before we're ready to
release. Also, the date was a consensus between NICTA and General
Dynamics C4 Systems, who own seL4 and its original correctness proof
(completed in 2009).

GD came to own seL4 once they acquired Open Kernel Labs in 2012. More
information about how and why OK Labs came to own seL4, which was
developed and verified by NICTA, is contained in the following blog
post by Gernot Heiser:
http://microkerneldude.wordpress.com/2012/10/02/giving-it-away-part-2-on-microkernels-and-the-national-interes/

To respond to Jonathan's concerns, with my personal point of view
(noting that I joined NICTA in 2010, so I'm a relative latecomer):

On 6 June 2014 06:23, Jonathan S. Shapiro <[email protected]> wrote:
> I have mixed
> feelings about it. I think it's worth noting that:
>
> 1. OKL4 actually was open source until OKLabs took it proprietary. That
> doesn't make me feel warm and fuzzy.

I can't speak to the history of OKL4 but, I can say that from my own
personal point of view, I'm looking forward to seL4 having a greater
chance to have impact once it is open sourced, and that I personally
think its best chance of having impact over the long term is if it
remains that way. This release is not a one-off code drop. The code
and proofs we plan to host on github, and will be updated there as we
continue our work at NICTA.  We're of course hoping this will attract
outside contributions too.

> 2. So far as I know, seL4 isn't a kernel that is actually shipping.

That's my understanding too.

> Regardless, I'm delighted to be able to openly examine how NICTA/OKLabs
> approached the formalization and verification process. I'll be interested to
> see if the formalization errors that we have identified in some prior work
> have been addressed.

Can you point me at anything that I could read more on here about
those formalisation errors? That sounds pretty interesting. One of the
things I pushed for early when joining NICTA was to get started on
proving security properties about seL4 so that we could be confident
that the spec against which it had been verified was correct (or at
least useful for enforcing certain security properties). Largely, we
didn't find any big problems with seL4 -- although its capability
deletion semantics turned out to be a little problematic for enforcing
confidentiality, which if you're interested we talk about in the
confidentiality proof paper from Oakland'13:
http://www.nicta.com.au/pub?id=6464

Our success with the subsequent security proofs, having proved both
integrity and confidentiality enforcement, is some evidence that the
original design and functional spec of seL4 was good. Although I don't
know that anyone would ever say that it's perfect. Indeed, the kernel
has evolved a bit since its original state in 2009, with the proofs of
course have been kept up to date with that evolution. You can read
more about our experience maintaining a verified kernel and its
proofs, as the kernel has evolved, in the TOCS paper I linked to in my
earlier message.


> Given the reticence with which the group has reacted to
> questions and issues raised by Scott Doerrie and myself, it will be good to
> be able to carefully examine and review the work.

I'd be happy to try to answer any questions you or Scott have (or have
had in the past). Or feel free to point me at any old posts that
didn't get satisfactory answers and I'll do my best.

>  No proof is perfect. The
> ability to explore their approach in depth is very valuable.

That's what we're hoping. Far too much really good formal methods work
has been locked away over the years (think of all the work that has
gone on at Defence companies that the world has never had the chance
to learn from -- the AAMP7 work comes to mind). I'm glad to say that
seL4 will no longer be in that category.

Cheers

Toby