Re: L4.sec

[Gernot Heiser]

On Fri, 08 Jun 2007 10:13:11 -0400, Jonathan S. Shapiro wrote:
shap> 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].

Present OKL4 is based on earlier NICTA work (L4-embedded), but the
roadmap integrates seL4 and L4.verified.

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

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

Correct.

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

shap> Yes. seL4 is very focused on embedded systems.

I'd say it's primarily focussed on embedded systems. Which means we
care about things like memory footprint (not just cache footprint),
and hard real-time capability (we want to be able to *guarantee*
worst-case latencies). This doesn't mean it won't be suitable for
non-embedded use. See the Darbat project, which is based on
Pistachio-embedded (and there are other projects using our "embedded"
kernels which aren't considered in the embedded domain, unfortunately
I can't presently talk about those).

shap> It is also very disturbing that they have borrowed greatly from
shap> the open community, but the majority of their results are
shap> proprietary.

Shap expands on this in his next posting, I'll reply to that one
instead.

Gernot