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
On 26 Sep 2017, at 11:59,
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.
) 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.
) 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
) 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
) 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.
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 mailing list