[seL4] How are capabilities assigned

Gerwin Klein Gerwin.Klein at nicta.com.au
Mon Feb 16 18:24:47 EST 2015


Hi Sebastian,

when the kernel initialises, it creates a number of standard predefined capabilities and hands them to the initial thread (root task), including capabilities to the device regions in the machine, and Untyped capabilities to free memory. The initial task can then use these to set up the rest of the system (creating threads, page tables, IPC endpoints, loading executables, etc).

There is a separate tool (capDL-loader) that takes a static description of the capability distribution the initial thread should achieve and produces an initial thread for you that sets up the system accordingly. There is no requirement to use this tool, but it has been quite handy for us so far.

IPC is managed by kernel calls (Wait, Send, Call, Reply) that have an endpoint capability as argument.

Cheers,
Gerwin

On 16.02.2015, at 17:54, Sebastian Lau <sebastianlau25 at gmail.com<mailto:sebastianlau25 at gmail.com>> wrote:


I have a question, how are capabilities assigned or given to processes? Is it through the kernel or can the root process (like init etc.) assign capabilities as well? Also is IPC managed by calls to the kernel? I have in mind to base something off of seL4 in the future but I'm not quite ready to start though and just want to get an understanding of how things work.

_______________________________________________
Devel mailing list
Devel at sel4.systems<mailto:Devel at sel4.systems>
https://sel4.systems/lists/listinfo/devel


________________________________

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://sel4.systems/pipermail/devel/attachments/20150216/0e72fc10/attachment.html>


More information about the Devel mailing list