On Sun, 3 Jun 2007 19:53:08 +1200, "Shams" shams@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