Question on multi-partition seL4 image/load for x86
seL4 Developers/SMEs: Does anyone have a seL4 load/configuration that includes more than 2 partitions with at least 2 of the partitions each having a dedicated Ethernet interface assigned to it? I am focused on an x86 host platform. Currently I have a Dell 7910 19" rack unit I am wanting to host on and it has 4 Ethernet ports. Thanks, Jim Marek Enterprise Architect Rockwell Collins
Hey Jim, Apologies, but I'm not sure I understand what you mean by "partition" in this context -- could you please clarify that for me? -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
A virtual machine. Or a “container” that is able to be time and space
isolated from from other containers.
I realize threads in seL4 are nearly as good as partitions in other OS, but
I really want the strict isolation provided by a VM. I am looking to
operate it more like a type 1 hypervisor.
Jim
Sent from my iPhone
On Aug 1, 2018, at 6:26 PM,
Hey Jim,
I took a while to respond because I was verifying my answer:
(1) The current seL4 CAmkES VMM supports multiple concurrent guests on x86, but it doesn't support multiple concurrent guests on ARM. it sounds like you care very strongly about airtight isolation between the guests, but our current CAmkES VMM does not provide this.
(2) If you would like to have multiple guests with their own NICs, you can either:
(2a) Use our Virt-IO Network support, and have the VMM expose a VirtIO-NIC to each of your guests, then have the VMM relay frames sent over the virtio-NIC devices down to a "real" NIC device on the host. It is very likely that you will have to write a new driver for the host NIC you wish to relay the frames out to.
(2b) If your host machine has multiple NICs, you can expose one NIC each to each guest and pass them through as PCI devices: we support presenting fake PCI devices to guests. However this is not "automated", in the sense that you will have to manually select the host NICs you want to expose to the guests, then manually do a PCI bus scan on your target host machine to find out their MMIO ranges, IRQs and IO-ports, and then manually describe those to the VMM ((i) Tell CAmkES where these resources are so that the untypeds get passed through to some designated component and (ii) manually tell the VMM to present a PCI device to each guest, explaining to it what BARs to present to each guest).
(3) Your phrasing implies strongly that you need very strong isolation as part of your mission, but the current CAmkES VMM was not designed to be completely airbag guests.
--
Kofi Doku Atuah
Kernel engineer
DATA61 | CSIRO
________________________________
From: Jim Marek
participants (2)
-
Jim Marek -
Kofidoku.Atuah＠data61.csiro.au