余計なことは、しない。

外しているもの

NoWayOSのイメージに入っているのは、アプリケーション、そのアプリケーションが使うドライバ、そしてseL4マイクロカーネルです。ブラウザエンジン、ウィンドウシステム、シェル、パッケージマネージャ、ユーザーアカウントはありません。どれも最初から組み込まれていないので、悪用する対象も、パッチを当てる対象も、設定を誤る対象も、そこにはありません。NoWayOSは、不要なソフトウェアとサービスを減らすよう設計されています。仕事に必要なければ、イメージには入りません。

それがこの名前の意味です。組み込まれていないものは、悪用しようがない。これは何がないかについての言明であって、何ひとつ問題が起きないという約束ではありません。組み込まれているものには、バグがありえます。私たちが主張するのは、その量がはるかに少ないこと、そしてバグがその区画にとどまることです。

汎用システムのロックダウンは、設定によるセキュリティです。締め出された機能はまだそこにあり、ひとつのバグですべての設定がすり抜けられてしまうこともあります。NoWayOSが目指すのは、構造によるセキュリティです。その機能は、最初から存在しません。

障害の封じ込め方

• 各部分はそれぞれ専用の保護ドメインで動き、自分専用のメモリを持ち、システム記述が付与したケイパビリティだけを保持します。seL4がそれを強制します。
• すべての付与はシステムの付与ファイルに一覧化されており、記述がファイルにないものを付与していたり、その逆があったりすれば、ビルドは失敗します。付与を広げることは、セキュリティ上の変更としてレビューされます。
• 部分どうしのメッセージは固定サイズのレコードで、チェックの前に共有メモリからコピーされるため、レコードがチェックを通った後で送り手がそれを書き換えることはできません。
• 入力は、チェックされるまで敵対的なものとして扱います。外部入力を扱うすべてのパーサーはファジングにかけられ、決してパニックしないように作られています。アプリケーションが受け取るのはキー、ポインター、タッチのイベントで、デバイスプロトコルではありません。
• スーパーバイザーは、フォールトした部分を停止させ、システムをクリーンに再起動します。フォールトが繰り返されると、デバイスはコールドスタートまでフェイルセーフ状態になります。

seL4の証明が対象とするもの、しないもの

seL4は約10,000行のマイクロカーネルで、正しさとセキュリティについて機械検査された証明を持っています。この証明はまれに見る成果であり、特定のプラットフォーム上の特定の構成について成り立ちます。正確な立ち位置は次のとおりです。

NoWayOSはseL4マイクロカーネルの上で動きます。seL4は、私たちのハードウェア上の特定の構成について、正しさとセキュリティの機械検査された証明を持っています。NoWayOSが使うのはseL4の混合クリティカリティ構成で、その証明は進行中です。

• プラットフォーム：seL4のAArch64検証済み構成には、Raspberry Pi 5と、NXPのi.MX8M Mini、Plus、Quadが挙げられています。
• スケジューリング：Microkitがビルドするのは、seL4の混合クリティカリティ（MCS）カーネルで、そのAArch64向けの証明は進行中です。したがって、現時点で、seL4の完了済みの証明の範囲に入るNoWayOSイメージはありません。
• コア：証明はシングルコアのカーネルを対象としています。複数のコアを使うイメージはその範囲外であり、自らそう明記します。
• カーネルより上：Microkitのツール、そしてNoWayOSの保護ドメインとドライバは、seL4の証明の対象外です。それらの保証は、Rust、隔離、レビュー、テスト、そしてNoWayOS自身の有界証明によるものです。

すべてのイメージは、隣に置かれたsel4-config.txtに自らの構成を記録します。helloシステムの開発ビルドの記録は、自らについて次のように述べています。

system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list

カーネルが検証済み構成のすべてのオプションに一致するイメージであっても、ここでは“検証済み”とは呼びません。記録は事実を述べます。そして、事実で十分です。

根拠と、それぞれのコマンド

