安全
它只做分内之事。
NoWayOS 设备省去任务用不上的东西，并把留下的部分密封在隔离舱中。本页说明这一切依托什么、哪些已被证明、哪些尚未证明，以及哪些仍需由您来做好。
省去了什么
NoWayOS 镜像包含其应用、该应用使用的驱动程序以及 seL4 微内核。没有浏览器引擎、窗口系统、Shell、包管理器或用户账户：它们从未被内置，因此既无从被利用，也无需打补丁，更谈不上配置错误。NoWayOS 的设计旨在减少不必要的软件和服务：任务用不上的，就不在镜像里。
这正是这个名字的含义：从未内置的东西，就无从被利用。这是对“缺席之物”的陈述，而不是承诺永远不会出问题。内置的部分仍然可能有缺陷；我们的主张是：这样的部分少得多，而且缺陷会留在它所在的隔离舱中。
锁定通用系统属于配置式安全：被锁起来的功能依然存在，一个缺陷就可能绕过所有设置。NoWayOS 的目标是构造式安全：这些功能从来就不存在。
如何遏制故障
- 每个部分都运行在自己的保护域中，拥有自己的内存，只持有其系统描述授予的能力。seL4 强制执行这些能力。
- 每项授权都列在系统的授权文件中；只要系统描述授予了文件未列出的任何东西，或者反过来，构建就会失败。放宽授权会被当作安全变更来审查。
- 部分之间的消息是固定大小的记录，在接受检查之前先从共享内存中复制出来，因此发送方无法在记录通过检查后再更改它。
- 输入在检查之前一律视为恶意。每个处理外部输入的解析器都经过模糊测试，并且构建为永不 panic；应用看到的是按键、指针和触摸事件，而从不接触设备协议。
- 监管器会停止出故障的部分，并让系统干净地重新启动。反复出现的故障会让设备进入故障安全状态，直到冷启动为止。
seL4 的证明覆盖什么，不覆盖什么
seL4 是一个约 10,000 行的微内核，拥有经机器检查的正确性与安全性证明。这些证明是难得的成就，而它们针对的是特定平台上的特定配置。确切的情况如下：
NoWayOS 运行在 seL4 微内核之上，seL4 针对我们硬件上的特定配置拥有经机器检查的正确性与安全性证明；NoWayOS 使用 seL4 的混合关键性配置，该配置的证明仍在进行中。
- 平台： seL4 的 AArch64 已验证配置列出了 Raspberry Pi 5 以及 NXP 的 i.MX8M Mini、Plus 和 Quad。
- 调度： Microkit 构建的是 seL4 的混合关键性（MCS）内核，其 AArch64 证明仍在进行中。因此，目前没有任何 NoWayOS 镜像处于 seL4 已完成的证明范围之内。
- 核心： 这些证明针对的是单核内核。使用多个核心的镜像不在证明范围之内，并会如实说明。
- 内核之上： Microkit 的工具以及 NoWayOS 的保护域和驱动程序不在 seL4 的证明覆盖范围内。它们的保障来自 Rust、隔离、审查、测试以及 NoWayOS 自己的有界证明。
每个镜像都会把它的配置记录在旁边的 sel4-config.txt 中。下面是 hello 系统的一个开发构建的记录对自身的描述：
system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list
即便某个镜像的内核与已验证配置的每个选项都一致，我们在这里也不会称它“已验证”。记录陈述事实，而事实就已足够。
证据，以及每项证据对应的命令
本页的每项主张都附有证据，而每一份证据都来自任何人都能在开发容器中运行的命令。make ci 会按顺序运行它们，make ci CI_SCOPE=full 会运行每一项证明和每一个模糊测试目标；检查与证据逐一作了说明。
| 主张 | 证据 | 运行 |
|---|---|---|
| 每项授权都有记录。 | 每个系统的授权文件，每次构建时都会对照其系统描述进行检查。 | make qemu-test SYSTEM=hello |
| 一个部分无法触及未被授予的资源。 | 隔离测试：其探针会进行未经授权的读写，seL4 必须阻止它们；另有一个故意放宽了授权的变体，它必须失败。 | make qemu-test SYSTEM=isolation-test |
| 消息解码器的性质对界限以内的每个输入都成立。 | 针对每个消息记录解码器的 Kani 证明，并通过变异检查表明这些证明能够失败。 | make kani |
| 处理外部输入的解析器能经受住恶意输入。 | 每个处理不可信输入的解析器都有一个模糊测试目标。崩溃一经修复，就会成为回归测试。 | make fuzz |
| unsafe 代码只出现在获准的位置。 | 一份允许清单，列出少数可以使用它的 crate 和文件，由 make ci 强制执行，并对这些 crate 运行 Miri。 | make unsafe-audit |
| 每个组件都是已知的。 | 每个工作区和每个系统镜像都有一份 CycloneDX 软件物料清单，每个组件都附带哈希值。 | make image-sbom SYSTEM=hello |
| 许可证和安全公告都经过检查。 | 对每个工作区运行 cargo-deny：许可证、来源、禁用的 crate 以及已知安全公告。 | make deny |
| 代码中没有密钥。 | 离线扫描代码树和每一次提交，查找密钥和凭据。 | make secrets |
| 每个镜像的 seL4 配置都有记录。 | 每个镜像旁都有一个 sel4-config.txt，另有一项检查，确认记录中的参考值与固定版本的 Microkit SDK 一致。 | make sel4-config-check |
阅读一个镜像的证据
您无需构建任何东西，就能看到证据是什么样子。下面是一个真实镜像的全部证据：ui-interactive，即可点击的用户界面，于 2026年11月1日为 QEMU 构建。
- 它的软件物料清单（CycloneDX 1.5）：62 个组成部分，从 seL4 内核和 Microkit 的加载器，到每个保护域中的每个 crate，各自附带 SHA-256。
- 它的 seL4 配置记录：它所运行的内核，逐项对照 seL4 的已验证配置，并明确指出它在哪些方面落在证明范围之外。
- 它的系统描述：每个保护域、内存区域、中断和通道，与 Microkit 构建它们的方式一致。
- 它的授权文件：同样的授权，每行写下一个事实，构建会对照系统描述检查它。
- 它绘制的屏幕：每次运行测试时，都会与这张核准图像逐像素比对。
仍由您负责的部分
NoWayOS 是一个平台，而不是经过认证的产品。一台设备是否安全，还取决于它如何部署和运行，而这部分属于构建和运营它的人。
- 物理安全。 一个插上的设备，或一只握住电源线的手，仍然可能让设备停止服务。外壳、端口和电源属于基于 NoWayOS 构建的产品的设计范畴。
- 每个系统授予什么。 NoWayOS 会检查系统与其授权文件是否一致。这些授权是否适合该任务，则是一项设计决策，也应当作为设计决策来审查。
- 网络与后端。 设备只连接其系统允许的目标。这些服务如何处理收到的内容，其安全由它们自己负责。
- 密钥与更新。 可安全回退的签名更新已完成设计，尚未构建。谁持有签名密钥、发布如何获批，是运营层面的决策。
- 认证。 运行在 NoWayOS 上的受监管产品需各自取得认证。NoWayOS 的设计目标是提供它们所需的证据；它本身并未经过认证。
尚未构建
- 安全启动和远程证明属于带有硬件信任根的生产硬件。两者都尚未构建。
- 在设备上应用的签名更新。 更新记录及其检查已经存在；在设备上应用更新的路径则尚未实现。
- Raspberry Pi 5 是开发板，而不是加固设备。拿到它的人可以替换其软件，而且在它上面，USB 设备的内存访问尚未受到限制。
您在这里找不到的词
我们不会称 NoWayOS“无法被黑客攻破”“防篡改”或“坚不可摧”，也不会声称它具有“零攻击面”。没有什么能做到这些；如果我们这样说，您停下不读也理所应当。本页的主张比这些要小，而且每一项都附有证据。
报告漏洞
请按照各代码仓库的 SECURITY.md 所述，私下报告漏洞：通过代码仓库 Security 选项卡中 GitHub 的私密漏洞报告功能，或发送电子邮件至 security@nowayos.com，不要提交公开 issue。由于每个部分都运行在自己的隔离舱中，按照设计，缺陷在修复期间会留在原处。