在 QEMU 中运行您的第一个系统

在 QEMU 中用一个 Rust 保护域启动 seL4，读懂定义系统的三个文件，看 seL4 如何阻止越界的部分，并点击体验用户界面。

NoWayOS 的系统是一组保护域，也就是设备的各个部分，它们在 seL4 上一同启动。每个系统都先在开发容器内的 QEMU 中启动，并检查自身的输出。本页先启动最小的一个，再启动几个能展示更多内容的系统。

启动 hello

make qemu-test SYSTEM=hello

这会构建 hello 系统、检查其授权，在 QEMU 中以无界面方式启动 seL4，并监视它打印的内容。当系统必须打印的每一行都已按顺序出现，且没有出现任何被禁止的内容时，测试即通过。

如果想亲自启动并观察，请运行 make qemu SYSTEM=hello。按 Ctrl-A，再按 x，即可退出 QEMU。

定义系统的三个文件

每个系统都由 systems/ 中的三个文件组成，与 pds/ 中的 Rust 代码并列。

hello.system 是 Microkit 系统描述：系统拥有的每个保护域、内存区域、通道和中断。hello 只有一个保护域，别无其他：

<system>
 <protection_domain name="hello" priority="1" stack_size="0x10000">
 <program_image path="nowayos-hello.elf" />
 </protection_domain>
</system>

hello.grants 列出系统授予的一切，每行一个事实。只要系统描述授予了这里没有列出的任何东西，或者这里列出了描述并未授予的东西，构建就会失败，因此对系统权限的任何改动，在审查时总是一目了然：

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect 按顺序列出系统必须打印的各行；以 ! 开头的，则是无论出现在哪里都会立即使测试失败的文本：

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

同一个预期文件也会根据开发板的串口日志，在 Raspberry Pi 5 上检查该系统。

保护域本身

pds/hello/src/main.rs 就是整个程序。它沿用 rust-sel4 的 Microkit 示例的最小结构：init 在启动时运行一次；如果系统为它提供了任何通道，处理程序就会接收通知。

#![no_std]
#![no_main]

use sel4_microkit::{Handler, Infallible, debug_println, protection_domain};

#[protection_domain]
fn init() -> HelloPd {
 debug_println!("NOWAYOS: rust pd starting");
 debug_println!("NOWAYOS: hello from rust");
 HelloPd
}

struct HelloPd;

impl Handler for HelloPd {
 type Error = Infallible;
}

这里没有堆（任何分配都会导致链接失败），没有 unsafe，也没有设备。之所以能打印，只是因为这是调试构建：发布版内核没有调试控制台。

看 seL4 阻止一个部分

make qemu-test SYSTEM=isolation-test

两个探针保护域各自尝试做未被授予的事：一个读取未映射给它的内存，另一个向只允许它读取的页面写入。seL4 以故障阻止了每一个，而一个旁观的保护域则毫发无损地继续运行。测试的最后一行这样写道：

NOWAYOS: isolation-test: 2 of 2 forbidden accesses faulted and were contained; bystander still running

系统	它展示了什么
`ipc-demo`	两个保护域通过共享环形缓冲区交换类型化记录；格式错误的记录会被拒绝
`timer-demo`	定时器保护域响应两个客户端，并按截止时间的先后交付它们的超时
`supervisor-test`	监管器接收到一个故障并复位开发板，下一次启动时其内存焕然一新
`ui-demo`	用户界面的脚本化会话，每一帧的哈希值都经过检查

点击体验用户界面

make qemu SYSTEM=ui-interactive VNC=1

QEMU 的屏幕通过 VNC 发布在您机器的 localhost:5900 上，并会打印一个仅对本次运行有效的密码。在 macOS 上，打开 vnc://localhost:5900（在“访达”中：“前往”>“连接服务器”），即可点击浏览各个演示屏幕。

构建在每个镜像旁留下了什么

在 build/BOARD/SYSTEM/ 中（对上述系统而言，即 build/qemu_virt_aarch64/hello/ 等），loader.img 旁边有：

sel4-config.txt：镜像的 seL4 配置，以及它是否处于 seL4 的证明范围之内。调试构建会明确说明它不在范围内。参见安全。
sbom.cdx.json：该镜像的 CycloneDX 软件物料清单：内核、加载器、每个保护域及其中的 crate，各自附带哈希值。
镜像所含内容的许可证文件，例如字体和图标的许可证。