L4 implementations

[Gernot Heiser]

>>>>> On Sun, 3 Jun 2007 19:53:08 +1200, "Shams" <shams at orcon.net.nz> said:
S> Hi,
S> Regarding OKL4:
S> http://www.ok-labs.com/products/

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

OKL4 is "commercial" in that it is professionally developed and
supported by Open Kernel Labs, and that it is deployed in commercial
products.  Eg Qualcomm ships wireless chipsets where the firmware is
based on OKL4, and Toshiba sells a mobile phone handset that runs
OKL4. There are many other deployments that aren't public yet.

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

OKL4 is based on the L4Ka::Pistachio code base, but has deviated
substantially from it, both in API and implementation. It is still
distributed under a BSD license.

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

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

The high-security API is that of the seL4 project, which is quite
different from L4.Sec. There is plenty of information, including
several very recent publications showing the liveness of the project
on the seL4 website, http://ertos.nicta.com.au/research/sel4/ There is
a prototype implementation, and an executable version of the
specification. The latter will be published as soon as we get our
lawyers to agree to it. We also have formal proofs of certain security
properties of the seL4 API.

The formal correctness proof is targeting the seL4 implementation,
details can be found on the L4.verified web page
http://ertos.nicta.com.au/research/l4.verified/

The OKL4 API is converging towards seL4 in small steps, to ensure a
migration path for existing OKL4e customers.

Gernot