言葉を、やさしく。

ソフトウェア部品表のためのオープンな標準形式。NoWayOSは、すべてのワークスペースとすべてのシステムイメージについて、この形式の部品表を書き出します。SBOMも参照してください。

Raspberry PiのUSBシリアル変換アダプター。Raspberry Pi 5のデバッグ用コネクタにつなぐと、ブートログを運び、テストイメージを読み込ませます。

オペレーティングシステムのグラフィックススタックを持たないデバイス向けの、Rustの2Dグラフィックスライブラリ。NoWayOSのユーザーインターフェースは、これで描画しています。

NXPの産業用Armプロセッサのファミリーで、NoWayOSが想定している本番用ハードウェア。まだ対応していません。

Rustのためのモデル検査器で、上限までのすべての入力について性質を証明します。NoWayOSはこれを使って、メッセージデコーダが決してパニックせず、オーバーフローせず、境界外を読まないことを証明しています。

seL4 Foundationのフレームワークで、システム記述で宣言した保護ドメインから静的なseL4システムを組み立てます。

未定義動作を検出するRustのインタープリター。NoWayOSは、unsafeなコードが許されたごく少数のクレートに対してこれを実行します。

オープンソースのマシンエミュレーター。NoWayOSのすべてのシステムは、ハードウェアに触れる前に、まずこの中で起動し、自らの出力をチェックします。

NoWayOSがリファレンスハードウェアとして使っている、低価格のボード。

安全なコードであればメモリ安全性バグを排除できるプログラミング言語。NoWayOS自身のコードは、隅々までRustです。

seL4 FoundationによるRustのサポート。Microkitの保護ドメインを書くためのクレートも含まれます。

Rustで書かれたTLSライブラリ。NoWayOSのTLS 1.3クライアントは、RustCryptoとともに、これの上に作られています。

ソフトウェア部品表。ソフトウェアに含まれるすべての構成要素とバージョンの一覧です。NoWayOSは、すべてのワークスペースとすべてのシステムイメージについて、CycloneDX形式で書き出します。

NoWayOSのビルド時ツールで、対応するサブセットに沿ってTSXで書かれたReactの画面を、NoWayOSのユーザーインターフェース用のRustに変換します。サブセットの外にあるものは、近似せずに拒否します。

seL4 Device Driver Framework。共有メモリのキューを使う、Microkit上のドライバのためのリファレンス設計です。NoWayOSのネットワークキューは、これに沿っています。

seL4 Foundationが保守する約10,000行のマイクロカーネルで、特定の構成について、正しさとセキュリティの機械検査された証明を持っています。NoWayOSは、この上で動きます。

NoWayOSのすべてのイメージの隣に書き出される記録。そのイメージのseL4構成と、その構成がseL4の完了済みの証明の範囲に入っているかどうかを記します。

あるデバイスのひとつの仕事のために作られたオペレーティングシステム。何でも動かせるように作ってから、ひとつのことに絞ってロックダウンするのではありません。条件は三つです。ひとつの仕事のために作られていること（イメージにはアプリケーション、それが使うドライバ、カーネルだけが入り、ほかには何も入っていない）。内側が区画で封じられていること（各部分がそれぞれの区画に入り、許可されたものにしか届かない）。そして根拠を示すこと（中に何が入っているかの根拠が付いてくる）。設定によるセキュリティのシステムをひとつのアプリに固定するキオスクモードとは違います。NoWayOSはSingle Purpose OS、ほかにすることが何もないコンピューターです。

実行中にメモリを確保しない、Rustで書かれたTCP/IPスタック。NoWayOSのネットワークスタックは、これの上に作られています。

コンパイラがメモリ安全性をチェックできないRustのコード。NoWayOSのクレートでは、チェックが強制する短いレビュー済みの一覧に載ったものを除き、すべて禁止されています。

デバイスが、どのソフトウェアで起動したかを、暗号を用いてリモートのサービスに証明すること。示すのは起動時に何が読み込まれたかであって、その後に起きたことすべてではありません。NoWayOSでは本番用ハードウェアで計画していますが、まだ作られていません。

ソフトウェアが定期的にキックしない限り、ボードをリセットするハードウェアタイマー。NoWayOSのウォッチドッグ保護ドメインは、ほかのすべての部分がハートビートに応答している間だけ、これをキックします。

NoWayOSのツールチェーン一式を収めた、バージョン固定のコンテナイメージ。Rustのツールチェーン、Microkit SDK、QEMU、チェック用のツールが入っています。makeのすべてのターゲットがこの中で動くので、手元のマシンに必要なのはPodmanとmakeだけです（Raspberry Pi 5を操作するなら、Python 3.11も）。

付与されていないものに手を伸ばし、それをseL4が止めなければならないシステム。わざと付与を広げた変種は失敗しなければならず、それがテストに失敗する力があることを示します。

明示的なレイアウトを持つ固定サイズのレコード。共有メモリを介して保護ドメインの間で受け渡され、受信時にチェックされます。コピーしてから検査も参照してください。

