<center> # seL4 Microkerneel </center> The idea behind a microkernel is to move as much functionality as possible out of the kernel, the core part of the operating system, and into user-space processes. This approach has several benefits, including increased modularity, flexibility, and security. ### History: One of the first microkernels was the Carnegie Mellon University's Mach kernel, which was developed in the mid-1980s and later became the basis for the Apple Mac OS X operating system. Another well-known microkernel is the L4 microkernel, which was developed in the 1990s by researchers at the German National Research Center for Computer Science. #### Where does sel4 fit in this history ? The seL4 microkernel is a direct descendant of the L4 microkernel, and it has been developed over the past decade by researchers at the Data61 division of the Commonwealth Scientific and Industrial Research Organization (CSIRO) in Australia. seL4 is notable for being the first operating-system microkernel with a formally-verified implementation, meaning that its security and reliability have been mathematically proven. The microkernel is minimized and it only provides basic services in kernel mode: - Memory management - Scheduling - InterProcess Communication (This helps the proof) Basically everything else is done in user space, i.e: - File systems - Device drivers (Serial, Ethernet) - Libraries ## Capabilities The seL4 microkernel uses a capability-based security model, in which access to resources and services is controlled by capabilities, which are encrypted tokens that represent the right to access a specific resource or service. A capability is like a key that unlocks access to a specific resource or service, and can be passed from one process to another as needed. Each capability contains a reference to the resource or service it represents, as well as the rights and permissions associated with that resource or service. For example, a capability might represent the right to read from or write to a specific memory region, or to create new threads. Basically every ressource that the kernel knows about has capabilities. The use of capabilities provides several important security benefits, including (+ Exemples for interrupts): - Fine-grained control: Capabilities allow for fine-grained control over access to resources and services, making it possible to grant only the necessary rights and permissions to each process. - Exemple: Access to interrupt handling can be restricted to only the processes that require it, using capabilities - Tamper-proof: Capabilities are encrypted and protected by the kernel, making it impossible for a process to modify or forge a capability. - Exemple: Capabilities ensure that only trusted processes can handle interrupts, and prevent unauthorized processes from tampering with interrupt handling. - Transferable: Capabilities can be passed from one process to another, allowing for secure delegation of access to resources and services. - Exemple: Capabilities can be passed between processes, allowing for secure delegation of interrupt handling responsibilities, as needed - Revocable: Capabilities can be revoked by the kernel at any time, allowing for dynamic control over access to resources and services. - Exemple: Dynamic control over interrupt handling, and making it possible to add or remove interrupt handling capabilities as needed. #### The derivation tree The capability derivation tree refers to the hierarchical structure that is used to manage capabilities and control access to resources and services. The tree consists of nodes that represent capabilities and the relationships between them. Each capability in the tree represents a specific resource or service, and can have parent and child capabilities. A parent capability represents a higher-level resource or service, and child capabilities represent more specific or lower-level resources or services. For example, consider a capability that represents access to a specific memory region. A child capability of that capability might represent access to a specific sub-region of that memory, or a different permission level (e.g., read-only access). #### The capability database The capability database is a centralized repository of information about capabilities, while the capability derivation tree is a data structure that represents the relationships between capabilities and processes in the seL4 microkernel #### Acquiring a capability to handle an interrupt Tutorial: https://docs.sel4.systems/Tutorials/interrupts.html a process can acquire a capability to handle an interrupt through a process called capability allocation. The process of capability allocation involves several steps: 1. The process that needs the capability invokes a system call asking the kernel for a capability to handle the interrupt. 2. The kernel checks its capability database to determine if the process has the necessary permissions to acquire the capability. 3. If the required permissions are present, the kernel allocates a capability to the process and adds it to the capability derivation tree. Here is an example of what the process of handling an interrupt in the seL4 microkernel might look like: 1. The hardware generates an interrupt. 2. The kernel determines the process that has the capability to handle the interrupt. (Via capability databse) 3. The process with the capability to handle the interrupt is notified of the interrupt. 4. The process with the capability to handle the interrupt performs the necessary actions to handle the interrupt. 5. The process with the capability to handle the interrupt signals to the kernel that the interrupt has been handled. ## Untyped memory Tutorial: https://docs.sel4.systems/Tutorials/untyped.html There are ten types of seL4 objects, all referenced by capabilities: - **Endpoints** are used to perform protected function calls - **Reply Objects** represent a return path from a protected procedure call - **Address Spaces** provide the sandboxes around components (thin wrappers abstracting hardware page tables) - **Cnodes** store capabilities representing a component’s access rights - **Thread Control Blocks** represent threads of execution - **Scheduling Contexts** represent the right to access a certain fraction of execution time on a core - **Notifications** are synchronisation objects (similar to semaphores) - **Frames** represent physical memory that can be mapped into address spaces - **Interrupt objects** provide access to interrupt handling - **Untyped memory** unused (free) physical memory that can be converted (“retyped”) into any of the other types. Untyped memory refers to a block of physical memory (the kernel uses physical memory for itself and virtual memory for user-space) that has not been assigned a specific type or size and is used as a resource for allocating memory for objects mentionned abovee such as capabilities, threads, and address spaces. ## Endpoints Tutorial: https://docs.sel4.systems/Tutorials/ipc.html An endpoint is a type of IPC (Inter-Process Communication) channel (like linux pipes, sockets) that allows processes to send messages to each other in a secure and efficient manner. When a process wants to send a message to another process, it writes the message to the endpoint capability and specifies the receiving process. The kernel then delivers the message to the receiving process, which can read the message from the endpoint. (System call) Endpoints can be used to transfer capabilities and send notifications. They are protected by the capabilities-based security model of the seL4 microkernel. This helps to ensure that only authorized processes can access the endpoint and send messages. This is meant for small data transfer. For larger data like files, one should use shared memory (shared virtual mapping to some memory). The process of creating shared memory typically involves the following steps: 1. Allocating physical memory: The first step is to allocate a portion of physical memory that will be used for the shared memory region. This can be done using the `seL4_Untyped_Retype` system call, which allows a process to allocate a portion of untyped memory and specify its type. 2. Creating a capability: Once the physical memory has been allocated, a capability must be created to represent the shared memory region. This is done using the `seL4_CNode_Create` system call, which creates a new capability in the capability space of the process. 3. Sharing the capability: The capability representing the shared memory region can be shared between processes via and endpoint `seL4_Call`. ## Verification Roadmap: TODO In addition to the provided, extract key points if any from https://www.youtube.com/watch?v=lvmjXO1jTec.