Still Active Development

[Lonnie Cumberland]

greetings all,

I have been watching Muen SK for a while now and like what I have been learning about Separation Kernels. I think that they have a huge potential.

I am really now wondering if Muen is still being actively developed as I would like to possibly investigate developing a type of SK/hypervisor  hybrid that would possibly combine Muen and Bhyve as the VMM but do not know how difficult thiswill be yet.

There was a Genode project in the past that combined Genode + Muen SK + a stripped down version of VirtualBox but I have not heard much about this for some time now.

My interest is in being able to run X86_64 (and possible some 32-bit OS's as well) for Windows, Linux, and possibly a few others.

Being a separation kernel, I would guess that Muen should be able to run these natively without any paravirtualization implemented.

Currently, on the hypervisor side, I have been playing around with CXP-ng (Xen) and SmartOS and like what they can do, but still an strangely drawn to the idea of a Separation Kernel implementation with perhaps some Type-1 components to be a hybrid SK where (LynxSecure is a similar commercial version that I think Muen could evolve into over time.

Any thoughts?

Best Regards,

Lonnie

[Adrian-Ken Rueegsegger]

Hello Lonnie,

Welcome back to the list :)

On 7/11/19 12:04 PM, Lonnie Cumberland wrote:
> greetings all,
>
> I have been watching Muen SK for a while now and like what I have been
> learning about Separation Kernels. I think that they have a huge potential.
>
> I am really now wondering if Muen is still being actively developed as I
> would like to possibly investigate developing a type of SK/hypervisor
> hybrid that would possibly combine Muen and Bhyve as the VMM but do not
> know how difficult thiswill be yet.

The Muen project is very much alive and well. Four weeks ago, we tagged
a minor release v0.9.1 with the accumulated changes over the past year
or so and since then we have merged more code into the devel branch
(most notably Tau0, a system resource manager written in SPARK 2014).

Additionally, we, the Muen core team, founded a company [1] in the
beginning of 2019 to continue development of the Muen SK platform
and provide commercial services around it.

Regarding Bhyve: currently, FreeBSD is not supported as a subject on top
of Muen. There was a student working on this topic as part of his
bachelor thesis, however the results are currently not in a shape to be
published. Of course, we would like to see this work released but due to
other topics having higher priority we will not be able to work on this
in the foreseeable future unfortunately.

> There was a Genode project in the past that combined Genode + Muen SK + a
> stripped down version of VirtualBox but I have not heard much about this
> for some time now.

Support for running Genode/VirtualBox 4.x on top of Muen was introduced
in Genode with release 16.08 [2]. Due to the maintenance burden to
upgrade from one VBox version to the next, we decided earlier this year
to no longer work/extend the Genode/VirtualBox support on top of Muen,
see the 19.02 release notes [3]. That being said, it is still possible
to run Genode/VirtualBox as a VMM with Genode versions prior to 19.02 on
top of Muen.

> My interest is in being able to run X86_64 (and possible some 32-bit OS's
> as well) for Windows, Linux, and possibly a few others.
>
> Being a separation kernel, I would guess that Muen should be able to run
> these natively without any paravirtualization implemented.

We have started looking into nested virtualization in order to support
different VMMs on top of Muen without the need for adaptations to the
guest hypervisor. With our (early) prototype we are able to run Linux
and Windows 10 64-bit guests on top of Linux/KVM. However, we are still
quite a bit away from being able to release this code since it is
currently an early prototype intended for design validation. The crucial
point is to not introduce unnecessary complexity into the SK while still
being able to host hypervisors on top of Muen.

Regards,
Adrian

[1] - https://www.codelabs.ch/
[2] -
https://genode.org/documentation/release-notes/16.08#VirtualBox_4_on_top_of_the_Muen_separation_kernel
[3] -
https://genode.org/documentation/release-notes/19.02#Updated_or_removed_3rd-party_software

[Lonnie Cumberland]

Hello Adrian,

Welcome back to the list :)

Happy to be back and hope that I can contribute more now as the project goes forward. 

>
> I have been watching Muen SK for a while now and like what I have been
> learning about Separation Kernels. I think that they have a huge potential.
>
> I am really now wondering if Muen is still being actively developed as I
> would like to possibly investigate developing a type of SK/hypervisor
> hybrid that would possibly combine Muen and Bhyve as the VMM but do not
> know how difficult thiswill be yet.

The Muen project is very much alive and well. Four weeks ago, we tagged
a minor release v0.9.1 with the accumulated changes over the past year
or so and since then we have merged more code into the devel branch
(most notably Tau0, a system resource manager written in SPARK 2014).

Looks like I will have to catch up on the code and read up on SPARK 2104 much more. 

Additionally, we, the Muen core team, founded a company [1] in the
beginning of 2019 to continue development of the Muen SK platform
and provide commercial services around it.

This is very exciting to know that you founded a company for Muen development. 

Regarding Bhyve: currently, FreeBSD is not supported as a subject on top
of Muen. There was a student working on this topic as part of his
bachelor thesis, however the results are currently not in a shape to be
published. Of course, we would like to see this work released but due to
other topics having higher priority we will not be able to work on this
in the foreseeable future unfortunately.

In this regard, I may try to dig into things enough to see if I can give it a shot, provided that time permits. 

> There was a Genode project in the past that combined Genode + Muen SK + a
> stripped down version of VirtualBox but I have not heard much about this
> for some time now.

Support for running Genode/VirtualBox 4.x on top of Muen was introduced
in Genode with release 16.08 [2]. Due to the maintenance burden to
upgrade from one VBox version to the next, we decided earlier this year
to no longer work/extend the Genode/VirtualBox support on top of Muen,
see the 19.02 release notes [3]. That being said, it is still possible
to run Genode/VirtualBox as a VMM with Genode versions prior to 19.02 on
top of Muen.

Yea, I saw the Genode/VirtualBox version some time ago but it did not run very well at that time and I was wondering if there were updates since that time. 

> My interest is in being able to run X86_64 (and possible some 32-bit OS's
> as well) for Windows, Linux, and possibly a few others.
>
> Being a separation kernel, I would guess that Muen should be able to run
> these natively without any paravirtualization implemented.

We have started looking into nested virtualization in order to support
different VMMs on top of Muen without the need for adaptations to the
guest hypervisor. With our (early) prototype we are able to run Linux
and Windows 10 64-bit guests on top of Linux/KVM. However, we are still
quite a bit away from being able to release this code since it is
currently an early prototype intended for design validation. The crucial
point is to not introduce unnecessary complexity into the SK while still
being able to host hypervisors on top of Muen.

If I understand separation kernels correctly, then they allow for OS's to run on native hardware by just segregating the resources (CPU's, Memory, etc..) effectively into partitions (i.e. smaller protected computers) in which a VMM may not be required. Would this be fair to say?  If so, then cannot one, or both, of those native partitions already run Linux/Windows 64-bit OS's directly?

I am still learning more about SK systems , but it seems that VMM's are required if you want to virtualize OS's to run many, perhaps on limited resources or possibly run OS's that need a different configuration than the current hardware supports (i.e. Bochs full virtualization comes to mind here), but for an SK like Muen (or LynxSecure although its a hybrid SK/Virtualizer) it is a matter of resource partitioning, correct?

I would like to compile up everything on my Ubuntu 18.04, or perhaps on the Docker container for Muen Development that I just found on Docker Hub which may be a better way to get setup and developing quicker.

Thanks again

Lonnie