アプリケーションからイメージへ
NoWayOSのデバイスは、設定して作るのではなく、ビルドして作ります。四つのステップで、あなたのコードはひとつの仕事をこなすデバイスになり、各ステップには確かめられるものが残ります。
アプリケーションを書く
Rustで、ひとつ以上の保護ドメインとして書きます。画面はNoWayOSの小さな宣言的UIコアで作るか、Reactでデザインしてビルド時にScreen Compilerで変換します。
システムを記述する
Microkitのシステム記述で、すべての保護ドメイン、メモリ領域、チャネル、割り込みを宣言します。その隣に、システムが付与するものをすべて並べた付与ファイルと、実行時に出力しなければならない内容を並べた期待出力ファイルを置きます。
systems/hello.system systems/hello.grants systems/hello.expectビルドする
開発コンテナの中で行います。ビルドは付与ファイルをシステム記述と照合し、それからソフトウェア部品表とseL4構成の記録を添えてイメージを書き出します。
make image SYSTEM=hello起動して、自らチェックさせる
まずはQEMUで。システムはヘッドレスで起動し、期待出力ファイルに並ぶすべての行を順番どおりに出力しなければならず、ファイルが禁じるものは何ひとつ出力してはなりません。次にRaspberry Pi 5で、同じファイルと照合します。
make qemu-test SYSTEM=hello
封じられた区画
NoWayOSシステムの各部分（画面、入力、ネットワーク、あなたのアプリケーション）は、seL4マイクロカーネルの上で、それぞれ専用の保護ドメインとして動きます。保護ドメインは自分専用のメモリを持ち、システム記述が付与したケイパビリティだけを保持します。ケイパビリティは、ひとつの扉だけを開けるカードキーのようなものです。seL4がそれを強制するので、各部分は与えられたものにしか届かず、ある部分のバグはその部分にとどまるよう設計されています。
- スーパーバイザーは、ほかの部分のフォールトを受け取り、フォールトした部分を停止させ、システムをクリーンな状態から再起動します。フォールトが続くと、デバイスはフェイルセーフ状態に入り、コールドスタートでしか元に戻りません。
- ウォッチドッグ保護ドメインは、ほかのすべての部分がハートビートに応答している間だけ、ハードウェアウォッチドッグをキックします。
- ロールは、各部分に与えてよいものを制限します。ある部分のロールが決して持ってはならない付与、たとえば描画だけをすべき部分へのデバイスの付与は、ビルドが拒否します。
型付きメッセージ、チェックの前にコピー
保護ドメイン同士は、明示的なレイアウトを持つ、固定サイズでバージョン付きのレコードでやり取りします。レコードは、共有メモリ上のシングルプロデューサーのリングで受け渡されます。すべてのレコードはチェックの前に共有メモリからコピーされるので、送り手がチェックと使用の間にそれを書き換えることはできません。
外部からの入力を扱うパーサーはすべてファジングにかけられ、決してパニックしないように作られています。また、すべてのメッセージデコーダには、Kaniモデル検査器による有界証明があります。
ネイティブな画面、ブラウザなし
ユーザーインターフェースは小さな宣言的コアです。レイアウト、フォーカス、ヒットテストを有界のメモリで行い、Rustのライブラリembedded-graphicsで描画し、変わったところだけを描き直します。テキストはビルド時にあらかじめ描いておいたグリフアトラスから描くので、デバイスがフォントファイルを解析することはありません。アプリケーションが受け取るのはキー、ポインター、タッチのイベントだけで、USBなどのデバイスプロトコルに触れることはありません。
デザイナーはReactで作業を続けられます。Screen Compilerは、対応するサブセットに沿って書かれた画面をビルド時にRustへ変換し、サブセットの外にあるものは近似せずに拒否します。
中に入っているもの
| 領域 | NoWayOSが提供するもの |
|---|---|
| ランタイム | Microkitとrust-sel4の上で保護ドメインを組むためのパターン。フォールトした部分を停止させてシステムをクリーンに再起動し、フォールトが繰り返されればフェイルセーフ状態に入るスーパーバイザー。ウォッチドッグ |
| メッセージ | 明示的なワイヤレイアウトを持つ型付きレコードと、共有メモリ上のシングルプロデューサーのリング |
| ドライバ | ディスプレイ（QEMUのramfb、Raspberry Pi 5のフレームバッファ）、入力（virtio、USBキーボード・マウス・タブレット）、ネットワーク（virtio-net、Pi 5のEthernet）、USBホスト（xHCI）、UART、タイマー、Pi 5のファン |
| ネットワーク | smoltcp上のIPスタック（DHCPとTCPに対応し、システムが許可した接続先にだけ接続）、rustlsとRustCrypto上のTLS 1.3クライアント |
| 時刻と信頼 | 決して混ざらない別々の型としての単調時刻と実時刻、ECDSA P-256署名の検証、署名付きアップデートのレコード、健全性テストを経たハードウェア乱数源からのシード |
| ユーザーインターフェース | レイアウト、フォーカス、ヒットテストを備えた有界の宣言的UIコア、embedded-graphics上のレンダラー、あらかじめ描いたグリフアトラスとアイコン |
| ツール | 開発コンテナ、プロダクトのリポジトリがビルドに使うmakeフラグメント、付与・unsafe・ライセンス・シークレットのチェック、SBOMとリリースの根拠を作るツール、QEMUとRaspberry Piのランナー |
ハードウェア
| 場所 | 役割 |
|---|---|
| QEMU（AArch64） | すべてのシステムが、まずここで開発コンテナの中で起動し、自らの出力をチェックします |
| Raspberry Pi 5 | 誰でも買える低価格のリファレンスボード。ユーザーインターフェース、USB入力、タイマー、ウォッチドッグが、すでにこの上で動いています |
| NXP i.MX8 | ハードウェアのルート・オブ・トラストを備えた、想定している本番用ハードウェア。まだ対応していません |
NoWayOSはApple silicon（arm64）のマシンで開発しています。x86-64でも開発イメージのパッケージは固定され、レビューも済んでいますが、そこでイメージをビルドし、端から端までテストしたことはまだありません。
土台にしているもの
NoWayOSは、ほかの人々の仕事の上に立っています。そのことを明記します。seL4、Microkit、rust-sel4、seL4 Device Driver Frameworkのネットワークキュー、smoltcp、rustls、RustCrypto、そしてembedded-graphicsです。