Genode, seL4 and VirtualBox

[Chris Rothrock]

I'm working with the team at Critical Technologies and I am trying to get
this combination to work - Genode with seL4 microkernel and the VirtualBox
module (using TinyCore Linux).

Let me first start off with saying that Genode, Nova and VirtualBox works
flawlessly - I can boot (an Intel-based machine) and go into either a
command line or GUI environment. The problem is when I try using seL4. I
can compile this without any errors. The ISO image is made perfectly, it
boots to this image on the same hardware - but that's where it stops. One
time only I was able to see the loading screen of TinyCore Linux within
VirtualBox but the boot time for this took about 45 minutes and I was
unable to reproduce this boot.

I guess my first question is this - does seL4 have the necessary
virtualization support for this module? If so, how can I make this work
reliably?

[Alexander Boettcher]

Hello,

Post by Chris Rothrock
Let me first start off with saying that Genode, Nova and VirtualBox works
flawlessly - I can boot (an Intel-based machine) and go into either a
command line or GUI environment. The problem is when I try using seL4. I
can compile this without any errors. The ISO image is made perfectly, it
boots to this image on the same hardware - but that's where it stops. One
time only I was able to see the loading screen of TinyCore Linux within
VirtualBox but the boot time for this took about 45 minutes and I was
unable to reproduce this boot.

what you are executing is Virtualbox without any hardware assisted
virtualization support. Mainly you were running Virtualbox just with the
module called "Recompiler" (REM), which is based on some older Qemu version.

Solely Genode/hw on Muen (32bit VM, one vCPU) and Genode/NOVA (32/64 bit
VMs and multiple vCPUs) are supported on x86 with full hardware assisted
virtualization (Intel's VT-x).

Post by Chris Rothrock
I guess my first question is this - does seL4 have the necessary
virtualization support for this module?

No, afaik. The supported version of Genode/seL4 is based on seL4 3.2.0.

According to [0] and [1] the required virtualization features for x86
got added later to seL4 master. Probably seL4 4.0 have the required
support, if I'm not mistaken.

Post by Chris Rothrock
If so, how can I make this work reliably?

Without updating Genode/seL4 to a recent seL4 kernel version - as first
step - I think you can't. So, in principle all the limitations as
mentioned in the 16.08 Genode release for our Genode/seL4 support still
apply [2].

[0] https://sel4.systems/pipermail/devel/2016-December/001161.html
[1] https://sel4.systems/Info/Roadmap/
[2] https://genode.org/documentation/release-notes/16.08#Limitations


Regards,

[Steven Harp]

Post by Alexander Boettcher
...
According to [0] and [1] the required virtualization features for x86
got added later to seL4 master. Probably seL4 4.0 have the required
support, if I'm not mistaken.

Post by Chris Rothrock
If so, how can I make this work reliably?

Without updating Genode/seL4 to a recent seL4 kernel version - as first
step - I think you can't. So, in principle all the limitations as
mentioned in the 16.08 Genode release for our Genode/seL4 support still
apply [2].
[0] https://sel4.systems/pipermail/devel/2016-December/001161.html
[1] https://sel4.systems/Info/Roadmap/
[2] https://genode.org/documentation/release-notes/16.08#Limitations

The combination of Genode and seL4 *is* particularly attractive.
How large an effort does upgrading to seL4 4.x represent?

Would this be any easier with seL4 on the ARM platform? I guess this is
not yet a supported combination, but should be possible...?

Regards,
Steve Harp

[Chris Rothrock]

We have also been putting forth the effort for Genode/seL4 on ARM with
mixed success on different ARM platforms. As it stands, if we can get an
ARM platform working with Genode/seL4 and especially with a VirtualBox
environment this would make us very happy. I doubt this combination is
even close to ready, however.

Post by Steven Harp

Post by Alexander Boettcher
...
According to [0] and [1] the required virtualization features for x86
got added later to seL4 master. Probably seL4 4.0 have the required
support, if I'm not mistaken.

Post by Chris Rothrock
If so, how can I make this work reliably?

Without updating Genode/seL4 to a recent seL4 kernel version - as first
step - I think you can't. So, in principle all the limitations as
mentioned in the 16.08 Genode release for our Genode/seL4 support still
apply [2].
[0] https://sel4.systems/pipermail/devel/2016-December/001161.html
[1] https://sel4.systems/Info/Roadmap/
[2] https://genode.org/documentation/release-notes/16.08#Limitations

The combination of Genode and seL4 *is* particularly attractive.
How large an effort does upgrading to seL4 4.x represent?
Would this be any easier with seL4 on the ARM platform? I guess this is
not yet a supported combination, but should be possible...?
Regards,
Steve Harp
------------------------------------------------------------
------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
genode-main mailing list
https://lists.sourceforge.net/lists/listinfo/genode-main