[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: L4.sec

From: Shams
Subject: Re: L4.sec
Date: Sat, 9 Jun 2007 12:43:01 +1200


See our active discussions at comp.micro-kernel.l4.devel:




"Jonathan S. Shapiro" <> wrote in message 
> 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 

reply via email to

[Prev in Thread] Current Thread [Next in Thread]