检查与贡献
检查与证据
make ci 运行什么、每项检查表明什么、每个 crate 都遵守的基本规则、如何阅读镜像的 seL4 记录和物料清单，以及关卡如何保持快速。
NoWayOS 的主张不多，而每一项都有一项您可以运行的检查作为支撑。本页说明每项检查能表明什么，以及不能表明什么。
一条命令，涵盖全部
make ci
make ci 就是完整的关卡，按以下顺序运行：密钥扫描、lint、测试、文档、演示、no_std 构建、许可证和安全公告检查、字形图集、物料清单、模糊测试和 Kani 证明，然后是系统检查和 QEMU 启动。只有每一步都通过，变更才算通过。
每项检查表明什么
| 命令 | 它表明什么 |
|---|---|
make test |
单元测试、属性测试、文档测试和黄金图像测试：代码的行为与其测试所描述的一致，且每个屏幕的绘制结果都与核准的完全相同 |
make lint |
rustfmt 和 clippy，警告视为错误 |
make nostd |
每个设备 crate 都能在没有标准库的情况下，为裸机（aarch64-unknown-none）构建 |
make deny |
先检查每个工作区都必须保持的基线，再运行 cargo-deny：许可证、来源、禁用的 crate 以及已知安全公告 |
make secrets |
离线扫描代码树和每一次提交，查找密钥和凭据 |
make fuzz |
每个模糊测试目标，用 libFuzzer 构建并针对生成的输入运行，每个运行 FUZZ_SECONDS（10 秒） |
make kani |
Kani 的有界证明：对于不超过最长记录的任何输入，每个记录解码器都不会 panic、溢出或越界读取；并通过变异检查表明每项证明都能够失败 |
make unsafe-audit |
unsafe 代码只出现在获准清单允许的位置 |
make pds-miri |
Miri 运行获准使用 unsafe 的 crate 的测试，检查是否存在未定义行为 |
make sbom |
每个工作区的 CycloneDX 物料清单 |
make image-sbom SYSTEM=NAME |
一个镜像及其物料清单：内核、加载器、监视器和每个保护域，以及每个保护域中的 crate 及其哈希值 |
make sel4-config-check |
记录在案的 seL4 验证状况，正是固定版本的 Microkit SDK 所对应的状况 |
make qemu-test-all |
每个系统都能在 QEMU 中、以其列出的每种配置启动，并打印其预期文件所规定的内容 |
有界证明只证明到规定大小的输入为止，而不是针对所有可能的输入。模糊测试能发现崩溃，却无法表明不存在崩溃。测试只表明它们所测试的情形。每一项都因其确实能表明的东西而值得拥有。
每个 crate 都遵守的基本规则
这些是每个工作区中的 lint 和检查，而不是指导原则：
- 不得使用
unsafe，只有一份简短的获准清单中、直接访问硬件或内存的 crate 和文件除外。向清单中添加条目需要说明理由并经过审查。 - 外部输入不得引发 panic：库代码中不得使用
unwrap、expect或panic!，不得有未经检查的索引或算术运算，每个 lint 例外都要说明理由。 - 设备 crate 均为
no_std，且不分配任何内存。 发布构建保留溢出检查，一旦 panic，该部分就会停止，而不是继续运行。 - 解析器在复制之前就拒绝过大的输入，返回类型化的错误，并配有属性测试和一个模糊测试目标。
- 任何地方都不得有密钥，开发密钥也不例外。测试密钥在测试运行时生成，从不保存。
阅读镜像的记录
每个镜像都写入 build/BOARD/SYSTEM/，旁边附有两份记录。
sel4-config.txt 写明镜像、其哈希值、开发板、Microkit SDK 和内核，然后说明该镜像相对于 seL4 证明所处的位置，每条理由一行 status:，并把起决定作用的每个内核选项与已验证配置中的取值并列。调试内核属于开发构建。多核或混合关键性内核，或不在 seL4 清单上的开发板，属于在 seL4 的证明范围之外。即使内核与每个选项都一致，也仍然不会被称为“已验证”：记录只给出事实，到此为止。
sbom.cdx.json 是该镜像的 CycloneDX 软件物料清单：它由什么组成，细致到每个保护域中的每个 crate，各自附带 sha256。
让关卡保持快速
完整的证明和模糊测试耗时很长，因此日常的 make ci 只在变更波及之处运行 Kani、模糊测试和 Miri。它会追踪变更所影响的、依赖于它的每个 crate，并跳过自上次通过以来输入没有变化的任何检查。make ci CI_SCOPE=full 会运行所有这些检查，不使用任何缓存；make kani、make fuzz 和 make pds-miri 则始终完整运行。
Kani 是最耗资源的一步：每个证明任务分配约 10 GB 内存，KANI_JOBS 设定同时运行的任务数。如果 make kani 内存不足，请为 Podman 的虚拟机分配更多内存，或设置 KANI_JOBS=1。