変更のたびに、自分たちのビルドを攻撃しています

どのセキュリティテストにも、居心地の悪い質問があります。そのテストは、失敗したことがありますか。一度も失敗したことのないテストが通っているのは、システムが健全だからかもしれませんし、テストに何も見えていないからかもしれません。外から見ると、この二つはまったく同じに見えます。

そこでNoWayOSは、セキュリティをテストするだけにとどめません。変更のたびに攻撃し、その攻撃が止められることを確かめます。

自分のものではないものに手を伸ばす

NoWayOSシステムの各部分は、seL4上の専用の区画で動き、付与されたものだけを持っています。隔離テストは、その境界を越えるプローブをわざと送り込みます。あるプローブは、与えられていないアドレスを読みます。あるプローブは、読み取りしか許されていないページに書き込みます。ユーザーインターフェースとまったく同じものを持つプローブは、インターフェースが読み取りしかできない、ディスプレイの制御ページに書き込もうとします。ネットワーククライアントとまったく同じものを持つ別のプローブは、ネットワークドライバのメモリに書き込もうとします。

seL4はそのすべてを止めなければならず、無関係な部分は影響を受けずに動き続けなければなりません。

失敗するように作ったテスト

ここからがひとひねりです。ユーザーインターフェースの隔離テストの横に、付与をひとつ、わざと広げた版を置いています。インターフェースの代役に、ディスプレイの非公開ページを与えるのです。この版のテストは失敗しなければなりません。もし通ってしまうなら、隔離テストには何も見えていないことになり、ビルドがそう知らせます。

同じ考え方が、ほかの検査にも通っています。部分どうしのメッセージのデコーダにはすべて、決してパニックせず、オーバーフローせず、境界外を読まないことを示す、モデル検査器Kaniによる有界証明があります。さらにミューテーション検査がデコーダをわざと壊し、証明がそれに気づくことを示します。外部からの入力のパーサーはすべて、敵対的なデータでファジングされます。

これらはすべて、あらゆる変更が通らなければならないゲート、make ciの一部です。隔離テストは毎回実行されます。証明やファジングは、対象のコードが変わるたびにやり直されます。

手の届かないゲート

ゲートの強さは、それを変更できる手の強さで決まります。そこで、NoWayOSへのすべてのコントリビューションが通らなければならない検査は、Defence Agentという独立した公開リポジトリで定義しています。ゲートに触れるプルリクエストは、メンテナーに向けて印が付けられます。

Defence Agentは、自分自身も同じ方法でテストします。仕込みのあるプルリクエストが二十件あり、それぞれにレビュアーが見落としかねないものが隠されています。コメントの中の、右から左へ書かれた隠しテキスト。そっくりなキリル文字に差し替えられた一文字。gitリポジトリから直接取得される依存関係。信頼できないコードを実行してしまうワークフロー。そのすべてが検出されなければならず、一方で、過去の実際の変更三件は通らなければなりません。

形容詞ではなく、根拠を

これらのどれも、デバイスを“ハッキング不可能”にするものではありません。そうするものは存在しませんし、私たちがそう言うこともありません。得られるのは根拠です。何が試され、何が止められたかの記録と、それを示すコマンドです。実際のイメージひとつ分の根拠、またはゲートそのものをご覧ください。