Lines Matching refs:a
9 Recall from \autoref{sec:cap-access-control} that seL4 implements a
16 \obj{CNode}s. A \obj{CNode} is a table of slots, each of which may
17 contain a capability. This may include capabilities to further
18 \obj{CNode}s, forming a directed graph. Conceptually a thread's CSpace
23 some \obj{CNode} in the CSpace), which may or may not contain a
26 capability in question. An address in a CSpace is the concatenation
32 % this section need to be cleaned up. They were clearly written at a time when
33 % it was not possible to change a capability's rights during a CNode_Copy.
37 \emph{minted} from old ones with a subset of their rights. Recall,
38 from \autoref{s:memRevoke}, that seL4 maintains a \emph{capability
41 removes all capabilities (in all CSpaces) that were derived from a
60 When creating a \obj{CNode} the user must specify the number of slots
65 Like any other object, a \obj{CNode} must be created by calling
68 must therefore have a capability to enough untyped memory as well as
80 \item[\apifunc{seL4\_CNode\_Mint}{cnode_mint}] creates a new
81 capability in a specified \obj{CNode} slot from an existing
83 the original and a different guard (see
85 can also create a badged capability (see \autoref{sec:ep-badges})
90 \item[\apifunc{seL4\_CNode\_Move}{cnode_move}] moves a capability
91 between two specified capability slots. You cannot move a capability
93 \item[\apifunc{seL4\_CNode\_Mutate}{cnode_mutate}] can move a
97 a copy. That is, if the capability is revokable, it remains revokable.
99 be used to adjust the guard of a \obj{CNode} capability. It cannot be
109 \item[\apifunc{seL4\_CNode\_Delete}{cnode_delete}] removes a
116 \item[\apifunc{seL4\_CNode\_SaveCaller}{cnode_savecaller}] moves a
130 newly-retyped objects are placed in consecutive slots in a
147 access rights associated with a capability determine the methods that
150 each other. GrantReply is a less powerful form of Grant e.g. if you already have
159 \apifunc{seL4\_CNode\_Mutate}{cnode_mutate}. If a greater set of
179 \caption{\label{tab:rights}seL4 access rights: What a specific right entitles a
187 derivations in a capability derivation tree.
224 illustrates a standard scenario: the top level is a large untyped
227 level. The third level on the left is a copy of the level 2 untyped
240 the mint method, a copy of the capability with a specific \emph{badge} can be
255 remove a capability from the specified CNode slot. Usually, this is
261 If the object to be destroyed was a capability container, i.e.\ a TCB
266 capability to a CNode is found within the container, the found CNode
274 CNode of a CSpace does not recursively delete the entire
281 unreachable CNodes can be cleaned up via revoking a covering untyped
292 complete in two specific circumstances. The first being where a
295 deleted as a result of the revoke. In this case the thread performing
298 capability that is the target of the revoke is deleted as a result of
313 When performing a system call, a thread specifies to the kernel the
319 a capability address must be efficient. Therefore, CSpaces are
321 % FIXME: need a references to justify the above decision
323 As explained earlier, a CSpace is a directed graph of \obj{CNode}
324 objects, and each \obj{CNode} is a table of slots, where each slot can
325 either be empty, or contain a capability, which may refer to another \obj{CNode}.
326 Recall from \autoref{s:sel4_internals} that the number of slots in a \obj{CNode}
327 must be a power of two. A \obj{CNode} is said to have a \emph{radix}, which is
328 the power to which two is raised in its size. That is, if a \obj{CNode} has
330 The kernel stores a capability to the root \obj{CNode} of each thread's
331 CSpace in the thread's TCB. Conceptually, a \obj{CNode} capability
332 stores not only a reference to the \obj{CNode} to which it refers, but
333 also carries a \emph{guard} value, explained in
338 Like a virtual memory address, a capability address is simply an
339 integer. Rather than referring to a location of physical memory (as
340 does a virtual memory address), a capability address refers to a
341 capability slot. When looking up a capability address presented by a
351 (including nothing). If $s$ contains a \obj{CNode} capability~$c$ and
369 Figure \ref{fig1.4} demonstrates a valid CSpace with the following
372 \item a top level CNode object with a 12-bit guard set to 0x000 and
374 \item a top level CNode with direct object references;
375 \item a top level CNode with two second-level CNode references;
377 \item a second level CNode that contains a reference to a top level
379 \item a second level CNode that contains a reference to another CNode
381 \item a second level CNode that contains a reference to another CNode
395 A capability address is stored in a CPointer (abbreviated CPTR), which
399 and addressing a range of capability slots.
403 translated. Therefore, in order to address a capability which may be
404 a \obj{CNode} capability, the user must supply not only a capability
407 When a CPointer is paired with depth limit \textit{depth}, only its
412 provide a range of capability slots. This is done by providing a base
414 together with a window size parameter, specifying the number of slots
432 \item[Cap A.] The first CNode has a 4-bit guard set to 0x0, and an
434 a \obj{CNode} capability, it may be referred to by any address of
441 \item[Cap B.] Again, the first CNode has a 4-bit guard set to 0x0, and
443 It also has a 4-bit guard of 0x0 and Cap B resides at index
454 providing a base address (which refers to the slot containing Cap C)
455 of 0x00F00060 and a window size of 5.
457 \item[L2 CNode Cap.] Recall that to address a \obj{CNode} capability,
458 the user must supply not only a capability address but also specify
461 which has a 4-bit guard of 0x0. Hence, it may be referred to by any
462 address of the form 0x\textit{nnnnn}00F with a depth limit of 12
467 has a 4-bit guard of 0x0. Hence, the capability may be referred to
468 by any address of the form 0x\textit{nn}00F000 with a depth limit of
472 In summary, to refer to any capability (or slot) in a CSpace, the user
473 must supply its address. When the capability might be a CNode, the
474 user must also supply a depth limit. To specify a range of capability
475 slots, the user supplies a starting address and a window size.
480 When a capability lookup fails, a description of the failure is given
490 A CSpace CPTR root (within which a capability was to be looked up)
491 is invalid. For example, the capability is not a \obj{CNode} cap.\\ \\
517 When resolving a capability, a CNode was traversed that resolved more
518 bits than was left to decode in the CPTR or a non-CNode capability was
533 When resolving a capability, a CNode was traversed with a guard size