Re: L4.sec

[Shams]

Hi,

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

http://thread.gmane.org/gmane.comp.micro-kernel.l4.devel/2030

Thanks
Shams

-- 

"Jonathan S. Shapiro" <> wrote in message 
news:address@hidden
> 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