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