术语，用平实的话说清楚。

设备拒绝启动未经其制造商签名的软件。NoWayOS 计划在生产硬件上实现；尚未构建。

Microkit 系统中一个相互隔离的部分：一个拥有自己内存的程序，只持有明确授予它的能力。也就是 NoWayOS 的密封隔离舱。

从启动开始计数的时间，从不设置，也从不倒退。NoWayOS 的每个超时都使用它，它也从不与挂钟时间混用。

一个尝试触及未被授予之资源的系统，seL4 必须阻止它。一个故意放宽了授权的变体必须失败，这表明测试确实能够失败。

攻击者可能用来对付一台设备的一切：它的代码、服务、接口和输入。代码越少、功能越少，攻击面就越小。

打造一台做不了那些高风险之事的设备，因为相应的功能从未被内置。这正是 NoWayOS 的方法。

当保护域做了内核不允许的事情或发生 panic 时，seL4 所报告的事件。该部分会保持停止，直到其故障处理程序采取行动。

NoWayOS 设备在故障接连不断时进入的状态：只有监管器、看门狗以及（在可能的情况下）显示继续运行，直到冷启动。

日期和时刻，来自经过认证的来源。NoWayOS 把它与单调时间分开，作为不同的类型。

seL4 带有调度预算和周期的配置，Microkit 构建的就是它。其 AArch64 证明仍在进行中，因此目前没有任何 NoWayOS 镜像处于 seL4 已完成的证明范围之内。

接收其他部分的故障、报告故障并让系统干净地重新启动的保护域。

固定版本的容器镜像，装有 NoWayOS 的全部工具链：Rust 工具链、Microkit SDK、QEMU 和各种检查工具。每个 make 目标都在其中运行，因此您的机器只需要 Podman 和 make（驱动 Raspberry Pi 5 时还需要 Python 3.11）。

一种硬件定时器，除非软件定期喂它，否则会复位开发板。NoWayOS 的看门狗保护域只有在其他每个部分都回应其心跳时才会喂它。

一项安全属性所依赖的、必须正确无误的一切。对 NoWayOS 系统而言：seL4 内核、Microkit 加载器和监视器，以及该属性所依赖的保护域。

固定大小、布局明确的记录，通过共享内存在保护域之间传递，并在接收时检查。参见先复制，再检查。

从断电状态开始的启动，与复位相对。只有冷启动才能让 NoWayOS 设备从故障安全状态中恢复。

用数以百万计的生成输入测试解析器，直到某个输入使其崩溃或违反某项检查。NoWayOS 每个处理外部输入的解析器都有一个模糊测试目标。

诸如读取超出缓冲区末尾、或在内存释放后继续使用之类的错误。Microsoft 和 Google 都曾报告，它们约 70% 的严重安全缺陷属于这一类；安全 Rust 可以杜绝这类缺陷。

在 seL4 中，一种无法伪造的令牌，指明一个内核对象以及对它所持有的权限，就像一张只开一扇门的门禁卡。保护域只能触及其能力所指明的东西。

通过更改设置让通用设备更安全。这些功能仍然存在，一个缺陷就可能绕过所有设置。

systems/NAME.grants：系统授予的一切，每行一个事实：优先级、预算、内存、设备、中断和通道。只要系统描述与授权文件不一致，构建就会失败。

一种缺陷：代码检查共享内存中的数据后又再次读取它，让另一方有机会在两次读取之间更改数据。先复制，再检查可以防止这种缺陷。

在 Microkit 中，两个保护域之间声明的连接，用于通知（不携带数据的信号，中断也属于此类）和受保护过程调用。

尽可能保持精简的内核，驱动程序、网络和屏幕都运行在内核之外，各自位于自己的隔离舱中。seL4 就是一个微内核。

Microkit 的 XML 文件，声明系统的每个保护域、内存区域、通道和中断。它就是系统的安全设计，对它的任何修改也都按安全设计来审查。

一条规则：消息在验证之前先从共享内存中复制出来，因此发送方无法在检查与使用之间更改它。它可以防止双重读取。

