L4.sec status ping

[Gernot Heiser]

>>>>> On Wed, 01 Aug 2007 23:42:54 +0200, "Ernst Rohlicek jun." <ernst.rohlicek at inode.at> said:
ERj> Hello everyone,
ERj> I would just like to ask about the current status or some roadmap for
ERj> L4.sec? Is it actively being worked on?

ERj> Reason is: I need to choose a microkernel to start working on an
ERj> experimental operating system within this year I need some facts for
ERj> decision-making - and I would prefer a capability-based one like L4.sec.

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.

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.

Gernot