headers
Shams | 6 Jun 2007 08:24
Picon
Favicon

Re: L4.sec

Hi,

Has anyone reviewed OKL4 for usage with Hurd?
http://www.ok-labs.com/technology/

It seems to be commercially supported, muture with BSD.

Thanks
Shams

-- 

"Marcus Brinkmann" <marcus.brinkmann <at> ruhr-uni-bochum.de> wrote in message 
news:874plslxjr.wl%marcus.brinkmann <at> ruhr-uni-bochum.de...
> At Thu, 31 May 2007 14:25:00 +1200,
> "Shams" <shams <at> orcon.net.nz> wrote:
>>
>> Hi,
>>
>> I have read that L4.Sec might be a candidate for Hurd.
>>
>> Does anyone know if L4.Sec is supposed to replace L4.Pistachio
>> and/or L4.Fiasco?
>
> L4.sec is developed in Dresden, while Pistachio was developed in
> Karlsruhe.  The available draft document indicates that it is more of
> a mini-revolution than an evolution of previous L4 architectures.
> Although I am involved in none of the projects you reference, I would
> expect that they will be continued in parallel for quite some time.
>
(Continue reading)

Permalink | Reply | 6 comments |
headers
Marcus Brinkmann | 8 Jun 2007 00:12
Picon
Favicon

Re: L4.sec

At Wed, 6 Jun 2007 18:24:33 +1200,
"Shams" <shams <at> orcon.net.nz> wrote:
> 
> Hi,
> 
> Has anyone reviewed OKL4 for usage with Hurd?
> http://www.ok-labs.com/technology/

As far as I know this project is based on the seL4 work from NICTA[1].
seL4 is a cross-over between EROS and the previous L4 generations: The
mapping paradigm of L4 is preserved, while kernel object semantics
resemble EROS in some details.

[1] http://ertos.nicta.com.au/research/sel4/

It's an interesting mix, with some things good and some things
uncertain.  Definitely a relevant project, but practical value of the
implementation to us is unclear to me.  The focus is also very
different (formal verification, embedded systems).

Thanks,
Marcus
Permalink | Reply | 5 comments |
headers
Prem Mallappa | 8 Jun 2007 05:49
Picon

Re: L4.sec

> [1] http://ertos.nicta.com.au/research/sel4/

Looks like it is written in Haskell, anybody has/interested in 'C/C++'
implementation?
Permalink | Reply | 2 comments |
headers
Jonathan S. Shapiro | 8 Jun 2007 16:13

Re: L4.sec

On Fri, 2007-06-08 at 00:12 +0200, Marcus Brinkmann wrote:
> At Wed, 6 Jun 2007 18:24:33 +1200,
> "Shams" <shams <at> orcon.net.nz> wrote:
> > 
> > Hi,
> > 
> > Has anyone reviewed OKL4 for usage with Hurd?
> > http://www.ok-labs.com/technology/
> 
> As far as I know this project is based on the seL4 work from NICTA[1].
> seL4 is a cross-over between EROS and the previous L4 generations: The
> mapping paradigm of L4 is preserved, while kernel object semantics
> resemble EROS in some details.

I believe that seL4 and L4.sec are independent projects. Both have
borrowed elements from EROS and (of course) from previous L4
generations.

shap

> 
> [1] http://ertos.nicta.com.au/research/sel4/
> 
> It's an interesting mix, with some things good and some things
> uncertain.  Definitely a relevant project, but practical value of the
> implementation to us is unclear to me.  The focus is also very
> different (formal verification, embedded systems).

Yes. seL4 is very focused on embedded systems. It is also very
disturbing that they have borrowed greatly from the open community, but
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jonathan S. Shapiro | 8 Jun 2007 16:22

Re: L4.sec

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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Jonathan S. Shapiro | 8 Jun 2007 16:25

Update on Coyotos

Yesterday, a hand written program executed a complete system callon
IA-32. It wasn't "invoke capability", but that will be next. If we can
do this, it means that the page fault path is working, the interrupt
handling is at least working for the timer code (extending that is
easy), the kernel object handling code is working. We expect the
invocation path to be working by end of month, but things are a little
crazy right now (two proposal deadlines this month, so lots of work).

Oh. The kernel is multiprocessor version, but we have not yet enabled or
attempted to debug the second CPU.

shap
Permalink | Reply | 0 comments |
headers
Shams | 9 Jun 2007 02:43
Picon
Favicon

Re: L4.sec

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:1181312572.21368.12.camel <at> shap.om-md.eros-os.com...
> 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.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gernot Heiser | 9 Jun 2007 07:24
Picon
Favicon

Re: L4.sec

On Fri, 08 Jun 2007 10:13:11 -0400, Jonathan S. Shapiro wrote:
shap> On Fri, 2007-06-08 at 00:12 +0200, Marcus Brinkmann wrote:
> At Wed, 6 Jun 2007 18:24:33 +1200,
> "Shams" <address <at> hidden> wrote:
> > 
> > Hi,
> > 
> > Has anyone reviewed OKL4 for usage with Hurd?
> > http://www.ok-labs.com/technology/
> 
> As far as I know this project is based on the seL4 work from NICTA[1].

Present OKL4 is based on earlier NICTA work (L4-embedded), but the
roadmap integrates seL4 and L4.verified.

> seL4 is a cross-over between EROS and the previous L4 generations: The
> mapping paradigm of L4 is preserved, while kernel object semantics
> resemble EROS in some details.

shap> I believe that seL4 and L4.sec are independent projects. Both have
shap> borrowed elements from EROS and (of course) from previous L4
shap> generations.

Correct.

> [1] http://ertos.nicta.com.au/research/sel4/
> 
> It's an interesting mix, with some things good and some things
> uncertain.  Definitely a relevant project, but practical value of the
> implementation to us is unclear to me.  The focus is also very
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gernot Heiser | 9 Jun 2007 08:38
Picon
Favicon

seL4 Availability (Was: L4.sec)

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.
(Continue reading)

Permalink | Reply | 7 comments |
headers
Gernot Heiser | 10 Jun 2007 06:40
Picon
Favicon

seL4 Verification (Was: L4.sec)

On Fri, 08 Jun 2007 10:22:52 -0400, Jonathan S. Shapiro wrote:
shap> 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?

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

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

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

Shap is essentially right. There are always some "missing links", but
they aren't where people might suspect them.

Let's look at what we have:

1) semi-formal (hacker-readable) spec written in Literal Haskell
(Continue reading)

Permalink | Reply | 501 comments |

Gmane