内核对象-db31dsjz005-2020 公共数据安全分级指南

2.3 内核对象 操作系统内核提供的功能，很多并不是内核本身提供的，而是跑在内核态的程序提供 的，象Linux这样的操作系统的内核，这类内核程序可能是驱动，或以伪驱动形式存在的 内核程序。 seL4中的内核对象是内核向用户程序提供的一组功能集，应用程序眼中的这些内核对 象，与内核眼中的这些对象，在接口上是一样的，就是说，服务态程序中看到的这些对象， 并没被单独包装过，只是需要通过句柄才能标识这些对象。  CNodes 存储句柄（capabilities），以使线程可以访问特定对象中的方法。每个CNode有固定 数量的槽（Slot），槽的数量于CNode创建时确定，槽中可以有一个句柄，也可以为空。  线程控制块 Thread Control Blocks （TCBs） 线程是seL4中执行与调度的基本单位，提供有阻塞、非阻塞等等功能。  IPC端点 IPC Endpoints 实现线程间的通信，seL4内核提供有下列两种端点：  同步端点 Synchronous endpoints (Endpoint), which cause the sending thread to block until its message is received; and  异步端点 Asynchronous endpoints (AsyncEP), which only allow short messages to be sent, but do not cause the sender to block. 一个指向端点的句柄可以被限定为只发送（send-only）或只接收（receive-only）， 并可以被设置为可以在线程间传递。  虚拟地址空间对象 Virtual Address Space Objects 用来创建虚拟地址空间（或VSpace），这些虚拟地址空间可以给一个线程或多个线程 使用。这些对象管理着物理的存储设备，例如，页字典（page directory）管理着页 表（page directory），页表就是让你的虚拟地址与物理地址对应起来的那个物理器 件MMU，内核还包括ASID Pool和ASID Control对象，用来跟踪地址空间状态。  中断对象 Interrupt Objects give applications the ability to receive and ac-knowledge interrupts from hardware devices. Initially, there is a capability to IRQControl, which allows for the creation of IRQHandler capabilities. An IRQHandler capability permits the management of a speci c interrupt source associated with a speci c device. It is delegated to a device driver to access an interrupt source. The IRQHandler object allows threads to wait for and acknowledge individual interrupts.  原始内存 Untyped Memory is the foundation of memory allocation in the seL4 kernel. Untyped memory capabilities have a single method which allows the creation of new kernel objects. If the method succeeds, the calling thread gains access to capabilities to the newly-created objects. Additionally, untyped memory objects can be divided into a group of smaller untyped memory objects allowing delegation of part (or all) of the system's memory. We discuss memory management in general in the following sections.