システムの組み立て

NoWayOSのデバイスは、どれもひとつのシステムです。ビルドする前に宣言された部分の固定された集まりで、各部分はseL4によって互いに切り離されています。実行時に何かが追加されることはありません。このページでは、それぞれの部品と、そのつながり方を説明します。

保護ドメイン

保護ドメインは、システムを構成する部分のひとつです。自分専用のメモリを持ち、付与されたケイパビリティだけを保持するプログラムです。seL4において、ケイパビリティとは、ひとつのカーネルオブジェクトと、それに対して持つ権限を指し示す、偽造できないトークンです。ひとつの扉だけを開けるカードキーのようなものです。保護ドメインは、自らのケイパビリティが指し示さないものには何も触れられず、seL4がそれを強制します。

典型的なシステムには、関心ごとにひとつずつ保護ドメインがあります。ディスプレイドライバ、入力経路、ネットワークスタック、ユーザーインターフェース、アプリケーション、タイマー、スーパーバイザー、ウォッチドッグ。それぞれがno_stdの小さなRustプログラムで、起動後は何も確保しません。

システム記述

Microkitのシステム記述（systems/NAME.system、XMLファイル）は、システム全体を宣言します。優先度、予算、スタックを伴うすべての保護ドメイン。すべてのメモリ領域と、それを誰がマップするか。すべてのチャネル。すべての割り込み。

• 記述はデバイスを名前で指し、アドレスは決して書きません（phys_addr="@NAME"）。アドレスはplatforms/にあるボードのファイルから、それぞれ出典付きで取り込まれるので、同じ記述でQEMU向けにもRaspberry Pi 5向けにもビルドできます。
• チャネルは二つの保護ドメインをつなぎ、通知（データを持たないシグナル。割り込みもそのひとつ）と、保護された手続き呼び出し（より優先度の高い部分への同期呼び出し）に使われます。

記述は、システムのセキュリティ設計そのものです。そのため、記述への変更はセキュリティ上の変更としてレビューされます。

付与ファイル

各記述の隣にあるsystems/NAME.grantsは、システムが付与するものすべてを、1行にひとつの事実として並べます。優先度、予算、メモリ、デバイス、割り込み、チャネル。両者がどちらの方向に食い違っても、ビルドは失敗します。

各保護ドメインにはロール（ui、input、broker、display、driver、network、security、storage、update、app、supervisor、watchdog、clock、testのいずれか）もあり、そのロールが決して持ってはならない付与は、ビルドが拒否します。ユーザーインターフェースが誤ってネットワークデバイスを渡されることはなく、テスト用の計器が製品に紛れ込むこともありません。

型付きメッセージ

保護ドメイン同士は型付きメッセージでやり取りします。明示的なレイアウトを持つ、固定サイズでバージョン付きのレコードで、共有メモリ上のシングルプロデューサー・シングルコンシューマーのリングで受け渡されます。

• コピーしてから検査。受信側は各レコードを検証する前に共有メモリからコピーするので、送り手がチェックと使用の間にそれを書き換えることはできません（ダブルフェッチと呼ばれるバグです）。
• デコーダはパニックしない。各デコーダは不正な形式のものすべてに型付きのエラーを返し、Kaniによる有界証明とファズターゲットを備えています。
• それぞれの側が、自分のビューを持つ。プロデューサーとコンシューマーは別々のメモリビューを通してリングを見ており、共有インデックスにはacquireとreleaseのメモリ順序を使います。

入力

アプリケーションが受け取るのは、正規化された入力イベント、つまりキー、ポインターの移動、タッチで、それぞれ画面と照合され、レート制限がかけられています。アプリケーションがUSBなどのデバイスプロトコルを目にすることはありません。それらは入力経路が専用の保護ドメインで解析し、すべてのバイトを敵対的なものとして扱います。

フォールト、スーパーバイザー、フェイルセーフ状態

保護ドメインがseL4の許さないことをしたり、パニックしたりすると、seL4はそれを停止させ、親にフォールトを報告します。

• スーパーバイザーは、ほかの部分の親です。各フォールトを受け取って報告し、ボードをリセットして、システムをクリーンな状態からやり直させます。スーパーバイザーは、QEMUのテストシステムでビルドされ、テストされています。
• フェイルセーフ状態は、フォールトが続いたときにデバイスが移る状態です。デフォルトでは、コールドスタートから4回目の再起動か、ストレージやアップデートのようにセキュリティ上重要な部分での2回目のフォールトで移ります。スーパーバイザー、ウォッチドッグ、そして可能であればディスプレイだけが動き続け、電源オフからのコールドスタートだけがデバイスを元に戻します。
• ウォッチドッグ保護ドメインは、ほかのすべての部分がハートビートに応答している間だけ、ハードウェアウォッチドッグをキックします。どれかが応答しなくなれば、ハードウェアがボードをリセットします。

メモリと時刻

• メモリは、イメージのビルド時に決まる。デバイスのコードは何も確保しません。すべてのバッファとキューは、nowayos-boundedによる決まったサイズを持ちます。唯一の例外であるTLSクライアントは、専用の固定アリーナの中で動きます。
• 決して混ざらない、二種類の時刻。単調時刻は起動時から数え、決して巻き戻りません。すべてのタイムアウトがこれを使います。実時刻、つまり日付と時刻は、認証されたソースから得ます。両者は別々のRustの型なので、一方を求める場所にもう一方を渡すことはできません。

自分のシステムをビルドする

あなたの製品独自のシステムと保護ドメインは、nowayosの中ではなく、その隣にある専用のリポジトリに置きます。そのリポジトリのMakefileでSYSTEM_REPO := $(CURDIR)を設定し、NoWayOSのmakeフラグメントをインクルードします。

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

これで、make image、make qemu-test、make qemu-test-all、そして各チェックが、NoWayOSの開発コンテナ、ボードファイル、付与のルール、チェックを使って、そのリポジトリのsystems/とpds/に対して動きます。変数はtools/make/system.mkの冒頭に記載されています。Showcaseは、まさにこの方法でビルドされています。