系统如何组成

每台 NoWayOS 设备都是一个系统：一组固定的部分，在构建之前就已声明，每个部分都由 seL4 与其他部分隔离开来。运行时不会添加任何东西。本页介绍这些组成部分，以及它们如何相互连接。

保护域

保护域是系统的一个部分：一个拥有自己内存的程序，只持有被授予的能力（capability）。在 seL4 中，能力是一种无法伪造的令牌，指明一个内核对象以及对它所持有的权限，就像一张只开一扇门的门禁卡。凡是其能力没有指明的东西，保护域一概无法触及，而 seL4 强制执行这一点。

典型的系统为每项职责各设一个保护域：显示驱动、输入路径、网络协议栈、用户界面、应用、定时器、监管器和看门狗。每个保护域都是一个小型 Rust 程序，no_std，启动后不再分配任何内存。

系统描述

Microkit 系统描述（systems/NAME.system，一个 XML 文件）声明整个系统：每个保护域及其优先级、预算和栈；每个内存区域以及由谁映射它；每个通道；每个中断。

• 描述中只写设备名，从不写地址：phys_addr="@NAME"。地址来自 platforms/ 中该开发板的文件，每个地址都注明出处，因此同一份描述既能为 QEMU 构建，也能为 Raspberry Pi 5 构建。
• 通道连接两个保护域，用于通知（不携带数据的信号，中断也属于此类）和受保护过程调用（对更高优先级部分的同步调用）。

系统描述就是系统的安全设计，因此对它的修改会被当作安全变更来审查。

授权文件

在每份描述旁，systems/NAME.grants 列出系统授予的一切，每行一个事实：优先级、预算、内存、设备、中断和通道。只要两者在任一方向上不一致，构建就会失败。

每个保护域还有一个角色（ui、input、broker、display、driver、network、security、storage、update、app、supervisor、watchdog、clock 或 test），构建会拒绝其角色绝不应拥有的授权。用户界面不会被误交一个网络设备，测试工具也无法混进产品。

类型化消息

保护域之间通过类型化消息通信：固定大小、带版本、布局明确的记录，经由共享内存上的单生产者单消费者环形缓冲区传递。

• 先复制，再检查。 接收方在验证每条记录之前，先把它从共享内存中复制出来，因此发送方无法在检查与使用之间更改它（这种缺陷称为双重读取）。
• 解码器不会 panic。 每个解码器对任何格式错误的输入都返回类型化的错误，并配有 Kani 有界证明和一个模糊测试目标。
• 双方各有自己的视图。 生产者和消费者通过各自独立的内存视图访问环形缓冲区，共享索引使用 acquire 和 release 内存序。

输入

应用看到的是规范化的输入事件：按键、指针移动和触摸，它们已对照屏幕进行检查，并经过速率限制。应用从不接触 USB 或任何其他设备协议；输入路径在自己的保护域中解析这些协议，并把每个字节都视为恶意。

故障、监管器和故障安全状态

当保护域做了 seL4 不允许的事情，或发生 panic 时，seL4 会停止它，并向其父级报告一个故障。

• 监管器是其他部分的父级。它接收每个故障并报告，然后复位开发板，让系统干净地重新启动。它已在 QEMU 测试系统中构建并经过测试。
• 故障安全状态是设备在故障接连不断时进入的状态：默认情况下，在自冷启动以来第四次重启时进入，或在存储、更新等安全敏感部分第二次出现故障时进入。此时只有监管器、看门狗以及（在可能的情况下）显示继续运行，并且只有从断电状态开始的冷启动才能让设备恢复。
• 看门狗保护域只有在其他每个部分都回应其心跳时，才会喂硬件看门狗。一旦有某个部分停止回应，硬件就会复位开发板。

内存与时间

• 内存在构建镜像时就已固定。 设备代码不分配任何内存：每个缓冲区和队列都有固定大小，来自 nowayos-bounded。唯一的例外是 TLS 客户端，它在自己的固定内存区（arena）中工作。
• 两种永不混用的时间。 单调时间从启动开始计数，从不倒退；每个超时都使用它。挂钟时间，即日期和时刻，来自经过认证的来源。它们是不同的 Rust 类型，因此不能在需要其中一种的地方传入另一种。

构建您自己的系统

您产品自己的系统和保护域位于一个独立的代码仓库中，与 nowayos 并列，而绝不放在它里面。该代码仓库的 Makefile 设置 SYSTEM_REPO := $(CURDIR)，并引入 NoWayOS 的 make 片段：

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

这样，make image、make qemu-test、make qemu-test-all 以及各项检查就会作用于它的 systems/ 和 pds/，并使用 NoWayOS 的开发容器、开发板文件、授权规则和检查。相关变量记录在 tools/make/system.mk 的开头。Showcase 正是这样构建的。