Genode 15.05 is out and brings the Muen Separation Kernel

Genode 15.05 is out and brings the Muen Separation Kernel

[kug1977]

Hi, 

Genode 15.05 was released, which is as itself nothing worth mention, but this release comes with the Muen Seperation Kernel, which is written in SPARK. So I think, this is Ada related and you might be interested. 

See the release note here: http://genode.org/documentation/release-notes/15.05

So at least two proven error free kernel are shipped with Genode: Muen and seL4.

King regards
kug1977

Re: Genode 15.05 is out and brings the Muen Separation Kernel

[Adrian-Ken Rueegsegger]

Hello,

On 05/27/2015 10:29 AM, kug1977@web.de wrote:
> Hi, 
> 
> Genode 15.05 was released, which is as itself nothing worth mention, but this release comes with the Muen Seperation Kernel, which is written in SPARK. So I think, this is Ada related and you might be interested. 

It is a nice surprise to see that this work is being noticed ;)

> See the release note here: http://genode.org/documentation/release-notes/15.05
> 
> So at least two proven error free kernel are shipped with Genode: Muen and seL4.

Just a minor clarification: the Genode release 15.05 does not ship with
the support for running on top of the Muen Separation Kernel. Even
though the porting work has been done [1] and works on Bochs as well as
on real hardware, we have not yet submitted it upstream for integration
into the Genode OS Framework.

Having said that, we expect that Muen support will land in Genode soon.

Regards,
Adrian

[1] - https://github.com/codelabs-ch/genode/tree/hw_x86_64_muen

Re: Genode 15.05 is out and brings the Muen Separation Kernel

[kug1977]

I'm a follower of L3/L4 for a long time now and it's impressiv what's happen in the microkernel development. But I'm not a good programmer, to understand all concepts and the proven part in seL4 was far away from the thinks I can imagen in my brain. So the questions I've on Muen: Can you use the theorems from seL4 and bring them over to SPARK and use them to ptove your kernel? Or have you to start fram scratch?