IMHO, the biggest problem with the Raspberry Pi is that most of its I/O (even the NIC) is connected through USB. A serial port is available (albeit without level shifters). So, running the seL4test should be possible without a USB stack, but as soon as you want to access a keyboard, network or filesystem, you'll need one.
You should keep in mind that seL4 is a microkernel. So the USB stack and drivers that depend on that stack should all be implemented as processes/tasks running on top of seL4.
I know it is not cool to mention Minix here, but it and Plan9 suggest ideas as to how the layers above seL4 could be structured.
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.
Am 10.03.2015 um 01:56 schrieb da Tyga:
IMHO, the biggest problem with the Raspberry Pi is that most of its I/O (even the NIC) is connected through USB. A serial port is available (albeit without level shifters). So, running the seL4test should be possible without a USB stack, but as soon as you want to access a keyboard, network or filesystem, you'll need one.You should keep in mind that seL4 is a microkernel. So the USB stack and drivers that depend on that stack should all be implemented as processes/tasks running on top of seL4.
Sure.
Nevertheless, for debug purposes at least, even seL4 uses a serial channel of some kind. Luckily for any seL4 porting effort, the Raspi has a UART and it is accessible directly, not through USB. Otherwise the microkernel would have to handle USB...
I know it is not cool to mention Minix here, but it and Plan9 suggest ideas as to how the layers above seL4 could be structured.
I believe NICTA and others have been/are actively working on that.
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...
Robert
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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.
-
da Tyga -
Gerwin Klein -
Robert Kaiser