1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11\chapter{\label{ch:cspace}Capability Spaces} 12 13Recall from \autoref{sec:cap-access-control} that seL4 implements a 14capability-based access control model. Each userspace thread has an 15associated \emph{capability space} (CSpace) that contains the 16capabilities that the thread possesses, thereby governing which 17resources the thread can access. 18 19Recall that capabilities reside within kernel-managed objects known as 20\obj{CNode}s. A \obj{CNode} is a table of slots, each of which may 21contain a capability. This may include capabilities to further 22\obj{CNode}s, forming a directed graph. Conceptually a thread's CSpace 23is the portion of the directed graph that is reachable starting with 24the \obj{CNode} capability that is its CSpace root. 25 26A CSpace address refers to an individual slot (in 27some \obj{CNode} in the CSpace), which may or may not contain a 28capability. Threads refer to capabilities in their CSpaces (e.g. when 29making system calls) using the address of the slot that holds the 30capability in question. An address in a CSpace is the concatenation 31of the indices of the \obj{CNode} capabilities forming the path to the 32destination slot; we discuss this further in 33\autoref{s:cspace-addressing}. 34 35% FIXME The references to mint in the following paragraph and previously in 36% this section need to be cleaned up. They were clearly written at a time when 37% it was not possible to change a capability's rights during a CNode_Copy. 38Recall that capabilities can be copied and moved within CSpaces, and 39also sent in messages (message sending will be described in detail in 40\autoref{sec:cap-transfer}). Furthermore, new capabilities can be 41\emph{minted} from old ones with a subset of their rights. Recall, 42from \autoref{s:memRevoke}, that seL4 maintains a \emph{capability 43 derivation tree} (CDT) in which it tracks the relationship between 44these copied capabilities and the originals. The revoke method 45removes all capabilities (in all CSpaces) that were derived from a 46selected capability. This mechanism can be used by servers to restore 47sole authority to an object they have made available to clients, or by 48managers of untyped memory to destroy the objects in that memory so it 49can be retyped. 50 51seL4 requires the programmer to manage all in-kernel data structures, 52including CSpaces, from userspace. This means that the userspace 53programmer is responsible for constructing CSpaces as well as 54addressing capabilities within them. This chapter first discusses 55capability and CSpace management, before discussing how capabilities 56are addressed within CSpaces, i.e. how applications can refer to 57individual capabilities within their CSpaces when invoking methods. 58 59\section{Capability and CSpace Management} 60 61\subsection{CSpace Creation} 62 63CSpaces are created by creating and manipulating \obj{CNode} objects. 64When creating a \obj{CNode} the user must specify the number of slots 65that it will have, and this determines the amount of memory that it 66will use. Each slot requires 16 bytes of physical memory and has the 67capacity to hold exactly one capability. Like any other object, a 68\obj{CNode} must be created by calling 69\apifunc{seL4\_Untyped\_Retype}{untyped_retype} on an appropriate 70amount of untyped memory (see \autoref{sec:object_sizes}). The caller 71must therefore have a capability to enough untyped memory as well as 72enough free capability slots available in existing \obj{CNode}s for 73the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} invocation to 74succeed. 75 76\subsection{CNode Methods} 77\label{sec:cnode-ops} 78 79Capabilities are managed largely through invoking \obj{CNode} methods. 80 81\obj{CNodes} support the following methods: 82\begin{description} 83\item[\apifunc{seL4\_CNode\_Mint}{cnode_mint}] creates a new 84 capability in a specified \obj{CNode} slot from an existing 85 capability. The newly created capability may have fewer rights than 86 the original and a different guard (see 87 \autoref{sec:cap_address_lookup}). \apifunc{seL4\_CNode\_Mint}{cnode_mint} 88 can also create a badged capability (see \autoref{sec:ep-badges}) 89 from an unbadged one. 90\item[\apifunc{seL4\_CNode\_Copy}{cnode_copy}] is similar to 91 \apifunc{seL4\_CNode\_Mint}{cnode_mint}, but the newly created 92 capability has the same badge and guard as the original. 93\item[\apifunc{seL4\_CNode\_Move}{cnode_move}] moves a capability 94 between two specified capability slots. You cannot move a capability 95 to the slot in which it is currently. 96\item[\apifunc{seL4\_CNode\_Mutate}{cnode_mutate}] can move a 97 capability similarly to \apifunc{seL4\_CNode\_Move}{cnode_move} and 98 also reduce its rights similarly to 99 \apifunc{seL4\_CNode\_Mint}{cnode_mint}, although without an 100 original copy remaining. 101\item[\apifunc{seL4\_CNode\_Rotate}{cnode_rotate}] moves two 102 capabilities between three specified capability slots. It is 103 essentially two \apifunc{seL4\_CNode\_Move}{cnode_move} invocations: 104 one from the second specified slot to the first, and one from the 105 third to the second. The first and third specified slots may be the 106 same, in which case the capability in it is swapped with the 107 capability in the second slot. The method is atomic; either both or 108 neither capabilities are moved. 109\item[\apifunc{seL4\_CNode\_Delete}{cnode_delete}] removes a 110 capability from the specified slot. 111\item[\apifunc{seL4\_CNode\_Revoke}{cnode_revoke}] is equivalent to 112 calling \apifunc{seL4\_CNode\_Delete}{cnode_delete} on each derived 113 child of the specified capability. It has no effect on the 114 capability itself, except in very specific circumstances outlined 115 in Section~\ref{s:cspace-revoke}. 116\item[\apifunc{seL4\_CNode\_SaveCaller}{cnode_savecaller}] moves a 117 kernel-generated reply capability of the current thread from the 118 special \obj{TCB} slot it was created in, into the designated CSpace 119 slot. 120\item[\apifunc{seL4\_CNode\_CancelBadgedSends}{cnode_cancelbadgedsends}] cancels 121 any outstanding sends that use the same badge and object as the 122 specified capability. 123\end{description} 124 125\subsection{Capabilities to Newly-Retyped Objects} 126\label{sec:caps_to_new_objects} 127 128When retyping untyped memory into objects with 129\apifunc{seL4\_Untyped\_Retype}{untyped_retype}, capabilities to the 130newly-retyped objects are placed in consecutive slots in a 131\obj{CNode} specified by its \texttt{root}, \texttt{node\_index}, and 132\texttt{node\_depth} arguments. The \texttt{node\_offset} argument specifies the 133index into the \obj{CNode} at which the first capability will be placed. 134The \texttt{num\_objects} argument specifies the number of capabilities (and, hence, objects) 135to create. All slots must be empty or an error will result. All resulting 136capabilities will be placed in the same \obj{CNode}. 137 138\subsection{Capability Rights} 139\label{sec:cap_rights} 140 141As mentioned previously, some capability types have \emph{access 142 rights} associated with them. Currently, access rights are 143associated with capabilities for \obj{Endpoint}s (see 144\autoref{ch:ipc}), \obj{Notification}s (see 145\autoref{ch:notifications}) and \obj{Page}s (see \autoref{ch:vspace}). The 146access rights associated with a capability determine the methods that 147can be invoked. seL4 supports three orthogonal access rights, which 148are Read, Write and Grant. The meaning of each right is interpreted 149relative to the various object types, as detailed 150in~\autoref{tab:rights}. 151 152When an object is first created, the initial capability that refers to 153it carries the maximum set of access rights. Other, less-powerful 154capabilities may be manufactured from this original capability, using 155methods such as \apifunc{seL4\_CNode\_Mint}{cnode_mint} and 156\apifunc{seL4\_CNode\_Mutate}{cnode_mutate}. If a greater set of 157rights than the source capability is specified for the destination 158capability in either of these invocations, the destination rights are 159silently downgraded to those of the source. 160 161\begin{table}[htb] 162 \begin{tabularx}{\textwidth}{p{0.15\textwidth}XXX} 163 \toprule 164 Type & Read & Write & Grant \\ 165 \midrule 166 \obj{Endpoint} & Required to receive. & Required to send. & Required to send capabilities (including reply capabilities).\\ 167 \obj{Notification} & Required to wait. & Required to signal. & N/A \\ 168 \obj{Page} & Required to map the page readable. & Required to map the page writable. & N/A \\ 169 \bottomrule 170 \end{tabularx} 171 \caption{\label{tab:rights}seL4 access rights.} 172\end{table} 173 174\subsection{Capability Derivation Tree} 175\label{sec:cap_derivation} 176 177As mentioned in \autoref{s:memRevoke}, seL4 keeps track of capability 178derivations in a capability derivation tree. 179 180Various methods, such as \apifunc{seL4\_CNode\_Copy}{cnode_copy} or 181\apifunc{seL4\_CNode\_Mint}{cnode_mint}, may be used to create derived 182capabilities. Not all capabilities support derivation. In general, 183only \emph{original} capabilities support derivation invocations, but 184there are exceptions. \autoref{tab:cap-derivation} summarises the 185conditions that must be met for capability derivation to succeed for 186the various capability types, and how capability-derivation failures 187are reported in each case. The capability types not listed can be 188derived once. 189 190\begin{table}[htb] 191 \begin{tabularx}{\textwidth}{p{0.25\textwidth}XX} 192 \toprule 193 Cap Type & Conditions for Derivation & Error Code on Derivation Failure \\ 194 \midrule 195 \obj{ReplyCap} & Cannot be derived & Dependent on syscall \\ 196 \obj{IRQControl} & Cannot be derived & Dependent on syscall \\ 197 \obj{Untyped} & Must not have children (\autoref{s:cspace-revoke}) & \enummem{seL4\_RevokeFirst} \\ 198 \obj{Page Table} & Must be mapped & \enummem{seL4\_IllegalOperation} \\ 199 \obj{Page Directory} & Must be mapped & \enummem{seL4\_IllegalOperation}\\ 200 \ifxeightsix 201 \obj{IO Page Table (IA-32 only)} & Must be mapped & \enummem{seL4\_IllegalOperation}\\ 202 \fi \bottomrule 203 \end{tabularx} 204 \caption{Capability derivation.\label{tab:cap-derivation}} 205\end{table} 206 207\begin{figure}[th] 208 \begin{center} 209 \includegraphics[width=0.8\textwidth]{figs/CDT} 210 \end{center} 211 \caption{Example capability derivation tree.}\label{fig:CDT} 212\end{figure} 213 214\autoref{fig:CDT} shows an example capability derivation tree that 215illustrates a standard scenario: the top level is a large untyped 216capability, the second level splits this capability into two regions 217covered by their own untyped caps, both are children of the first 218level. The third level on the left is a copy of the level 2 untyped 219capability. Untyped capabilities when copied always create children, 220never siblings. In this scenario, the untyped capability was typed 221into two separate objects, creating two capabilities on level 4, both 222are the original capability to the respective object, both are 223children of the untyped capability they were created from. 224 225Ordinary original capabilities can have one level of derived 226capabilities. Further copies of these derived capabilities will 227create siblings, in this case remaining on level 5. There is an 228exception to this scheme for \obj{Endpoint} and \obj{Notification} capabilities --- they support an 229additional layer of depth though \emph{badging}. 230The original \obj{Endpoint} or \emph{Notification} capability will be unbadged. Using 231the mint method, a copy of the capability with a specific \emph{badge} can be 232created (see \autoref{s:ep-badge}, \autoref{s:notif-badge}). This new, badged capability to the same object is treated as 233an original capability (the ``original badged endpoint capability'') 234and supports one level of derived children like other capabilities. 235 236 237\section{Deletion and Revocation} 238\label{s:cspace-revoke} 239 240Capabilities in seL4 can be deleted and revoked. Both methods 241primarily affect capabilities, but they can have side effects on 242objects in the system where the deletion or revocation results in the 243destruction of the last capability to an object. 244 245As described above, \apifunc{seL4\_CNode\_Delete}{cnode_delete} will 246remove a capability from the specified CNode slot. Usually, this is 247all that happens. If, however, it was the last typed capability to an 248object, this object will now be destroyed by the kernel, cleaning up 249all remaining in-kernel references and preparing the memory for 250re-use. 251 252If the object to be destroyed was a capability container, i.e.\ a TCB 253or CNode, the destruction process will delete each capability held in 254the container, prior to destroying the container. This may result in 255the destruction of further objects if the contained capabilities are 256the last capabilities.\footnote{The recursion is limited as if the last 257capability to a CNode is found within the container, the found CNode 258is not destroyed. Instead, the found CNode is made unreachable by 259moving the capability pointing to the found CNode into the found cnode 260itself, by swapping the capability with the first capability in the 261found cnode, and then trying to delete the swapped capability 262instead. This breaks the recursion. 263 264The result of this approach is that deleting the last cap to the root 265CNode of a CSpace does not recursively delete the entire 266CSpace. Instead, it deletes the root CNode, and the branches of the 267tree become unreachable, potentially including the deleting of some of 268the unreachable CNode's caps to make space for the self-referring 269capability. The practical consequence of this approach is that CSpace 270deletion requires user-level to delete the tree leaf first if 271unreachable CNodes are to be avoided. Alternatively, any resulting 272unreachable CNodes can be cleaned up via revoking a covering untyped 273capability, however this latter approach may be more complex to 274arrange by construction at user-level.} 275 276The \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} method will 277\apifunc{seL4\_CNode\_Delete}{cnode_delete} all CDT children of the 278specified capability, but will leave the capability itself intact. If 279any of the revoked child capabilities were the last capabilities to an 280object, the appropriate destroy operation is triggered. 281 282Note: \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} may only partially 283complete in two specific circumstances. The first being where a 284CNode containing the last capability to the TCB of the thread 285performing the revoke (or the last capability to the TCB itself) is 286deleted as a result of the revoke. In this case the thread performing 287the revoke is destroyed during the revoke and the revoke does not 288complete. The second circumstance is where the storage containing the 289capability that is the target of the revoke is deleted as a result of 290the revoke. In this case, the authority to perform the revoke is 291removed during the operation and the operation stops part way 292through. Both these scenarios can be and should be avoided at 293user-level by construction. 294 295Note that for page tables and page directories 296\apifunc{seL4\_CNode\_Revoke}{cnode_revoke} will not revoke frame 297capabilities mapped into the address space. They will only be 298unmapped from the space. 299 300 301\section{CSpace Addressing} 302\label{s:cspace-addressing} 303 304When performing a system call, a thread specifies to the kernel the 305capability to be invoked by giving an address in its CSpace. This 306address refers to the specific slot in the caller's CSpace that 307contains the capability to be invoked. 308 309CSpaces are designed to permit sparsity, and the process of looking-up 310a capability address must be efficient. Therefore, CSpaces are 311implemented as \emph{guarded page tables}. 312% FIXME: need a references to justify the above decision 313 314As explained earlier, a CSpace is a directed graph of \obj{CNode} 315objects, and each \obj{CNode} is a table of slots, where each slot can 316either be empty, or contain a capability, which may refer to another \obj{CNode}. 317Recall from \autoref{s:sel4_internals} that the number of slots in a \obj{CNode} 318must be a power of two. A \obj{CNode} is said to have a \emph{radix}, which is 319the power to which two is raised in its size. That is, if a \obj{CNode} has 320$2^k$ slots, its radix would be $k$. 321The kernel stores a capability to the root \obj{CNode} of each thread's 322CSpace in the thread's TCB. Conceptually, a \obj{CNode} capability 323stores not only a reference to the \obj{CNode} to which it refers, but 324also carries a \emph{guard} value, explained in 325\autoref{sec:cap_address_lookup}. 326 327\subsection{Capability Address Lookup} 328\label{sec:cap_address_lookup} 329Like a virtual memory address, a capability address is simply an 330integer. Rather than referring to a location of physical memory (as 331does a virtual memory address), a capability address refers to a 332capability slot. When looking up a capability address presented by a 333userspace thread, the kernel first consults the \obj{CNode} capability 334in the thread's TCB that defines the root of the thread's CSpace. It 335then compares that \obj{CNode}'s \emph{guard} value against the most 336significant bits of the capability address. If the two values are 337different, lookup fails. Otherwise, the kernel then uses the next 338most-significant \emph{radix} bits of the capability address as an 339index into the \obj{CNode} to which the \obj{CNode} capability 340refers. The slot~$s$ identified by these next \emph{radix} bits might 341contain another \obj{CNode} capability or contain something else 342(including nothing). If $s$ contains a \obj{CNode} capability~$c$ and 343there are remaining bits (following the \emph{radix} bits) in the 344capability address that have yet to be translated, the lookup process 345repeats, starting from the \obj{CNode} capability~$c$ and using these 346remaining bits of the capability address. Otherwise, the lookup 347process terminates successfully; the capability address in question 348refers to the capability slot~$s$. 349 350\begin{figure}[tb] 351 \begin{center} 352 \includegraphics[scale=0.5]{figs/fig1-4.pdf} 353 \caption{An example CSpace demonstrating object references at 354 all levels, various guard and radix sizes and internal CNode 355 references.} 356 \label{fig1.4} 357 \end{center} 358\end{figure} 359 360Figure \ref{fig1.4} demonstrates a valid CSpace with the following 361features: 362\begin{itemize} 363\item a top level CNode object with a 12-bit guard set to 0x000 and 364 256 slots; 365\item a top level CNode with direct object references; 366\item a top level CNode with two second-level CNode references; 367\item second level CNodes with different guards and slot counts; 368\item a second level CNode that contains a reference to a top level 369 CNode; 370\item a second level CNode that contains a reference to another CNode 371 where there are some bits remaining to be translated; 372\item a second level CNode that contains a reference to another CNode 373 where there are no bits remaining to be translated; and 374\item object references in the second level CNodes. 375\end{itemize} 376 377It should be noted that \autoref{fig1.4} demonstrates only what is 378possible, not what is usually practical. Although the CSpace is legal, 379it would be reasonably difficult to work with due to the small number 380of slots and the circular references within it. 381 382 383\subsection{Addressing Capabilities} 384\label{sec:cap_addressing} 385 386A capability address is stored in a CPointer (abbreviated CPTR), which 387is an unsigned integer variable. Capabilities are addressed in 388accordance with the translation algorithm described above. Two 389special cases involve addressing \obj{CNode} capabilities themselves 390and addressing a range of capability slots. 391 392Recall that the translation algorithm described above will traverse 393\obj{CNode} capabilities while there are address bits remaining to be 394translated. Therefore, in order to address a \obj{CNode} capability, 395the user must supply not only a capability address but also specify 396the maximum number of bits of the capability address that are to be 397translated, called the \emph{depth limit}. 398 399Certain methods, such as 400\apifunc{seL4\_Untyped\_Retype}{untyped_retype}, require the user to 401provide a range of capability slots. This is done by providing a base 402capability address, which refers to the first slot in the range, 403together with a window size parameter, specifying the number of slots 404(with consecutive addresses, following the base slot) in the range. 405 406 407\autoref{fig2.1} depicts an example CSpace. In order to illustrate 408these ideas, we determine the address of each of the 10 capabilities 409in this CSpace. 410 411\begin{figure}[tb] 412 \begin{center} 413 \includegraphics[scale=0.5]{figs/fig2-1.pdf} 414 \caption{An arbitrary CSpace layout.} 415 \label{fig2.1} 416 \end{center} 417\end{figure} 418 419 420\begin{description} 421\item[Cap A.] The first CNode has a 4-bit guard set to 0x0, and an 422 8-bit radix. Cap A resides in slot 0x60 so it may be referred to by 423 any address of the form 0x060xxxxx (where xxxxx is any number, 424 because the translation process terminates after translating the 425 first 12 bits of the address). For simplicity, we usually adopt the 426 address 0x06000000. 427 428\item[Cap B.] Again, the first CNode has a 4-bit guard set to 0x0, and 429 an 8-bit radix. The second CNode is reached via the L2 CNode Cap. 430 It also has a 4-bit guard of 0x0 and Cap B resides at index 431 0x60. Hence, Cap B's address is 0x00F06000. Translation of this 432 address terminates after the first 24 bits. 433 434\item[Cap C.] This capability is addressed via both CNodes. The third 435 CNode is reached via the L3 CNode Cap, which resides at index 0x00 436 of the second CNode. The third CNode has no guard and Cap C is at 437 index 0x60. Hence, its address is 0x00F00060. Translation of this 438 address leaves 0 bits untranslated. 439 440\item[Caps C--G.] This range of capability slots is addressed by 441 providing a base address (which refers to the slot containing Cap C) 442 of 0x00F00060 and a window size of 5. 443 444\item[L2 CNode Cap.] Recall that to address a \obj{CNode} capability, 445 the user must supply not only a capability address but also specify 446 the depth limit, which is the maximum number of bits to be 447 translated. L2 CNode Cap resides at offset 0x0F of the first CNode, 448 which has a 4-bit guard of 0x0. Hence, its address is 0x00F00000, 449 with a depth limit of 12 bits. 450 451\item[L3 CNode Cap.] This capability resides at index 0x00 of the 452 second CNode, which is reached by the L2 CNode Cap. The second CNode 453 has a 4-bit guard of 0x0. Hence, the capability's address is 454 0x00F00000 with a depth limit of 24 bits. Note that the addresses of 455 the L2 and L3 CNode Caps are the same, but that their depth limits 456 are different. 457\end{description} 458 459In summary, to refer to any capability (or slot) in a CSpace, the user 460must supply its address. When the capability might be a CNode, the 461user must also supply a depth limit. To specify a range of capability 462slots, the user supplies a starting address and a window size. 463 464\section{Lookup Failure Description} 465\label{sec:lookup_fail_desc} 466 467When a capability lookup fails, a description of the failure is given 468to either the calling thread or the thread's exception handler in its 469IPC buffer. The format of the description is always the same but may 470occur at varying offsets in the IPC buffer depending on how the error 471occurred. The description format is explained below. The first word 472indicates the type of lookup failure and the meaning of later words 473depend on this. 474 475\subsection{Invalid Root} 476 477A CSpace CPTR root (within which a capability was to be looked up) 478is invalid. For example, the capability is not a \obj{CNode} cap.\\ \\ 479 480\begin{tabularx}{\textwidth}{XX} 481 \toprule 482 Data & Meaning \\ 483 \midrule 484 \ipcbloc{Offset + 0} & \enummem{seL4\_InvalidRoot} \\ 485 \bottomrule 486\end{tabularx} 487 488\subsection{Missing Capability} 489 490A capability required for an invocation is not present or does not 491have sufficient rights. \\ \\ 492 493\begin{tabularx}{\textwidth}{XX} 494 \toprule 495 Data & Meaning \\ 496 \midrule 497 \ipcbloc{Offset + 0} & \enummem{seL4\_MissingCapability} \\ 498 \ipcbloc{Offset + seL4\_CapFault\_BitsLeft} & Bits left \\ 499 \bottomrule 500\end{tabularx} 501 502\subsection{Depth Mismatch} 503 504When resolving a capability, a CNode was traversed that resolved more 505bits than was left to decode in the CPTR or a non-CNode capability was 506encountered while there were still bits remaining to be looked up. \\ \\ 507 508\begin{tabularx}{\textwidth}{XX} 509 \toprule 510 Data & Meaning \\ 511 \midrule 512 \ipcbloc{Offset + 0} & \enummem{seL4\_DepthMismatch} \\ 513 \ipcbloc{Offset + seL4\_CapFault\_BitsLeft} & Bits of CPTR remaining to decode \\ 514 \ipcbloc{Offset + seL4\_CapFault\_DepthMismatch\_BitsFound} & Bits that the current CNode being traversed resolved \\ 515 \bottomrule 516\end{tabularx} 517 518\subsection{Guard Mismatch} 519 520When resolving a capability, a CNode was traversed with a guard size 521larger than the number of bits remaining or the CNode's guard did not 522match the next bits of the CPTR being resolved. \\ \\ 523 524\begin{tabularx}{\textwidth}{XX} 525 \toprule 526 Data & Meaning \\ 527 \midrule 528 \ipcbloc{Offset + 0} & \enummem{seL4\_GuardMismatch} \\ 529 \ipcbloc{Offset + seL4\_CapFault\_BitsLeft} & Bits of CPTR remaining to decode \\ 530 \ipcbloc{Offset + seL4\_CapFault\_GuardMismatch\_GuardFound} & The CNode's guard \\ 531 \ipcbloc{Offset + seL4\_CapFault\_GuardMismatch\_BitsFound} & The CNode's guard size \\ 532 \bottomrule 533\end{tabularx} 534 535 536