このページのすべての主張には根拠があり、すべての根拠は、誰でも開発コンテナで実行できるコマンドから生まれます。make ciはそれらを順番に実行し、make ci CI_SCOPE=fullはすべての証明とファズターゲットを実行します。それぞれの説明はチェックと根拠にあります。

イメージひとつ分の根拠を読む

根拠がどんなものかを見るのに、何かをビルドする必要はありません。実際のイメージひとつ分の根拠を、すべてここに置いています。クリックして操作できるユーザーインターフェースui-interactiveを、2026年11月1日にQEMU向けにビルドしたものです。

• ソフトウェア部品表（CycloneDX 1.5）：seL4カーネルとMicrokitのローダーから、すべての保護ドメインのすべてのクレートまで、62個の構成要素を、それぞれSHA-256付きで。
• seL4構成の記録：動作するカーネルを、seL4の検証済み構成とオプションごとに比べ、どこで証明の範囲外になるかをはっきり示しています。
• システム記述：Microkitがビルドするとおりの、すべての保護ドメイン、メモリ領域、割り込み、チャネル。
• 付与ファイル：同じ付与を、1行にひとつの事実として書き出したもの。ビルドがこれをシステム記述と照合します。
• このイメージが描く画面。テストが走るたびに、この承認済み画像とピクセル単位で比較されます。

あなたの側に残るもの

NoWayOSはプラットフォームであり、認証を受けた製品ではありません。デバイスが安全かどうかは、それがどう導入され、どう運用されるかにもかかっています。その部分は、デバイスを作り、運用する人の責任です。

• 物理的なセキュリティ。差し込まれたデバイスや、電源ケーブルにかかった手ひとつで、デバイスが止まることはありえます。筐体、ポート、電源は、NoWayOSの上に作られる製品の設計の一部です。
• 各システムが付与するもの。NoWayOSは、システムとその付与ファイルが一致していることをチェックします。その付与が仕事にとって正しいかどうかは設計上の判断であり、設計判断としてレビューされるべきです。
• ネットワークとバックエンド。デバイスは、システムが許可した接続先にだけ接続します。それらのサービスが受け取ったものをどう扱うかは、サービスの側で守るべきことです。
• 鍵とアップデート。安全にフォールバックできる署名付きアップデートは、設計はできていますが、まだ作られていません。誰が署名鍵を持ち、リリースをどう承認するかは、運用上の判断です。
• 認証。NoWayOSの上で動く規制対象の製品は、それぞれ独自に認証を受けます。NoWayOSは、それらが必要とする根拠を提供するよう設計されていますが、NoWayOS自体は認証を受けていません。

まだ作られていないもの

• セキュアブートとアテステーションは、ハードウェアのルート・オブ・トラストを備えた本番用ハードウェアで実現するものです。どちらもまだ作られていません。
• デバイス上で適用する署名付きアップデート。アップデートのレコードとそのチェックはありますが、デバイス上でアップデートを適用する経路は、まだありません。
• Raspberry Pi 5は開発用ボードであり、堅牢化されたデバイスではありません。手にした人はそのソフトウェアを入れ替えられますし、USBデバイスのメモリアクセスは、このボード上ではまだ制限されていません。

ここにない言葉

私たちはNoWayOSを“ハッキング不可能”“改ざん不可能”“鉄壁”とは呼びませんし、“攻撃対象領域ゼロ”とも言いません。そう言えるものなど、何ひとつありません。そう書かれていたら、そこで読むのをやめて正解です。このページの主張はそれよりずっと控えめで、どれにも根拠が付いています。

脆弱性の報告

脆弱性は、公開のissueではなく、非公開で報告してください。各リポジトリのSECURITY.mdに記載のとおり、リポジトリのSecurityタブにあるGitHubのプライベート脆弱性報告を使うか、security@nowayos.com へメールしてください。各部分はそれぞれ専用の区画で動いているので、修正が用意されるまでの間、欠陥はその場所にとどまるよう設計されています。