Re: L4.sec

At Wed, 6 Jun 2007 18:24:33 +1200,
"Shams" <[email protected]> wrote:
> 
> Hi,
> 
> Has anyone reviewed OKL4 for usage with Hurd?
> http://www.ok-labs.com/technology/

As far as I know this project is based on the seL4 work from NICTA[1].
seL4 is a cross-over between EROS and the previous L4 generations: The
mapping paradigm of L4 is preserved, while kernel object semantics
resemble EROS in some details.

[1] http://ertos.nicta.com.au/research/sel4/

It's an interesting mix, with some things good and some things
uncertain.  Definitely a relevant project, but practical value of the
implementation to us is unclear to me.  The focus is also very
different (formal verification, embedded systems).

Thanks,
Marcus