Separation kernel とは

分離カーネルは、分散環境をシミュレートするために使用される一種のセキュリティカーネルです。この概念は、1981年の論文でJohn Rushbyによって導入されました。 Rushbyは、「汎用マルチユーザーシステムでのマルチレベルの安全な操作を提供する」ための、大規模で複雑なセキュリティカーネルの開発と検証で生じた困難と問題の解決策として分離カーネルを提案しました。ラシュビー氏によれば、「分離カーネルの課題は、物理的に分散したシステムによって提供されるものと区別できない環境を作り出すことです。各レジームは独立した独立したマシンであるように見える必要があり、情報は1つのマシン分離カーネルの特性を証明しなければならない性質の1つは、明示的に提供されている以外のレジーム間での情報の流れのためのチャネルがないということです。
分離カーネルの変形であるパー​​ティショニングカーネルは、単一のプロセッサ上に複数の機能、おそらくは混在した重要な機能を統合する方法として、商業航空業界で受け入れられています。このジャンルの商用リアルタイムオペレーティングシステム製品は、航空機メーカーが安全に重要な航空電子工学アプリケーションに使用されています。
2007年に米国国家安全保障局(NSA)の情報保証局は、最も敵対的な脅威環境で使用するのに適した分離カーネルのセキュリティ要件仕様である分離カーネル保護プロファイル(SKPP)を公開しました。 SKPPは、Common Criteria用語で、Rushbyの概念分離カーネルの基本的な特性を提供する最新の製品群を記述しています。これは分離カーネルの構築と評価のためのセキュリティ機能と保証の要件を定義しているが、開発者が選択できる範囲にある程度の自由度を提供する。
SKPPは、分離カーネルを「複数のパーティションを確立し、分離し、分離し、これらのパーティションに割り当てられた主体とエクスポートされたリソースとの間の情報フローを制御することであるハードウェアおよび/またはファームウェアおよび/またはソフトウェア機構」と定義する。さらに、分離カーネルのコア機能要件には、
 評価対象者が使用する内部リソースの不正アクセスからのすべてのリソース(CPU、メモリ、デバイスを含む)の保護。エクスポートされたリソースからのサブジェクトの分割および分離に利用可能なセキュリティ機能(TSF)エクスポートされたリソース間の監査サービス
分離カーネルは、制御下にあるすべてのエクスポートされたリソースをパーティションに割り振ります。パーティションは、明示的に許可された情報フローを除いて分離されています。 1つのパーティション内のサブジェクトのアクションは、そのフローが許可されていない限り、別のパーティション内のサブジェクトから隔離されています(つまり、検出されなかったり、通信されたりすることはありません)。パーティションとフローは構成データで定義されます。 'partition'と 'subject'は直交抽象であることに注意してください。 'Partition'は、数学的起源によって示されるように、システム実体の集合論的グループ分けを提供するが、 'subject'は、システムの個々の活性実体について推論することを可能にする。したがって、パーティション(0個以上の要素を含むコレクション)はサブジェクト(アクティブな要素)ではなく、0個以上のサブジェクトを含むことができます。
分離カーネルは、ホストされたソフトウェアプログラムに、改ざん防止およびバイパス不可能である高保証パーティション化および情報フロー制御プロパティを提供する。これらの機能は、さまざまなシステムアーキテクチャに構成可能な信頼できる基盤を提供します。
2008年9月、Green Hills SoftwareのINTEGRITY-178BがSKPPに対して認定された最初の分離カーネルになりました。
ウインドリバーシステムズは、2009年にアクティブな認証プロセスにあった分離カーネル技術を採用しています。
2011年には、情報保証部がSKPPを改装しました。 NSAは、SKPPとの分離カーネルを含む特定のオペレーティングシステムをもはや認証することはなく、「この保護プロファイルへの適合は単独では、適合している大規模システムの状況において、国家安全保障情報が適切に保護されているという十分な確信を提供しない製品は統合されています。
seL4マイクロカーネルは分離カーネルとして構成できるという正式な証明があります。情報フロー実施の証拠は、これと一緒に、その用途のための非常に高いレベルの保証を意味する。