Re: L4.sec

[Jonathan S. Shapiro]

On Fri, 2007-06-08 at 09:19 +0530, Prem Mallappa wrote:
> > [1] http://ertos.nicta.com.au/research/sel4/
> 
> Looks like it is written in Haskell, anybody has/interested in 'C/C++'
> implementation?

This is not quite what is happening. The seL4 project has built an
executable *model* of the system in Haskell. This version is a complete
but unoptimized version of seL4. It runs real application binaries. It
is the one that they are verifying certain properties about. Think of
the Haskell version as providing a low-level formal model.

Separately, they are doing an implementation in a constrained subset of
C (I think it is C rather than C++, but I'm not sure). The idea is to be
able to translate this implementation into their theorem prover as well,
and then to show that it corresponds to the Haskell low-level model. So
there *is* an implementation in C.

There are many missing links in their verification story, but it is very
promising, and it is much further along than anyone else has managed to
get.

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

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

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

Jonathan