QEMUで最初のシステムを動かす

Rustの保護ドメインひとつでQEMU上にseL4を起動し、システムを定義する三つのファイルを読み、手を伸ばしすぎた部分をseL4が止めるのを見届け、ユーザーインターフェースをクリックして操作します。

NoWayOSのシステムとは、seL4の上で一緒に起動する保護ドメイン、つまりデバイスの部分の集まりです。すべてのシステムは、まずQEMUで、開発コンテナの中で起動し、自らの出力をチェックします。このページでは、いちばん小さなシステムを起動し、続いて、もう少し多くを見せてくれるいくつかのシステムを起動します。

helloを起動する

make qemu-test SYSTEM=hello

これでhelloシステムがビルドされ、付与がチェックされ、seL4がQEMUでヘッドレスに起動し、その出力が監視されます。システムが出力すべきすべての行が順番どおりに現れ、禁じられたものが何も現れなければ合格です。

自分で起動して様子を見るには、make qemu SYSTEM=helloを実行してください。QEMUを終了するには、Ctrl-Aを押してからxを押します。

システムを定義する三つのファイル

各システムはsystems/にある三つのファイルからなり、Rustのコードはその隣のpds/にあります。

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 は、システムが付与するものすべてを、1行にひとつの事実として並べます。記述がここにないものを付与していたり、ここにあるものを付与していなかったりすれば、ビルドは失敗します。そのため、システムに何を許すかの変更は、レビューで必ず目に入ります。

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-test SYSTEM=NAMEで実行でき、make qemu-test-allですべてのシステムを実行できます。

ユーザーインターフェースをクリックして操作する

make qemu SYSTEM=ui-interactive VNC=1

QEMUの画面は、手元のマシンのlocalhost:5900でVNC経由で公開され、その実行限りのパスワードが表示されます。macOSではvnc://localhost:5900を開き（Finderの「移動」→「サーバへ接続」）、デモ画面をクリックして操作してください。

ビルドが各イメージの隣に残すもの

build/BOARD/SYSTEM/（今回のシステムならbuild/qemu_virt_aarch64/hello/など）の中、loader.imgの隣に、次のものが置かれます。

sel4-config.txt：イメージのseL4構成と、それがseL4の証明の範囲に入っているかどうか。デバッグビルドは、範囲外であることをはっきり記します。セキュリティを参照してください。
sbom.cdx.json：イメージのCycloneDX形式のソフトウェア部品表。カーネル、ローダー、各保護ドメインとそこに含まれるクレートを、それぞれハッシュ付きで記載します。
イメージに含まれるもののライセンスファイル。フォントやアイコンのライセンスなど。