Re: L4.sec

[Jonathan S. Shapiro]

On Fri, 2007-06-08 at 00:12 +0200, Marcus Brinkmann wrote:
> At Wed, 6 Jun 2007 18:24:33 +1200,
> "Shams" <address@hidden> 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.

I believe that seL4 and L4.sec are independent projects. Both have
borrowed elements from EROS and (of course) from previous L4
generations.

shap

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

Yes. seL4 is very focused on embedded systems. It is also very
disturbing that they have borrowed greatly from the open community, but
the majority of their results are proprietary.

shap