L4.sec status ping

[Ernst Rohlicek jun.]

> If you are looking for a capability-based L4 kernel you should have a
> look at seL4: http://ertos.nicta.com.au/research/sel4/
> 
> Work on this is quite advanced, see for example
> http://ertos.nicta.com.au/publications/papers/Elphinstone_KDRH_07.pdf
> 
> The API is quite stable by now and will be released shortly (the only
> reason it isn't released yet is that we have to deal with lawyers and
> no-one wants to spend their time on this ;-). There is also an
> executable model of the API (aka simulator) that supports running ARM
> binaries built with a standard GNU toolchain, so you can port software
> to it. That executable model should be released at the same time as
> the API.

That is good to hear - I thought seL4 would take a longer time to a
first (even if alpha/beta) release. I'm looking forward to it!

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


> 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.

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

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

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


Greetings,

Ernst Rohlicek jun.
<ernst.rohlicek at inode.at>