チェックと根拠

NoWayOSの主張は多くありません。そして、そのひとつひとつを、実行できるチェックで裏付けています。このページでは、各チェックが何を示し、何を示さないかを説明します。

すべてをひとつのコマンドで

make ci

make ciはゲート全体で、次の順に実行します。シークレットのスキャン、リント、テスト、ドキュメント、デモ、no_stdビルド、ライセンスとアドバイザリのチェック、グリフアトラス、部品表、ファジングとKaniの証明、そしてシステムのチェックとQEMUでの起動。すべてのステップが通ったときにだけ、変更は合格します。

各チェックが示すもの

有界証明は、定められたサイズまでの入力についての証明であって、ありうるすべての入力についての証明ではありません。ファジングはクラッシュを見つけますが、クラッシュがないことは示せません。テストが示すのは、テストしたケースだけです。どれも、それが示せることのために、持つ価値があります。

すべてのクレートが守る基本ルール

これらはガイドラインではなく、すべてのワークスペースにあるリントとチェックです。

• unsafeは使わない。例外は、ハードウェアやメモリに直接触れる、承認済みの短いクレートとファイルの一覧だけです。一覧への追加には、理由の明記とレビューが必要です。
• 外部入力でパニックしない。ライブラリのコードにunwrap、expect、panic!はなく、チェックなしのインデックスや算術もありません。リントの例外には、すべて理由が書かれています。
• デバイス用クレートはno_stdで、何も確保しない。リリースビルドでもオーバーフローチェックを残し、パニックしたら、そのまま続けるのではなく、その部分を止めます。
• パーサーは、大きすぎる入力をコピーする前に拒否する。型付きのエラーを返し、プロパティテストとファズターゲットを備えています。
• シークレットは、どこにも置かない。開発用の鍵でさえも。テスト用の鍵はテストの実行時に作り、保存はしません。

イメージの記録を読む

すべてのイメージはbuild/BOARD/SYSTEM/に書き出され、その隣に二つの記録が置かれます。

sel4-config.txt は、イメージの名前、ハッシュ、ボード、Microkit SDK、カーネルを記した後、そのイメージがseL4の証明に対してどこに位置するかを、理由ごとに1行のstatus:で述べます。そして、その判断を左右する各カーネルオプションを、検証済み構成の値と並べて一覧にします。デバッグカーネルは開発ビルドです。マルチコアや混合クリティカリティのカーネル、あるいはseL4の一覧にないボードは、seL4の証明の範囲外です。すべてのオプションが一致するカーネルであっても、決して“検証済み”とは呼びません。記録は事実を示し、そこで終わります。

sbom.cdx.json は、イメージのCycloneDX形式のソフトウェア部品表です。何からできているかを、各保護ドメインの各クレートに至るまで、それぞれsha256付きで記します。

ゲートを速く保つ

証明とファジングをすべて行うと長い時間がかかるので、日常のmake ciは、Kani、ファジング、Miriを、変更が及ぶところだけで実行します。変更を、それに依存するすべてのクレートまでたどり、前回合格してから入力が変わっていないチェックは飛ばします。make ci CI_SCOPE=fullは、キャッシュを使わずにそれらすべてを実行します。make kani、make fuzz、make pds-miriは、常に全体を実行します。

Kaniは、最もメモリを食うステップです。証明ジョブにはそれぞれ約10 GBのメモリが割り当てられ、KANI_JOBSで同時に実行する数を設定します。make kaniでメモリが足りなくなったら、Podmanの仮想マシンにもっとメモリを割り当てるか、KANI_JOBS=1を設定してください。