Re: seL4 is going open source

Hi Jonathan,

good to hear from you, it’s been a while. Also good to see you have lost none of the fire :-)

We completely understand people being sceptical about proofs they can’t see. It’s been frustrating for us as well, and it's why we’ve worked pretty hard with GD to make this open source release happen. As you say, another 50 days and things will be out there.

I do remember the VSTTE’08 discussion, there was terminology in the paper that may have confused people. Theorem 2 should have been called "authority confinement" instead of “isolation of authority". The full formal statement of the theorem is in the paper, though, that’s how you could tell, after all. Nice that science works ;-) And you’ll notice that we have amended our ways and Toby called it authority confinement.

I don’t remember any discussions about Dhammika’s thesis. I wasn’t his supervisor and wasn’t much involved with his thesis, because Dhammika was a student in the kernel team, not my verification team. His supervisor was Kevin, who you might have been talking to. He does take feedback usually very seriously (as did Dhammika) and I’m sure he has passed it on. We’re certainly not in the habit of letting students publish dissertations with unacknowledged known problems. That wouldn’t be a smart move in any case, because theses at UNSW are reviewed and assessed by external reviewers, i.e. the supervisor is not assessing and has no incentive to sweep anything under the rug. This probably was a basic miscommunication. Sorry if that’s been sitting there unresolved for that long.

In any case, as Toby points out, none of these are formally connected to the functional correctness of seL4 or the subsequent security theorems. Dhammika’s work has influenced the kernel mostly from the design side, and his proofs and formalisations were high-level sanity checks of the design. The actual seL4 proofs are orders of magnitude more complex.

For axioms and assumptions, lets have a look at the proofs when they are out and compare to Scott’s work when that is there. We have significantly fewer assumptions than any other previous kernel verification that I’m aware of (in fact, almost any formal software verification in general that I’m aware of), and it will be good for everyone if Scott was able to improve on that. We’ll be quite happy to discuss details.

Cheers,
Gerwin


> Toby:
>
> To respond specifically I'd have to dig through a decade of email for
> just a few messages, and the email isn't even gathered in one place.
> Sorry. Not going to happen. You might consider dropping a note to
> Scott Doerrie - he may be able to gather the exchanges.
>
> The first one I remember is that the main theorem for Dhammika's
> isolation proof from VSTTE'08 is stated incorrectly. 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. 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. 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.
>
> 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.
>
> At this point, these questions have been outstanding for years. The
> answers can wait another 60 days. :-)
>
>
> Jonathan

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.