Dear Norman,

On 17.04.2017 19:53, Shahbaz khan wrote:
> VirtualBox closely interacts with the virtualization hardware. On Muen,
> this interaction naturally has to go through the Muen SK. By using
> Genode as runtime for VirtualBox, Muen is able to leverage Genode's
> existing solution of the interaction of VirtualBox with a
> microkernel-based virtualization mechanism.
>
>
> Similar to karma-vmm, fiasco.oc and l4linux.

I don't see the connection. My email was not related to Fiasco.OC,
Karma, or L4Linux.

I think I got the problem. Muen subject is not a subject like that of an OS.

> Conceptually, a Muen partition is a hardware platform, similar to a
> board. Like on any board, you can run software directly (in supervisor
> mode). But for running a complex software stack, or more than one
> application, one has to use an operating system (OS). Genode/base-hw
> plays this role.
>
>
> Simply put a build time think. Base-hw kernel means muen sk for genode
> runtime.

Muen can be used without base-hw.

Base-hw can be used without Muen.

Second problem in my mind would be imagining the spartan environment provided by Muen to be fulfilled with Genode runtime minus microkernel. This would be as follows.

Base-HW is a microkernel as you mentioned earlier. Like a layman I ask the name of this microkernel. Is it Nova? Again to my preliminary question ... we run a micro-kernel on microkernel to run virtualbox rather than virtualbox on Muen SK.

But when combined, Genode's version of VirtualBox can run on top of Muen.

Muen is a micro-hypervisor. What is the nature of inter-subject communication? Considering we don't like pure hypervisor approach.

I liked Nova's architecture much more and I would opt for Nova if formal verification could be as simple for it as in Muen. And the luxury of C++ too.

Regards,

Shahbaz