Can you use this setup to use Linux's device drivers for SeL4? Given the paranoia level involved, I imagine you'd run a stripped down Linux kernel per driver, with all device commands proxied through L4. Your Linux or whatever other userland would see virtual devices through L4 as well. Possible? Hopelessly inefficient? Or does L4's capability pipelining save the day?