General question about software
So, I know that at a basic level, a block device driver would probably need I/O permissions, and I'm guessing that it would be handling requests from a file system driver. Is that basically how the seL4 software ecosystem is laid out? What's typical for how "software in the wild" is actually organized and layered on top of the microkernel? I only know about seL4 from a theoretical standpoint, read the manual and stuff, and mostly familiar with the actual kernel, but I'm a complete noob when it comes to actual software.
Hi Raymond, seL4 is a general purpose microkernel, which means that it supports any architecture you wish to put on top of it. These architectures can vary on many axis of dynamism, componentisation etc. The 'typical' architecture therefore is hard to pin down, as it depends upon how you want to leverage the benefits of seL4 in your system, but there are some common points in the design space. Splitting a piece of software into several components, that run in their own isolated address spaces, is one of the core designs seen on any microkernel. How fine you make your components depends upon what kinds of isolation you want and where you are placing trust. It is valid, for example, to place a disk driver in the same component as the file system driver, but it is also valid for them to be in different components. Systems can have varying levels of dynamism, which is really about providing different levels of trust. A static system that has a simple loader than performs operations detailed in an offline spec and then disables itself, is clearly easier to reason about than a complicated stay resident object/resource manager that stays alive forever with effective ownership and control of every component it loads. CAmkES (https://wiki.sel4.systems/CAmkES) is the system we use for such static component systems, and allows you to creates as fine or coarse a component as you want. Currently we do not yet have many well established interfaces for devices/drivers/etc so the granularity level is not something we have come up with a standard for yet and are still determining on a system by system basis. rumprun (https://github.com/SEL4PROJ/rumprun-sel4-demoapps) is (currently a not very componentised way) of building semi dynamic systems that are happy with a unikernel to provide them with a pile of services. Services in rumprun are less trusted (due to the large amount of code in a single address space), but provide a nice set of services with a posix interface. The typical use case here is to have a rumprun application that is not very trusted, and then have some other applications running in different address spaces. Due to necessity we have also built pieces of a library OS, which is what you see used in sel4test (https://github.com/seL4/sel4test-manifest) and this is a bit of a wild west that just provides you with helpers to do anything without limiting the 'general purposeness' of the microkernel. These are not exclusive choices though. Both library OS and rumprun systems can just be components inside a CAmkES systems. The CAmkES VM (https://github.com/seL4/camkes-vm-manifest) is a system that has a 'dynamic' component in it to run a Linux VM, that is then connected to a set of static componentised drivers and services on CAmkES. Hope I answered what you were trying to ask somewhere in here, but as you can see currently it is hard to say what is 'typical' and there is a large valid design space to choose from. Hopefully the examples I linked provide some more concrete explanation, and we are still working on providing better examples and skeletons to build from, but this takes time. Adrian On Tue 26-Sep-2017 10:51 AM, Raymond Jennings wrote:
So, I know that at a basic level, a block device driver would probably need I/O permissions, and I'm guessing that it would be handling requests from a file system driver.
Is that basically how the seL4 software ecosystem is laid out? What's typical for how "software in the wild" is actually organized and layered on top of the microkernel?
I only know about seL4 from a theoretical standpoint, read the manual and stuff, and mostly familiar with the actual kernel, but I'm a complete noob when it comes to actual software.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
One piece to add to Adrian’s excellent summary: If you are after a fully dynamic system, then the best environment right now is Genode (https://genode.org). It’s a very general and reasonably mature system that gives you a complete OS environment. The drawback is that there is no assurance story for Genode (and none likely to happen in the foreseeable future), while CAmkES has (at least partial) proofs of correctness of glue code and system initialisation. Gernot On 26 Sep 2017, at 11:59, Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au wrote: Hi Raymond, seL4 is a general purpose microkernel, which means that it supports any architecture you wish to put on top of it. These architectures can vary on many axis of dynamism, componentisation etc. The 'typical' architecture therefore is hard to pin down, as it depends upon how you want to leverage the benefits of seL4 in your system, but there are some common points in the design space. Splitting a piece of software into several components, that run in their own isolated address spaces, is one of the core designs seen on any microkernel. How fine you make your components depends upon what kinds of isolation you want and where you are placing trust. It is valid, for example, to place a disk driver in the same component as the file system driver, but it is also valid for them to be in different components. Systems can have varying levels of dynamism, which is really about providing different levels of trust. A static system that has a simple loader than performs operations detailed in an offline spec and then disables itself, is clearly easier to reason about than a complicated stay resident object/resource manager that stays alive forever with effective ownership and control of every component it loads. CAmkES (https://wiki.sel4.systems/CAmkES) is the system we use for such static component systems, and allows you to creates as fine or coarse a component as you want. Currently we do not yet have many well established interfaces for devices/drivers/etc so the granularity level is not something we have come up with a standard for yet and are still determining on a system by system basis. rumprun (https://github.com/SEL4PROJ/rumprun-sel4-demoapps) is (currently a not very componentised way) of building semi dynamic systems that are happy with a unikernel to provide them with a pile of services. Services in rumprun are less trusted (due to the large amount of code in a single address space), but provide a nice set of services with a posix interface. The typical use case here is to have a rumprun application that is not very trusted, and then have some other applications running in different address spaces. Due to necessity we have also built pieces of a library OS, which is what you see used in sel4test (https://github.com/seL4/sel4test-manifest) and this is a bit of a wild west that just provides you with helpers to do anything without limiting the 'general purposeness' of the microkernel. These are not exclusive choices though. Both library OS and rumprun systems can just be components inside a CAmkES systems. The CAmkES VM (https://github.com/seL4/camkes-vm-manifest) is a system that has a 'dynamic' component in it to run a Linux VM, that is then connected to a set of static componentised drivers and services on CAmkES. Hope I answered what you were trying to ask somewhere in here, but as you can see currently it is hard to say what is 'typical' and there is a large valid design space to choose from. Hopefully the examples I linked provide some more concrete explanation, and we are still working on providing better examples and skeletons to build from, but this takes time. Adrian On Tue 26-Sep-2017 10:51 AM, Raymond Jennings wrote: So, I know that at a basic level, a block device driver would probably need I/O permissions, and I'm guessing that it would be handling requests from a file system driver. Is that basically how the seL4 software ecosystem is laid out? What's typical for how "software in the wild" is actually organized and layered on top of the microkernel? I only know about seL4 from a theoretical standpoint, read the manual and stuff, and mostly familiar with the actual kernel, but I'm a complete noob when it comes to actual software. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
participants (3)
-
Adrian.Danis＠data61.csiro.au -
Gernot.Heiser＠data61.csiro.au -
Raymond Jennings