L4 implementations

[Jorge Torres]

Hi Shams,

On 6/3/07, Shams <shams at orcon.net.nz> wrote:

> 1. Is OKL4 is a commercial implementation of L4?


I'm not sure about what you mean by commercial, but OKL4  is still BSD
licensed,
As far as I understand, Open kernel labs is a son of NICTA, with the purpose
of commercializing ERTOS research program developments, you may find more
information about this at NICTA's web site.

2. Is OKL4  based on the L4.Pistachio code base and still open-source
> but with a separate source tree?


 L4.Pistachio is developed  and maintained by the System Architecture Group
at the University of Karlsruhe, people from U of new south wales used it to
make their l4.embedded, and added a minimal OS personality called iguana,
the L4.embedded  API has changed a lot in the last  year,  and it is now
released under the name of OKL4, by open kernel labs.
OKL4=OKL4 microkernel + iguana + wombat

3. The OKL4 roadmap http://www.ok-labs.com/products/product_roadmap
> mentions "High-security API" and "Formal correctness proof".


What I understand is that the formal correctness  proof its being worked  in
team with NICTA, using Isabelle.

Does this mean that L4.Sec may or is already getting implemented in OKL4?


I think they are two different things.


Well hope it helps.

Thanks
> Shams
>
>
>
>
> _______________________________________________
> l4-hackers mailing list
> l4-hackers at os.inf.tu-dresden.de
> http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://os.inf.tu-dresden.de/pipermail/l4-hackers/attachments/20070603/659d7e8e/attachment.htm>