systems/NAME.expect。システムが順番どおりに出力しなければならない行と、どこかに現れたらテストを失敗させるテキストを記したファイルです。同じファイルで、QEMU上のシステムも、Raspberry Pi 5上のシステムもチェックします。

ビルド時にあらかじめ文字ごとの画像として描いておいたフォント。これによりデバイスは、フォントファイルを一度も解析せずにテキストを描けます。

ソフトウェアが仕様を満たすことを、計算機で検査した数学的な証明によって示すこと。seL4は、特定の構成についてこれを備えています。NoWayOS自身のコードは、その代わりにRust、隔離、テスト、有界証明に頼っています。

seL4において、ひとつのカーネルオブジェクトと、それに対して持つ権限を指し示す、偽造できないトークン。ひとつの扉だけを開けるカードキーのようなものです。保護ドメインが触れられるのは、自らのケイパビリティが指し示すものだけです。

攻撃者がデバイスに対して利用を試みうるものすべて。コード、サービス、インターフェース、入力などです。コードが少なく、機能が少ないほど、攻撃対象領域も小さくなります。

危険なことをそもそも実行できないデバイスを作ること。それらの機能は、最初から組み込まれていないからです。NoWayOSのアプローチです。

リセットではなく、電源オフの状態からの起動。NoWayOSのデバイスをフェイルセーフ状態から戻せるのは、コールドスタートだけです。

メッセージを検証する前に共有メモリからコピーするというルール。これにより、送り手がチェックと使用の間にメッセージを書き換えることはできません。ダブルフェッチを防ぎます。

スケジューリングの予算と周期を備えたseL4の構成で、Microkitがビルドするもの。そのAArch64向けの証明は進行中のため、現時点で、seL4の完了済みの証明の範囲に入るNoWayOSイメージはありません。

システムのすべての保護ドメイン、メモリ領域、チャネル、割り込みを宣言する、MicrokitのXMLファイル。システムのセキュリティ設計そのものであり、これへの変更はセキュリティ設計の変更としてレビューされます。

認証されたソースから得る、日付と時刻。NoWayOSはこれを、別の型として単調時刻から切り離して扱います。

ほかの部分のフォールトを受け取り、報告し、システムをクリーンな状態から再起動する保護ドメイン。

デバイスが、メーカーの署名がないソフトウェアの起動を拒否すること。NoWayOSでは本番用ハードウェアで計画していますが、まだ作られていません。

汎用デバイスを、設定を変えることでより安全にすること。機能はまだそこにあり、ひとつのバグですべての設定がすり抜けられてしまうこともあります。

共有メモリ上のデータをチェックした後に、コードがもう一度それを読み込むバグ。その間に相手側がデータを書き換えられてしまいます。コピーしてから検査で防ぎます。

起動時から数える時刻。設定されることも、巻き戻ることもありません。NoWayOSのすべてのタイムアウトはこれを使い、実時刻と混ざることはありません。

Microkitにおいて、二つの保護ドメインの間に宣言された接続。通知（データを持たないシグナル。割り込みもそのひとつ）と、保護された手続き呼び出しに使います。

あるセキュリティ上の性質が、正しく動くことを前提にしているものすべて。NoWayOSのシステムでは、seL4カーネル、Microkitのローダーとモニター、そしてその性質が依存する保護ドメインです。

生成した何百万もの入力をパーサーに与え、クラッシュやチェック違反を起こすものを探すテスト。外部入力を扱うNoWayOSのパーサーには、すべてファズターゲットがあります。

フォールトが続いたときに、NoWayOSのデバイスが移る状態。コールドスタートまで、スーパーバイザー、ウォッチドッグ、そして可能であればディスプレイだけが動き続けます。

保護ドメインがカーネルの許さないことをしたとき、またはパニックしたときに、seL4が報告するもの。その部分は、フォールトハンドラが対処するまで停止したままです。

systems/NAME.grants。システムが付与するもののすべてを、1行にひとつの事実として記したファイルです。優先度、予算、メモリ、デバイス、割り込み、チャネル。システム記述と付与ファイルが食い違えば、ビルドは失敗します。

Microkitシステムを構成する、隔離された部分のひとつ。自分専用のメモリを持ち、明示的に付与されたケイパビリティだけを保持するプログラムです。NoWayOSの「封じられた区画」にあたります。

できるかぎり小さく保ったカーネル。ドライバ、ネットワーク、画面はその外で、それぞれ専用の区画で動きます。seL4はそのひとつです。

バッファの終端を越えて読む、解放済みのメモリを使うといった誤り。MicrosoftとGoogleはそれぞれ、深刻なセキュリティバグのおよそ70%がこの種のものだと報告しています。安全なRustのコードでは、これらは起こりえません。

ある性質が、定められたサイズまでのすべての入力について成り立つことの証明。NoWayOSは、メッセージデコーダをこの方法で、Kaniを使って証明しています。