seL4 Availability (Was: L4.sec)

[Gernot Heiser]

Shap posted a few opinions about seL4 and our commercialisation
agenda. They contain some significant misunderstandings/confusions,
which I'll try to clarify.

On Fri, 08 Jun 2007 10:22:52 -0400, Jonathan S. Shapiro wrote:
shap> [...]

shap> Unfortunately, I suspect that the C implementation will never be
shap> released in open form.

This is a claim that is based on assertions (below) that are
incorrect.

shap> The seL4 team has formed a company, 

Indeed, we set up Open Kernel Labs (OK) for commercialising our
microkernel technology (see http://ok-labs.com).

As everyone can easily confirm from the OK web site
(http://portal.ok-labs.com/), the complete kernel (called OKL4) and
other stuff is downloadable and is under an OSI-approved open-source
license.

It is true that the OKL4 download presently supports fewer
architectures and platforms than the NICTA::Pistachio-embedded
downloads it is derived from. The reasons is that OK only provides
code that is heavily QA-ed, which consumes significant resources, so
some things aren't presently released because they haven't been
through the QA process yet.

There is also some discussion as to the most appropriate open-source
license to use, which is holding up some things. There are no plans to
move away from open-source licenses.

shap> and most of the work is being done by that company.

That's actually *not* true. seL4 and the verification project
L4.verified are all done by NICTA (but, of course, there is excellent
communication between the NICTA and OK researchers and
engineers). Outcomes will be transferred to OK.

shap> They have 30 people employed
shap> already. For those of you who don't have any experience with corporate
shap> finances, 30 people cost between $6M US and $7.5M US per year. Perhaps
shap> 15% less in Australia, but that isn't important to the point I am
shap> making. The company has been operating for at least two years. If you
shap> are externally funded (as they are) the expected return on investment is
shap> generally around 35% per year, compounded annually. In effect, they have
shap> taken out two loans of ~$7.5M each (one for each year). To pay that loan
shap> off, the company would require a valuation *today* of $23.78M. If they
shap> have to wait another year to be saleable, they will need $42.22M.

shap> You can see that the slope is very very steep. Even if they *want* to
shap> release everything, the investors probably will not allow them to do so.

shap> This, by the way, is why The EROS Group chose *not* to fund our
shap> development using investor dollars.

I'm impressed about your knowledge of OK's finances, Jon. Particularly
the external investment/loan is news to me. Given that I am one of the
main shareholders, and a member of the BoD, I somehow doubt that the
company could have had an investment round without me hearing about it ;-)

I'm not going to discuss OK's finances, which are obviously
confidential. But it has been publicly stated before that OK is funded
from revenue.

As to the future status of seL4: We have every intention of providing
an open-source implementation of seL4, when it's ready. Whether we'll
release a prototype or wait until we have a production version is a
management/business decision that will be taken some time in the
future.

A release of the Haskell prototype is overdue. Unfortunately,
releasing stuff from NICTA isn't quite as easy as from a
university. There are lawyers involved :-(

Gernot