1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Documentation file, introduction to the abstract specification. 9*) 10 11chapter "Introduction" 12 13(*<*) 14theory Intro_Doc 15imports Main 16begin 17(*>*) 18text \<open> 19 20The seL4 microkernel is an operating system kernel designed to be a 21secure, safe, and reliable foundation for systems in a wide variety of 22application domains. As a microkernel, seL4 provides a minimal number of 23services to applications. This small number of services directly 24translates to a small implementation of approximately $8700$ lines of C code, 25which has allowed the kernel to be formally proven in the Isabelle/HOL 26theorem prover to adhere to a formal specification. 27 28This document gives the text version of the formal Isabelle/HOL 29specification used in this proof. The document starts by giving a brief 30overview of the seL4 microkernel design, followed by text generated from 31the Isabelle/HOL definitions. 32 33This document is not a user manual to seL4, nor is it intended to 34be read as such. Instead, it is a precise reference to the 35behaviour of the seL4 kernel. 36 37Further information on the models and verification techniques 38can be found in previous publications~\cite{Boyton_09,Cock_08,Cock_KS_08,Derrin_EKCC_06,Elkaduwe_GE_07,Elkaduwe_GE_08,Elphinstone_KDRH_07,Heiser_EKKP_07,Klein_09,Klein_DE_09,Klein_EHACDEEKNSTW_09,Klein_EHACDEEKNSTW_10,Tuch_08,Tuch_09,Tuch_KH_05,Tuch_KN_07,Tuch_Klein_05,Tuch:phd,Winwood_KSACN_09}. 39 40 41\section{The seL4 Microkernel} 42 43The seL4 microkernel is a small operating system kernel of the L4 44family. SeL4 provides a minimal number of services to applications, such 45as abstractions for virtual address spaces, threads, inter-process 46communication (IPC). 47 48SeL4 uses a capability-based access-control model. All memory, devices, 49and microkernel-provided services require an associated 50\emph{capability} (access right) to utilise them 51\cite{Dennis_VanHorn_66}. The set of capabilities an application 52possesses determines what resources that application can directly 53access. SeL4 enforces this access control by using the hardware's memory 54management unit (MMU) to ensure that userspace applications only have 55access to memory they possess capabilities to. 56 57\autoref{fig:sample} shows a representative seL4-based system. It 58depicts the microkernel executing on top of the hardware as the only 59software running in privileged mode of the processor. The first 60application to execute is the supervisor OS. The supervisor OS (also 61termed a \emph{booter} for simple scenarios) is responsible for 62initialising, configuring and delegating authority to the specific 63system layered on top. 64 65\begin{figure}[tb] 66 \centering 67 \includegraphics[width=6cm]{imgs/seL4-background_01} 68 \caption{Sample seL4 based system} 69 \label{fig:sample} 70\end{figure} 71 72In \autoref{fig:sample}, the example system set up by the supervisor consists 73of an instance of Linux on the left, and several instances of trusted or 74sensitive applications on the right. The group of applications on the left and 75the group on the right are unable to directly communicate or interfere with 76each other without explicit involvement of the supervisor (and the 77microkernel) --- a barrier is thus created between the untrusted left and the 78trusted right, as indicated in the figure. The supervisor has a 79kernel-provided mechanism to determine the relationship between applications 80and the presence or absence of any such barriers. 81 82\subsection{Kernel Services} 83\label{s:kernel_services} 84 85A limited number of service primitives are provided by the 86microkernel; more complex services may be implemented as applications 87on top of these primitives. In this way, the functionality of the 88system can be extended without increasing the code and complexity in 89privileged mode, while still supporting a potentially wide number of 90services for varied application domains. 91 92The basic services the microkernel provides are as follows: 93\begin{description} 94\item[Threads] are an abstraction of CPU execution that support running 95 software; 96\item[Address Spaces] are virtual memory spaces that each contain an 97 application. Applications are limited to accessing memory in their 98 address space; 99\item[Interprocess Communication] (IPC) via \emph{endpoints} allows 100threads to communicate using message passing; 101\item[Device Primitives] allow device drivers to be implemented as unprivileged 102 applications. The kernel exports hardware device interrupts 103 via IPC messages; and 104\item[Capability Spaces] store capabilities (i.e., access rights) to kernel services along 105with their book-keeping information. 106\end{description} 107 108All kernel services are accessed using kernel-provided system calls 109that \emph{invoke} a capability; 110the semantics of the system call depends upon the type of the 111capability invoked. For example, invoking the \meth{Call} system call on a 112thread control block (TCB) with certain arguments will suspend the 113target thread, while invoking \meth{Call} on an endpoint will result 114in a message being sent. In general, the message sent to a capability 115will have an entry indicating the desired operation, along with any 116arguments. 117 118The kernel provides to clients the following system calls: 119\begin{description} 120\item[\meth{Send}] delivers the system call arguments to the target object 121and allows the application to continue. If the 122target object is unable to receive and/or process the arguments 123immediately, the sending application will be blocked until the arguments 124can be delivered. 125 126\item[\meth{NBSend}] performs non-blocking send in a similar fashion 127to \meth{Send} except that if the object is unable to receive the 128arguments immediately, the message is silently dropped. 129 130\item[\meth{Call}] is a \meth{Send} that blocks the application until the 131object provides a response, or the receiving application replies. In 132the case of delivery to an application (via an \obj{Endpoint}), an 133additional capability is added to the arguments and delivered to the 134receiver to give it the right to respond to the sender. 135 136\item[\meth{Recv}] is used by an application to block until the target 137object is ready. 138 139\item[\meth{Reply}] is used to respond to a \meth{Call}, using the 140capability generated by the \meth{Call} operation. 141 142\item[\meth{ReplyRecv}] is a combination of \meth{Reply} and 143\meth{Recv}. It exists for efficiency reasons: the common case of 144replying to a request and waiting for the next can be performed in a 145single kernel system call instead of two. 146\end{description} 147 148\subsection{Capability-based Access Control} 149\label{s:sel4_cap_access_control} 150 151 152The seL4 microkernel provides a capability-based access control model. 153Access control governs all kernel services; in order to perform any 154system call, an application must invoke a capability in its possession 155that has sufficient access rights for the requested service. With 156this, the system can be configured to isolate software components from 157each other, and also to enable authorised controlled communication 158between components by selectively granting specific communication 159capabilities. This enables software component isolation with a high 160degree of assurance, as only those operations explicitly authorised by 161capability possession are permitted. 162 163A capability is an unforgeable token that references a specific kernel 164object (such as a thread control block) and carries access 165rights that control what operations may be performed when it is invoked. 166Conceptually, a capability resides in an application's 167\emph{capability space}; an address in this space refers to a 168\emph{slot} which may or may not contain a capability. An application 169may refer to a capability --- to request a kernel service, for example 170--- using the address of the slot holding that capability. The seL4 171capability model is an instance of a \emph{segregated} (or 172\emph{partitioned}) capability 173model, where capabilities are managed by the kernel. 174 175Capability spaces are implemented as a directed graph of kernel-managed 176\emph{capability nodes} (\obj{CNode}s). A \obj{CNode} is a table of 177slots, where each slot may contain further \obj{CNode} capabilities. 178An address in a capability space is then the concatenation of the 179indices of the \obj{CNode} capabilities forming the path to the 180destination slot; we discuss \obj{CNode} objects further in 181\autoref{s:cnode_obj}. 182 183Capabilities can be copied and moved within capability spaces, and 184also sent via IPC. This allows creation of applications with specific 185access rights, the delegation of authority to another application, and 186passing to an application authority to a newly created (or selected) 187kernel service. Furthermore, capabilities can be \emph{minted} to 188create a derived capability with a subset of the rights of the 189original capability (never with more rights). A newly minted 190capability can be used for partial delegation of authority. 191 192Capabilities can also be revoked in their entirety to withdraw 193authority. Revocation includes any capabilities that may have 194been derived from the original capabilities. The propagation of 195capabilities through the system is controlled by a 196\emph{take-grant}-based model~\cite{Elkaduwe_GE_07}. 197 198\subsection{Kernel Objects} 199\label{s:sel4_internals} 200 201In this section we give a brief overview of the kernel implemented 202objects that can be invoked by applications. The interface to these 203objects forms the interface to the kernel itself. The creation and use 204of the high-level kernel services is achieved by the creation, 205manipulation, and combination of these kernel objects. 206 207\subsubsection{\obj{CNodes}} 208\label{s:cnode_obj} 209 210As mentioned in the previous section, capabilities in seL4 are stored 211in kernel objects called \obj{CNodes}. A \obj{CNode} has a fixed 212number of slots, always a power of two, determined when the 213\obj{CNode} is created. Slots can be empty or contain a capability. 214 215\begin{figure}[htb] 216 \centering 217 \includegraphics[height=5cm]{imgs/sel4objects_01.pdf} 218 \caption{\obj{CNodes} forming a \obj{CSpace}} 219 \label{fig:cnode} 220\end{figure} 221 222 223\obj{CNodes} have the following operations: 224\begin{description} 225\item[\meth{Mint}] creates a new capability in a specified \obj{CNode} slot 226from an existing capability. The newly created capability may have fewer rights than the original. 227\item[\meth{Copy}] is similar to \meth{Mint}, but the newly created capability 228 has the same rights as the original. 229\item[\meth{Move}] moves a capability between two specified capability slots. 230\item[\meth{Mutate}] is an atomic combination of \meth{Move} and 231 \meth{Mint}. It is a performance optimisation. 232\item[\meth{Rotate}] moves two capabilities between three specified 233 capability slots. It is essentially two \meth{Move} operations: one 234 from the second specified slot to the first, and one from the third 235 to the second. The first and third specified slots may be the same, 236 in which case the capability in it is swapped with the capability in 237 the second slot. The operation is atomic; either both or neither capabilities 238 are moved. 239\item[\meth{Delete}] removes a capability from the specified slot. 240\item[\meth{Revoke}] is equivalent to calling \meth{Delete} on each 241 derived child of the specified capability. It has no effect on the 242 capability itself. 243\item[\meth{SaveCaller}] moves a kernel-generated reply capability of the 244 current thread from the special \obj{TCB} slot it was created in, into 245 the designated \obj{CSpace} slot. 246\item[\meth{Recycle}] is equivalent to \meth{Revoke}, except that it 247 also resets most aspects of the object to its initial state. 248\end{description} 249 250\subsubsection{IPC Endpoints and Notifications} 251 252The seL4 microkernel supports \emph{synchronous} IPC (\obj{EP}) endpoints, 253used to facilitate 254interprocess communication between threads. Capabilities to endpoints 255can be restricted to be send-only or receive-only. They can also 256specify whether capabilities can be passed through the endpoint. 257 258Endpoints allow both data and capabilities to be 259transferred between threads, depending on the rights on the endpoint 260capability. Sending a message will block the sender until the message 261has been received; similarly, a waiting thread will be blocked until a 262message is available (but see \meth{NBSend} above). 263 264When only notification of an event is required, notification objects can 265be used. These have the following invocations: 266% 267\begin{description} 268\item[\meth{Notify}] simply sets the given set of semaphore bits in the 269notification object. 270Multiple \meth{Notify} system calls without an intervening \meth{Recv} 271result in the bits being ``or-ed'' with any bits already set. As such, 272\meth{Notify} is always non-blocking, and has no indication of whether 273a receiver has received the notification. 274\end{description} 275% 276Additionally, the \meth{Recv} system call may be used with an 277notification object, allowing the calling thread to retrieve all set 278bits from the notification object. By default, if no \meth{Notify} 279operations have taken place since the last \meth{Recv} call, the 280calling thread will block until the next \meth{Notify} takes place. 281There is also a non-blocking (polling) variant of this invocaction. 282 283\subsubsection{\obj{TCB}} 284 285The \emph{thread control block} (\obj{TCB}) object represents a thread 286of execution in seL4. Threads are the unit of execution that is 287scheduled, blocked, unblocked, etc., depending on the applications 288interaction with other threads. 289 290As illustrated in 291\autoref{fig:sel4_internals}, a thread needs both a \obj{CSpace} and a 292\obj{VSpace} in which to execute to form an application (plus some 293additional information not represented here). The \obj{CSpace} 294provides the capabilities (authority) required to manipulated kernel 295objects, in order to send messages to another application for example. The 296\obj{VSpace} provides the virtual memory environment required to 297contain the code and data of the application. A \obj{CSpace} is 298associated with a thread by installing a capability to the root 299\obj{CNode} of a \obj{CSpace} into the \obj{TCB}. Likewise, a 300\obj{VSpace} is associated with a thread by installing a capability to 301a \obj{Page Directory} (described shortly) into the \obj{TCB}. Note that multiple threads 302can share the same \obj{CSpace} and \obj{VSpace}. 303 304\begin{figure}[htb] 305 \centering 306 \includegraphics[width=0.8\textwidth]{imgs/sel4_internals_01} 307 \caption{Internal representation of an application in seL4} 308 \label{fig:sel4_internals} 309\end{figure} 310 311The TCB object has the following methods: 312 313\begin{description} 314\item[\meth{CopyRegisters}] is used for copying the state of a 315 thread. The method is given an additional capability argument, which 316 must refer to a \obj{TCB} that will be used as the source of the 317 transfer; the invoked thread is the destination. The caller may 318 select which of several subsets of the register context will be 319 transferred between the threads. The operation may also suspend the 320 source thread, and resume the destination thread. 321 322 Two subsets of the context that might be copied (if indicated by the 323 caller) include: firstly, the parts of the register state that are used or preserved 324 by system calls, including the instruction and stack pointers, and 325 the argument and message registers; and secondly, the 326 remaining integer registers. Other subsets are architecture-defined, 327 and typically include coprocessor registers such as the floating 328 point registers. Note that many integer registers are modified or 329 destroyed by system calls, so it is not generally useful to use 330 \meth{CopyRegisters} to copy integer registers to or from the 331 current thread. 332\item[\meth{ReadRegisters}] is a variant of \meth{CopyRegisters} for 333 which the destination is the calling thread. It uses the message 334 registers to transfer the two subsets of the integer registers; the 335 message format has the more commonly transferred instruction 336 pointer, stack pointer and argument registers at the start, and will 337 be truncated at the caller's request if the other registers are not 338 required. 339\item[\meth{WriteRegisters}] is a variant of \meth{CopyRegisters} for 340 which the source is the calling thread. It uses the message 341 registers to transfer the integer registers, in the same order used 342 by \meth{ReadRegisters}. It may be truncated if the later registers 343 are not required; an explicit length argument is given to allow 344 error detection when the message is inadvertently truncated by a 345 missing IPC buffer. 346\item[\meth{SetPriority}] configures the thread's scheduling 347 parameters. In the current version of seL4, this is simply a 348 priority for the round-robin scheduler. 349\item[\meth{SetIPCBuffer}] configures the thread's local storage, 350 particularly the IPC buffer used for sending parts of the message 351 payload that don't fit in hardware registers. 352\item[\meth{SetSpace}] configures the thread's virtual memory and 353 capability address spaces. It sets the roots of the trees (or other 354 architecture-specific page table structures) that represent the two 355 address spaces, and also nominates the \obj{Endpoint} that the kernel uses 356 to notify the thread's pager\footnote{A \emph{pager} is a term for a 357 thread that manages the \obj{VSpace} of another application. For 358 example, Linux would be called the pager of its applications.} of 359 faults and exceptions. 360\item[\meth{Configure}] is a batched version of the three 361 configuration system calls: \meth{SetPriority}, \meth{SetIPCBuffer}, 362 and \meth{SetSpace}. \meth{Configure} is simply a performance 363 optimisation. 364\item[\meth{Suspend}] makes a thread inactive. The thread will not 365 be scheduled again until a \meth{Resume} operation is performed on 366 it. A \meth{CopyRegisters} or \meth{ReadRegisters} operation may 367 optionally include a \meth{Suspend} operation on the source thread. 368\item[\meth{Resume}] resumes execution of a thread that is 369 inactive or waiting for a kernel operation to complete. If the 370 invoked thread is waiting for a kernel operation, \meth{Resume} will 371 modify the thread's state so that it will attempt to perform the 372 faulting or aborted operation again. \meth{Resume}-ing a thread that 373 is already ready has no effect. \meth{Resume}-ing a thread that is 374 in the waiting phase of a \meth{Call} operation may cause the 375 sending phase to be performed again, even if it has previously 376 succeeded. 377 378 A \meth{CopyRegisters} or \meth{WriteRegisters} operation may 379 optionally include a \meth{Resume} operation on the destination 380 thread. 381\end{description} 382 383\subsubsection{Virtual Memory} 384 385A virtual address space in seL4 is called a \obj{VSpace}. In a similar 386way to \obj{CSpaces}, a \obj{VSpace} is composed of objects provided 387by the microkernel. Unlike \obj{CSpaces}, these objects for managing 388virtual memory largely directly correspond to those of the hardware, 389that is, a page directory pointing to page tables, which in turn map 390physical frames. The kernel also includes \obj{ASID Pool} and 391\obj{ASID Control} objects for tracking the status of address spaces. 392 393\autoref{fig:vspace} illustrates a \obj{VSpace} with the requisite 394components required to implement a virtual address space. 395 396\begin{figure}[htb] 397 \centering 398 \includegraphics[height=5cm]{imgs/sel4objects_05.pdf} 399 \caption{Virtual Memory in seL4.} 400 \label{fig:vspace} 401\end{figure} 402 403These \obj{VSpace}-related objects are sufficient to implement the 404hardware data structures required to create, manipulate, and destroy 405virtual memory address spaces. It should be noted that, as usual, the 406manipulator of a virtual memory space needs the appropriate 407capabilities to the required objects. 408 409\paragraph{\obj{Page Directory}} 410 411The \obj{Page Directory} (PD) is the top-level page table of the ARM 412two-level page table structure. It has a hardware defined format, but 413conceptually contains 1024 page directory entries (PDE), which are one 414of a pointer to a page table, a 4 megabyte \obj{Page}, or an invalid 415entry . The \obj{Page Directory} has no methods itself, but it is used 416as an argument to several other virtual memory related object calls. 417 418\paragraph{\obj{Page Table}} The \obj{Page Table} object forms the 419second level of the ARM page table. It contains 1024 slots, each of which 420contains a page table entry (PTE). A page table entry contains either an 421invalid entry, or a pointer to a 4 kilobyte \obj{Page}. 422 423\obj{Page Table} objects possess only a single method: 424\begin{description} 425\item[\meth{Map}] takes a \obj{Page Directory} 426 capability as an argument, and installs a reference to the invoked 427 \obj{Page Table} to a specified slot in the \obj{Page 428 Directory}. 429\end{description} 430 431\paragraph{\obj{Page}} 432 433A \obj{Page} object is a region of physical memory that is used to 434implement virtual memory pages in a virtual address space. The 435\obj{Page} object has the following methods: 436\begin{description} 437\item[\meth{Map}] takes a 438 \obj{Page Directory} or a \obj{Page Table} capability as an argument 439 and installs a PDE or PTE referring to the \obj{Page} in the 440 specified location, respectively. In addition, \meth{Map} has a 441 remapping mode which is used to change the access permissions on an 442 existing mapping. 443\item[\meth{Unmap}] removes an existing mapping. 444\end{description} 445 446\paragraph{\obj{ASID Control}} 447 448For internal kernel book-keeping purposes, there is a fixed maximum 449number of applications the system can support. In order to manage 450this limited resource, the microkernel provides an \obj{ASID Control} 451capability. The \obj{ASID Control} capability is used to generate a 452capability that authorises the use of a subset of available address 453space identifiers. This newly created capability is called an 454\obj{ASID Pool}. \obj{ASID Control} only has a single method: 455\begin{description} 456\item[\meth{MakePool}] together with a capability to 457\obj{Untyped Memory} (described shortly) as argument creates an \obj{ASID Pool}. 458\end{description} 459 460\paragraph{\obj{ASID Pool}} 461 462An \obj{ASID Pool} confers the right to create a subset of the available 463maximum applications. For a \obj{VSpace} to be usable by an application, it 464must be assigned to an ASID. This is done using a capability to an 465\obj{ASID Pool}. The \obj{ASID Pool} object has a single method: 466\begin{description} 467\item[\meth{Assign}] assigns an ASID to the \obj{VSpace} 468 associated with the \obj{Page Directory} passed in as an argument. 469\end{description} 470 471\subsubsection{Interrupt Objects} 472 473Device driver applications need the ability to receive and acknowledge 474interrupts from hardware devices. 475 476A capability to \obj{IRQControl} has the ability to create a new 477capability to manage a specific interrupt source associated with a 478specific device. The new capability is then delegated to a device 479driver to access an interrupt source. \obj{IRQControl} has one method: 480\begin{description} 481\item[\meth{Get}] creates an \obj{IRQHandler} capability for the 482 specified interrupt source. 483\end{description} 484 485An \obj{IRQHandler} object is used by driver application to handle 486interrupts for the device it manages. It has three methods: 487\begin{description} 488\item[\meth{SetEndpoint}] specifies the \obj{NTFN} that a 489 \meth{Notify} should be sent to when an interrupt occurs. The driver 490 application usually \meth{Recv}-s on this endpoint for interrupts to 491 process. 492\item[\meth{Ack}] informs the kernel that the userspace driver has finished 493 processing the interrupt and the microkernel can send further pending 494 or new interrupts to the application. 495\item[\meth{Clear}] de-registers the \obj{NTFN} from the 496 \obj{IRQHandler} object. 497\end{description} 498 499\subsubsection{\obj{Untyped Memory}} 500 501The \obj{Untyped Memory} object is the foundation of memory allocation 502in the seL4 kernel. Untyped memory capabilities have a single method: 503\begin{description} 504 \item[\meth{Retype}] creates a number of new kernel objects. If this 505method succeeds, it returns capabilities to the newly-created objects. 506\end{description} 507 508In particular, untyped memory objects can be divided into a group of 509smaller untyped memory objects. We discuss memory management in 510general in the following section. 511 512\subsection{Kernel Memory Allocation} 513\label{sec:kernmemalloc} 514 515The seL4 microkernel has no internal memory allocator: all kernel 516objects must be explicitly created from application controlled memory 517regions via \obj{Untyped Memory} capabilities. Applications must have 518explicit authority to memory (via \obj{Untyped Memory} capabilities) 519in order to create other services, and services consume no extra 520memory once created (other than the amount of untyped memory from 521which they were originally created). The mechanisms can be used to 522precisely control the specific amount of physical memory available to 523applications, including being able to enforce isolation of physical 524memory access between applications or a device. Thus, there are no 525arbitrary resource limits in the kernel apart from those dictated by 526the hardware\footnote{The treatment of virtual ASIDs imposes a fixed 527number of address spaces, but this limitation is to be removed in 528future versions of seL4.}, and so many denial-of-service attacks via 529resource exhaustion are obviated. 530 531At boot time, seL4 pre-allocates all the memory required for the 532kernel itself, including the code, data, and stack sections (seL4 is a 533single kernel-stack operating system). The remainder of the memory is 534given to the first task in the form of capabilities to \obj{Untyped 535Memory}, and some additional capabilities to kernel objects that were 536required to bootstrap the supervisor task. These objects can then be 537split into smaller untyped memory regions or other kernel objects 538using the \meth{Retype} method; the created objects are termed 539\emph{children} of the original untyped memory object. 540 541See \autoref{fig:alloc2} for an 542example. 543 544\begin{figure}[htb] 545 \centering 546 \includegraphics[width=7cm]{imgs/seL4-background_03} 547 \caption{Memory layout at boot time} 548 \label{fig:alloc2} 549\end{figure} 550 551\begin{figure}[htb] 552 \centering 553 \includegraphics[width=7cm]{imgs/seL4-background_04} 554 \caption{Memory layout after supervisor creates kernel services.} 555 \label{fig:alloc-sup} 556\end{figure} 557 558The user-level application that creates an object using \meth{Retype} 559receives full authority over the resulting object. It can then 560delegate all or part of the authority it possesses over this object to 561one or more of its clients. This is done by selectively granting each 562client a capability to the kernel object, thereby allowing the client 563to obtain kernel services by invoking the object. 564 565For obvious security reasons, kernel data must be protected from user 566access. The seL4 kernel prevents such access by using two mechanisms. 567First, the above allocation policy guarantees that typed objects never 568overlap. Second, the kernel ensures that each physical frame mapped 569by the MMU at a user-accessible address corresponds to a 570\obj{Page} object (described above); \obj{Page} objects contain no kernel 571data, so direct 572user access to kernel data is not possible. All other kernel objects 573are only indirectly manipulated via their corresponding capabilities. 574 575\subsubsection{Re-using Memory} 576\label{s:memRevoke} 577 578The model described thus far is sufficient for applications to 579allocate kernel objects, distribute authority among client 580applications, and obtain various kernel services provided by these 581objects. This alone is sufficient for a simple static system 582configuration. 583 584The seL4 kernel also allows memory re-use. Reusing a region of memory 585is sound only when there are no dangling references (e.g.\ 586capabilities) left to the objects implemented by that memory. The 587kernel tracks \emph{capability derivations}, that is, the children 588generated by various \obj{CNode} methods (\meth{Retype}, \meth{Mint}, 589\meth{Copy}, and \meth{Mutate}). Whenever a user requests that the 590kernel create new objects in an untyped memory region, the kernel uses 591this information to check that there are no children in the region, 592and thus no live capability references. 593 594The tree structure so generated is termed the \emph{capability 595derivation tree} (CDT)\footnote{Although we model the CDT as a 596separate data structure, it is implemented as part of the CNode object 597and so requires no additional kernel meta-data.}. For example, when a 598user creates new kernel objects by retyping untyped memory, the newly 599created capabilities would be inserted into the CDT as children of the 600untyped memory capability. 601 602Finally, recall that the \meth{Revoke} operation destroys all 603capabilities derived from the argument capability. Revoking the last 604capability to a kernel object is easily detectable, and triggers the 605\emph{destroy} operation on the now unreferenced object. Destroy 606simply deactivates the object if it was active, and cleans up any 607in-kernel dependencies between it and other objects. 608 609By calling \meth{Revoke} on the original 610capability to an untyped memory object, the user removes all of the 611untyped memory object's children --- that is, all capabilities pointing to 612objects in the untyped memory region. 613Thus, after this operation there are no valid references 614to any object within the untyped region, and the region may be 615safely retyped and reused. 616 617\section{Summary} 618\label{s:backsum} 619 620This chapter has given an overview of the seL4 microkernel. The 621following chapters are generated from the formal Isabelle/HOL 622definitions that comprise the formal specification of the seL4 kernel 623on the ARM11 architecture. The specification does not cover any other 624architectures or platforms. 625 626The order of definitions in this document is as processed by 627Isabelle/HOL: bottom up. All concepts are defined before first used. 628This means the first chapters mainly introduce basic data types and 629structures while the top-level kernel entry point is defined in the 630last chapter (\autoref{c:syscall}). The following section shows 631the dependency graph between the theory modules in this specification. 632We assume a familiarity with Isabelle syntax; see Nipkow et 633al.~\cite{LNCS2283} for an introduction. In addition to the standard 634Isabelle/HOL notation, we sometimes write @{text "f $ x"} for 635@{text "(f x)"} and use monadic do-notation extensively. The latter 636is defined in \autoref{c:monads}. 637 638\section{Theory Dependencies} 639 640\centerline{\includegraphics[height=0.8\textheight]{session_graph}} 641 642\<close> 643(*<*) 644end 645(*>*) 646