Trustのアーキテクチャ：証明可能な安全なオペレーティングシステム (PSOS) の再考

1979年、SRI InternationalのRichard J. FeiertagとPeter G. Neumannは、「The foundations of a provably secure operating system (PSOS)」を発表しました。クラウドコンピューティングや遍在するマルウェアの現代的な時代が到来する数十年前に書かれた論文ですが、その内容は、驚くほど今日でも関連性の高いオペレーティングシステムのセキュリティに関するビジョンを概説しています。PSOSの核心は、既存のカーネルにセキュリティ機能を追加することではなく、形式手法を用いてセキュリティ特性が数学的に証明可能であることを保証するために、システムをゼロから構築することにありました。

階層的開発手法 (HDM)

PSOSは、SRI Hierarchical Development Methodology (HDM) を用いて設計されました。多くのオペレーティングシステムで一般的なアドホックな開発とは異なり、HDMは、形式的に記述された要件と仕様に依存します。システムは階層的に構成されたモジュールの集合として構造化されており、各モジュールの設計はSPECIALと呼ばれる言語を使用して形式的に指定されます。

このアプローチにより、2段階の形式検証プロセスが可能になります：

仕様検証 (Specification Verification): 形式的な仕様が、望ましいセキュリティ要件を満たしていることを証明すること。
実装検証 (Implementation Verification): 実際のプログラム（ハードウェア、ファームウェア、またはソフトウェア）が、それらの仕様と一致していることを証明すること。

コアメカニズム：Capabilities

PSOSを定義付ける特徴は、capabilities の一律的な使用です。PSOSにおいて、capabilityはオブジェクトへのアクセスを許可する、偽造不可能なトークンです。プロセスがオブジェクトに対するcapabilityを持っていなければ、そのオブジェクトにアクセスすることはできません。それだけです。

Capabilityの構造

各capabilityは、2つの不変のパーツで構成されています：

Unique Identifier (UID): オブジェクトを一意に識別する、システム生成のID。
Access Rights: 許可される操作（read, write, execute, delete）を定義するBoolean配列。

執行とセキュリティ

プログラムが独自のcapabilityを偽造することを防ぐため、PSOSは tagging を採用しています。Capabilityは、プロセッサとメモリ内の、ユーザープログラムからはアクセスできないタグビットでマークされます。これにより、capabilityが改ざんされたり、何もないところから作成されたりすることを防ぎます。capabilityは、システムによって作成されるか、既存のcapabilityから restrict_access 操作を通じて派生されることしかできません。この操作は、権限を削除することはできますが、決して追加することはできません（単調性のルール）。

抽象化とType Manager

PSOSは、その機能をLevel 0 (Capabilities) からLevel 16 (User Request Interpretation) までの抽象化の階層に整理しています。これにより、システムは、原始的な物理リソース（レジスタや割り込みなど）の上に、複雑な仮想リソース（ディレクトリやユーザープロセスなど）を構築することができます。

ここでの重要な革新は、Type Manager です。Type managerは、特定のタイプのオブジェクトを担当するプログラムです。それは、capabilityのUIDを、抽象オブジェクトの実際の表現へとマッピングします。capabilityメカニズムは非常に単純で、システムの最低レベルに位置しているため、アーキテクチャのすべてのレベルで一律に使用することができ、異なる種類のシステムオブジェクトに対して専用の機能を用意する必要がなくなります。

PSOS vs. カーネルアプローチ

FeiertagとNeumannは、PSOSを、当時の他の安全なシステムで一般的だった「カーネル」アーキテクチャと比較しています。従来のカーネルアプローチでは、セキュリティポリシーを強制するために、小さく不可欠なコードの断片（カーネル）が隔離されています。

しかし、著者らは、これがしばしば「信頼されたプロセス (trusted processes)」、つまり、カーネルの外にあるものの、セキュリティに不可欠でありながら、そのようにラベル付けされていないプログラムを生じさせると主張しています。これは実際のTCB (Trusted Computing Base) を肥大化させ、検証を複雑にします。

PSOSは異なるルートを取ります。単一の、硬直的なカーネルが1つのポリシーを強制するのではなく、PSOSは、高度に拡張可能なフレームワークを提供します。それは、複数のサブシステムを作成することを可能にし、それぞれが特定のタスクのための「カーネル」として機能することで、システムが、潜在的に対立する複数のセキュリティポリシーを同時にサポートすることを可能にします。

現代的な考察：インターネット時代

PSOSは1979年当時は理論的な基盤でしたが、その哲学は現代のセキュリティ課題と共鳴しています。Hacker Newsのディスカッションのコメントにおいて、ユーザーたちは、現在の業界がアンチウイルスソフトウェア、シグネチャ、およびアプリストアの審査に依存している現状は、根本的なアーキテクチャの欠陥、すなわちcapability-based system の欠如に対する、反応的なアプローチであると指摘しています。

「1979年当時は... capability OSアーキテクチャが、無関係であったかもしれない理由は理解できます... しかし、その後、インターネット時代のように、どこからでも何かをダウンロードして実行できる時代においては、それは唯一の適切なアーキテクチャのように聞こえます... プログラムは、デフォルトで何もにもアクセス権を持たないということが。」

今日、私たちは、仮想化やコンテナ化（例：Docker）の台頭に、PSOSの哲学の反映を見ることができます。コンテナ内でプログラムを隔離することで、開発者は、数十年前のPSOSが提案したcapability-based isolation の粗いバージョンを、実質的に作成していることになります。つまり、サードパーティのパッケージにおけるマルウェアのリスクをmitigateするために、プロセスがデフォルトで「見ること」や「触れる」ことができる範囲を制限しているのです。

PSOSを再考することで、私たちは、真に安全なシステムを構築する道は、より多くのセキュリティソフトウェアを追加することではなく、セキュリティがシステム自体の固有で、証明可能な特性であるようなアーキテクチャを設計することにあるのだということを思い出させてくれます。