Re: Fwd: seL4 is going open source

(cc'ing Gerwin to give him the chance to respond if he wishes)

On 7 June 2014 04:17, Jonathan S. Shapiro <[email protected]> wrote:
> the main theorem for Dhammika's
> isolation proof from VSTTE'08 is stated incorrectly.

Dhammika's take-grant was improved upon by Andrew Boyton, in:
https://www.ssrg.nicta.com.au/publications/nictaabstracts/Boyton_09.abstract.pml

I'd be curious to know what the error was and if it is present in
Andrew's work too.

My understanding is that the original plan was to complete a proof of
refinement between seL4's functional abstract specification (against
which its implementation was verified) and Andrew's take-grant model
(i.e. to prove that seL4 implements a take-grant capability model);
but that didn't eventuate. Instead, we proved security theorems
directly about the functional specification that were much stronger
than linking it to a take-grant protection model. In particular, the
proofs of authority confinement, integrity and confidentiality give
much better guarantees and provide a better basis for reasoning about
systems built on seL4 than a take-grant style model.

Building on something Thomas Sewell once said to me, take-grant allows
you to compute the fixed point of capability distribution. But better
is to simply start at that fixed point (which is roughly what the
authority confinement proofs do) and then reason about what you can
enforce from that fixed point (as we did in terms of integrity and
confidentiality).

> His dissertation
> contains further substantive errors that Scott Doerrie pointed out
> privately during reviews of early drafts. We included Gerwin in some
> of those exchanges. It's very possible that we misinterpreted his
> response, but the sense we got seemed to be "It's just a dissertation,
> why fix it?" I think he was worried about delaying Dhammika's
> completion, but I think it's very problematic to publish a
> dissertation with known, unacknowledged errors - especially a
> verification dissertation.

Having worked closely with Gerwin for the last 4 years I can only
assume he was misinterpreted here. I have vivid memories of Gerwin
carefully correcting my informal explanations of the integrity and
authority confinement properties we proved about seL4, to make sure
they corresponded exactly to the formal theorems -- he is nothing if
not careful.

> At the time, Gerwin's seeming lack of
> interest reduced my confidence in the OKL4 verifications more
> generally, but as I say we may not have understood the sense of his
> responses correctly. It may be that Dhammika's work wasn't relied on
> in the mainstream OKL4 verification, so perhaps I shouldn't draw broad
> conclusions too quickly.

(I know you know, but for anyone else: OKL4 isn't verified, and is
completely independent of seL4.)

None of the take-grant work (Andrew's or Dhammika's) was relied on in
the mainstream verification work, as alluded to above.

> Now that the verifications are to be
> published, we'll be able to check them. More importantly, we'll be
> able to understand how the seL4 API has been pruned in comparison to
> the OKL4 API. Or at least the legacy OKL4 API, the current version not
> being public.

Not knowing OKL4 closely, my understanding is that seL4 is not a
subset of OKL4 -- even given that the two kernels were independent
developments. For instance, seL4 allows capabilities to be passed in
IPC, which I had thought OKL4 does not. seL4 was not designed by
starting with OKL4 and pruning everything that couldn't be verified.
But instead by starting from first principles that were different to
those that drove OKL4's design (e.g. seL4's memory allocation model
comes to mind here). I don't know if Kevin & Gernot's SOSP paper from
last year might have more to say here:
http://www.ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml


> The other issue that has concerned us at various points is that the
> verification efforts we saw were not axiom free. Some of the axioms we
> encountered were both non-obvious and non-trivial. This is a source of
> concern for two reasons. First, we're not convinced those verification
> results actually hold. But more importantly, if a single one of those
> axioms turns out to be wrong then the entire *family* of verifications
> that rely on them are unsound. Scott's forthcoming dissertation work
> *is* axiom-free. Relying on axioms would have cut years off of his
> doctoral work, but having actually doing the work we're even *more*
> suspicious of axioms than we were at the beginning.

The axiomatised bits of the seL4 verification that come to mind are:
  - the kernel's assembly code
  - the kernel's initialisation code
  - the fact that the machine operations that the kernel performs do
not destroy the kernel's view of the world
  - (see the papers for a better description that I can come up with
off the top of my head...)

Each of these can of course be verified, with more effort. However,
only under other axioms, such as:
  - the hardware correctly implements the ISA spec

When trying to talk about the real world, one must always axiomatise
the behaviour of the bits of the world one doesn't want to verify. I
cannot see how that can be avoided. Such axioms, I agree, should
always be treated with suspicion until they can be validated (by
consensus if so be it).

I'll await Scott's dissertation to learn more about the axioms he
avoids that the seL4 verification does not. But note that since 2009,
one of the things we've been working on is reducing that set of
axioms. Thomas Sewell's verification (with Magnus Myreen) of the gcc
compilation of seL4 at last year's PLDI is a good example, allowing us
to largely remove the compiler from the TCB:
http://www.nicta.com.au/pub?id=6449

Of course, you'll always have the axioms that underpin the logic in
which you're working. These are usually easy for everyone to agree on,
such as for any term t, "t = t". Although, the constructivists might
take issue with the law of excluded middle -- I guess you can't please
everyone :)

Cheers

Toby