As far as I can understand, seL4 is not an operating system, it is a microkernel upon which one or more operating systems could be built. The key reason to use seL4 would be due to it providing capabilities based isolation between the layers that run on top of it and thus preventing rogue processes from interfering with other processes.
In the context of "one or more" operating systems, the question arises how to deal with shared resources, such as a USB stack. Imagine multiple OSes handling different USB devices which are all physically connected to the single USB host controller of a Rasperry Pi. What should be the position of the USB stack in this case? We agreed that it should not be in the microkernel. SInce it has to be shared, it can not be part of any one of the OSes. So it would have to exist as a self-contained component (a "server" if you will). But then, how should it be controlled/configured and where does it get its resources from?
Similar thoughts apply to a network stack and, in the case of the Raspi, the NIC is accessed through USB, so we end up with a shared component (networking) on top of another shared component (USB). Tricky...
We are working on a demo implementation for a shared network driver on x86 and can probably post a pointer to that here in a few weeks. The architecture is as you say: if you have multiple VMs that need to share one device, you will usually implement a separate seL4-native driver for that device, which multiplexes the device to the VMs, so that each VM sees a separate virtual device. The sharing and separation policy (and trust) is now encapsulated in that one shared driver. If done right, you should be able to stack these fairly arbitrarily. Writing USB drivers still has its own set of problems and fun, of course. Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.