L4.sec status ping

[Gernot Heiser]

>>>>> On Fri, 03 Aug 2007 19:10:22 +0200, "Ernst Rohlicek jun." <ernst.rohlicek at inode.at> said:

ERj> [...]

ERj> In the paper, there is a mention of a "Coyotos" project by Mr. Shapiro,
ERj> also striving to create a high-security microkernel. Where would you see
ERj> seL4's strengths compared to Coyotos and vice versa?

seL4 is an OL4 kernel, so it provides an upgrade path for existing
commercial deployments of L4.

Also, seL4 will have a formal correctness proof, i.e., a mathematical
proof that the security (and other) properties proved about the API
will hold for the actual implementation. No such proof exists for any
system out there, nor is likely to exist for any other system in the
foreseeable future (see http://ertos.nicta.com.au/research/l4.verified/).

>> The commercial OKL4 microkernel is converging on the seL4 API, it
>> presently contains simplified versions of IPC control and all kernel
>> resource allocation is under control of a user-level policy server. It
>> should implement a full seL4 API probably sometime next year.

ERj> I've already come across OKL4 - I've always wondered what would happen
ERj> when OKL4 has actually developed into an seL4 API implementation.

ERj> Was OKL4 started as a second chance effort "should seL4 not work out" or
ERj> "should it take longer than anticipated" or simply to allow clients
ERj> using L4 to slowly migrate with each OKL4 realease toward seL4? Will
ERj> they co-exist or will one be selected?

No, OKL4 is the commercially-supported version of what used to be
called L4-embedded. It wasn't "started" in that sense, it was
continued to provide commercial support for pre-existing and new commercial
customers. It's out there in end-user products (see the recent
announcement about the Toshiba phone).

seL4 was done initially as a separate code base (forked from
L4-embedded) to avoid hampering the research project with commercial
realities, but while it is progressing, the OKL4 API is being
successively adapted towards seL4. Having a large customer base (with
many big multinationals) we need to be gentle with API changes. Most
of it will be dealt with by migrating customers to a higher-level API
that hides most changes.

ERj> Thanks for your time and the update on seL4; I really appreciate it.

Welcome,
Gernot