Re: Fwd: seL4 is going open source

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