Hello everyone, I’m a new guy about seL4, and I’m reading the seL4 tutorial about the capability things.There is a sentence here that I don’t quite understand: In seL4, capabilities to all resources controlled by the kernel are given to the root task on initialisation. My question is:
Is the root task kernel task or user task?
If it is a user task, the user task has all capability about kernel object, wouldn’t that be very dangerous for whole system?
Can someone answer my doubts? Thank you very much.
Disclaimer: I’m also new to seL4, I might get something wrong…
It is a user-level task, there are no kernel tasks in seL4. seL4 does not do anything at the kernel level it does not absolutely have to - it multiplexes the hardware and provides multiplexing of the CPU while enforcing security policy - that’s pretty much it. There are recordings of Gernot Heiser’s Advanced Operating Systems course, you can find those here: https://www.youtube.com/watch?v=IvqM2pmApSY&list=PLtoQeavghzr3nlXyJEXaTLU9Ca0DXWMnt&t=630s
The root task is a similar basic idea (but quite different in implementation) to an init system: an init system starts all the services making up e.g. a Linux system (and uses Linux-y security mechanisms like running them as different users for security), the root task loads and gives only the necessary capabilities to the tasks making up an seL4-based system. In both cases they have pretty much complete power over the system - but for setup and delegating permissions (capabilities in seL4) that’s necessary.
Some details on the capability concept.
When a thread requests an object from capability-based system, it receives not the requested object itself, but corresponding capability (specifically, its index in a capability list).
It means the thread accesses key system resources only through interfaces provided by the capabilities. So, Init Thread has “full permission” on the capabilities, where “full permission” means the whole scope of operations provided by the capability interface.
Next, this is the difference of microkernel: its responsibility is IPC, virtual memory, threads. Everything else functions in user space. How functionally safe the whole system is depends on the design of the stack “above” microkernel. Microkernel guarantees “safety” of the three items mentioned above. So, Init Thread receives all the capabilities to manage available resources according to the system tasks.
To also leave the response here in text so people can find it in the future: yes, the root task is inherently a trusted component of the system, because it has authority to everything.
It is possible to generate (and for many configurations also formally verify) this root task so that it sets up systems that then have less authority, for example where there is then a static number of components with pre-defined communication endpoints. All of this can be described declaratively in a language called capDL that describes capability distributions in an seL4-based system. The resulting system can be as static or dynamic as needed, depending on how much authority you delegate to each component (for static setups authority is clearer is and easier to reason about).
The default root task that does this is the so-called capDL loader, which comes in an unverified C version and a verified cakeML version (has less features and is currently still harder to use, but it exists and works).
The idea is that the authority distribution is completely up to user-level and to the kind of system one would like to build.
