On Fri, 03 Aug 2007 19:10:22 +0200, "Ernst Rohlicek jun." ernst.rohlicek@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