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.

沙发：在seL4微内核之上构建的操作系统

自动确保安全策略执行（AASPE） 关于工具 AASPE工具旨在用于制造安全可靠的安全关键系统。 这些工具正在使用AADL和OSATE工具集。 它提供以下功能： 攻击影响元模型 Attack Impact图形编辑器 攻击树编辑器元模型 攻击树图形编辑器 从攻击影响到攻击树的桥梁 从AADL到攻击影响的桥梁 安装工具 逐步版本 步骤1：下载并安装OSATE 进入OSATE并下载。 将产品解压缩到笔记本电脑上。 步骤2：启动OSATE 安装OSATE后，双击可执行文件以启动它。 步骤3：安装安全工具 在“帮助”菜单中，选择“安装新组件”，如下所示。 选择实验性网站一旦显示了可用组件的列表，请选择AASPE工具，如下所示。 接受许可证，确认并重新启动OSATE。 TL; DR版本 要安装工具，可以使用更新站点，然后选择要在Eclipse中安装的工具。 使用的更新站点。 实验性功能的UR

微内核白皮书、sel4微内核白皮书、seL4-whitepaper.pdf

seL4 Tutorials实验源码

seL4的功能介绍，API编程手册说明，非常详细

国外原版介绍seL4系统操作手册，非常详细，值得阅读

seL4内核参考手册中文翻译，主要依据原版本11.0.0（2019年11月20日），对截止当前(2020年4月7日)的内核树少量变动也作了同步更新。在对照源码的基础上力求搬运地清楚准确。

国内知名大学的sel4文档手册，相当值得借鉴，中文版。带书签。