分離カーネル

分離カーネルは、分散環境をシミュレートするために使用されるセキュリティカーネルの一種です。この概念は、1981 年の論文でJohn Rushbyによって導入されました。 ^[1] Rushby は、"汎用マルチユーザー システムでマルチレベルの安全な操作を提供する" ことを目的とした大規模で複雑なセキュリティ カーネルの開発と検証で発生した困難と問題の解決策として、分離カーネルを提案しました。Rushby によると、"分離カーネルのタスクは、物理的に分散されたシステムによって提供される環境と区別がつかない環境を作成することです。つまり、各レジ​​ームが別個の隔離されたマシンであるかのように見え、情報は既知の外部通信回線に沿って 1 つのマシンから別のマシンにのみ流れる必要があります。したがって、分離カーネルについて証明しなければならない特性の 1 つは、明示的に提供されるもの以外にレジーム間の情報フローのチャネルが存在しないことです。"

分離カーネルの変形であるパー​​ティショニング カーネルは、複数の機能を混合クリティカルな単一のプロセッサに統合する方法として、民間航空業界で受け入れられています。このジャンルの商用リアルタイム オペレーティング システム製品は、航空機メーカーによって安全性が重要な航空電子機器アプリケーションに 使用されています。

2007 年に米国国家安全保障局(NSA) の情報保証局は、最も過酷な脅威環境で使用するのに適した分離カーネルのセキュリティ要件仕様である分離カーネル保護プロファイル (SKPP) ^{[2]を公開しました。SKPP は、} Common Criteria ^[3]の用語で、Rushby の概念的な分離カーネルの基本特性を提供する最新の製品のクラスを説明しています。SKPP は、分離カーネルの構築と評価に関するセキュリティ機能と保証の要件を定義しながら、開発者に利用可能な選択肢に一定の自由度を提供します。

SKPP では、分離カーネルを「複数のパーティションを確立、分離、分離し、それらのパーティションに割り当てられたサブジェクトとエクスポートされたリソース間の情報フローを制御することを主な機能とするハ​​ードウェア、ファームウェア、ソフトウェア メカニズム」と定義しています。さらに、分離カーネルのコア機能要件には次のものが含まれます。

• すべてのリソース（CPU、メモリ、デバイスを含む）を不正アクセスから保護します。
• 評価対象セキュリティ機能 (TSF) によって使用される内部リソースを、サブジェクトが利用できるようにエクスポートされたリソースから分離します。
• エクスポートされたリソースのパーティション分割と分離。
• パーティション間およびエクスポートされたリソース間の情報フローの仲介。
• 監査サービス。

分離カーネルは、その制御下にあるすべてのエクスポートされたリソースをパーティションに割り当てます。パーティションは、明示的に許可された情報フローを除いて分離されています。あるパーティション内のサブジェクトのアクションは、そのフローが許可されていない限り、別のパーティション内のサブジェクトから分離されます (つまり、別のパーティション内のサブジェクトによって検出または通信されることはありません)。パーティションとフローは、構成データで定義されます。「パーティション」と「サブジェクト」は直交する抽象概念であることに注意してください。「パーティション」は、その数学的な起源が示すように、システムエンティティの集合論的グループ化を提供しますが、「サブジェクト」は、システムの個々のアクティブエンティティについて推論できるようにします。したがって、パーティション (0 個以上の要素を含むコレクション) はサブジェクト (アクティブ要素) ではありませんが、0 個以上のサブジェクトを含むことができます。^[2] 分離カーネルは、ホストされたソフトウェアプログラムに、改ざん防止とバイパス不可能の両方を備えた高保証のパーティション分割と情報フロー制御プロパティを提供します。これらの機能は、さまざまなシステムアーキテクチャに構成可能な信頼できる基盤を提供します。^[2]

• PikeOS は、分離カーネル ハイパーバイザー テクノロジーとハードリアルタイム機能を組み合わせています。
• Green Hills SoftwareのINTEGRITY-178Bは2008年9月にSKPPに対して認定された最初の分離カーネルとなった。^[4]
• Wind River Systems は、2009 年に認証プロセスが進行中だった分離カーネル テクノロジを持っています。
• Lynx Software Technologies には、分離カーネルLynxSecureがあります。

2011年、情報保証局はSKPPを廃止しました。NSAは、分離カーネルを含む特定のオペレーティングシステムをSKPPに対して認証しなくなり、「この保護プロファイルへの適合だけでは、適合製品が統合されている大規模システムのコンテキストで国家安全保障情報が適切に保護されているという十分な信頼性が得られない」と述べています。^[5]

seL4マイクロカーネルは、分離カーネルとして構成できるという正式な概念実証を持っています。^[6]強制的な情報の継続^[7]は、これが高度な保証の例であることを意味します。Muen ^[8]分離カーネルも、x86マシン用の正式に検証されたオープンソースの分離カーネルです。

• 分離カーネルに基づくコンピュータ セキュリティ アーキテクチャについては、「複数の独立したセキュリティ レベル」を参照してください。
• クルート
• FreeBSD 刑務所
• オペレーティング システム レベルの仮想化