由计算机检查的数学证明，证明软件符合其规约。seL4 针对特定配置拥有这种证明。NoWayOS 自身的代码则依靠 Rust、隔离、测试和有界证明。

证明某个性质对不超过规定大小的每个输入都成立。NoWayOS 用 Kani 以这种方式证明其消息解码器。

systems/NAME.expect：系统必须按顺序打印的各行，以及一旦在任何地方出现就会使测试失败的文本。同一个文件既在 QEMU 中、也在 Raspberry Pi 5 上检查系统。

设备以密码学方式向远程服务证明它启动了哪些软件。它表明的是启动时加载了什么，而不是此后发生的一切。NoWayOS 计划在生产硬件上实现；尚未构建。

在构建时预先绘制成字符图像的字体，使设备绘制文字时从不需要解析字体文件。

一种用于软件物料清单的开放标准格式。NoWayOS 为每个工作区和每个系统镜像各写一份。参见 SBOM。

Raspberry Pi 的 USB 转串口适配器。接在 Raspberry Pi 5 的调试接口上，它传送启动日志并加载测试镜像。

一个面向没有操作系统图形栈的设备的 Rust 2D 图形库。NoWayOS 的用户界面用它绘制。

NXP 的工业级 Arm 处理器系列，也是 NoWayOS 计划中的生产硬件。目前尚不支持。

一个 Rust 模型检查器，能证明某些性质对界限以内的每个输入都成立。NoWayOS 用它证明其消息解码器永远不会 panic、溢出或越界读取。

seL4 基金会的框架，用于构建由系统描述中声明的保护域组成的静态 seL4 系统。

一个能检测未定义行为的 Rust 解释器。NoWayOS 对少数获准使用 unsafe 代码的 crate 运行它。

一个开源的机器模拟器。每个 NoWayOS 系统在接触硬件之前，都先在其中启动并检查自身的输出。

NoWayOS 用作参考硬件的低成本开发板。

一种编程语言，其安全代码可以杜绝内存安全缺陷。NoWayOS 自身的代码全部用 Rust 编写。

seL4 基金会提供的 Rust 支持，包括用于编写 Microkit 保护域的 crate。

一个用 Rust 编写的 TLS 库。NoWayOS 的 TLS 1.3 客户端基于它和 RustCrypto 构建。

软件物料清单：列出一个软件中每个组件及其版本的清单。NoWayOS 为每个工作区和每个系统镜像各写一份 CycloneDX 格式的 SBOM。

NoWayOS 的构建时工具，把以 TSX 按受支持子集编写的 React 屏幕转换为面向 NoWayOS 用户界面的 Rust 代码。对子集之外的任何内容，它一律拒绝，而不是近似处理。

seL4 设备驱动框架（seL4 Device Driver Framework）：一种基于 Microkit、使用共享内存队列的驱动程序参考设计。NoWayOS 的网络队列遵循这一设计。

一个约 10,000 行的微内核，由 seL4 基金会维护，针对特定配置拥有经机器检查的正确性与安全性证明。NoWayOS 运行在它之上。

写在每个 NoWayOS 镜像旁的记录：其 seL4 配置，以及该配置是否处于 seL4 已完成的证明范围之内。

为一台设备的唯一任务而构建的操作系统，而不是先构建成什么都能运行、再锁定为只做一件事。它由三点界定：专为一项任务而建（镜像只包含应用、应用使用的驱动程序和内核，别无其他）；内部密封（每个部分都在自己的隔离舱中，只能触及被授予的资源）；有据可查（内部有什么，都附有证据）。它不是 Kiosk 模式——那只是把配置式安全的系统锁定在一个应用上。NoWayOS 就是一个 Single Purpose OS：一台心无旁骛的计算机。

一个用 Rust 编写、运行时不分配内存的 TCP/IP 协议栈。NoWayOS 的网络协议栈基于它构建。

编译器无法检查其内存安全的 Rust 代码。除了一份由检查强制执行的、简短且经过审查的清单之外，所有 NoWayOS crate 都禁止使用。