Loading article…
コンピュータ科学において、マイクロカーネル（しばしばμカーネルと略される）とは、オペレーティングシステム（OS）を実装するために必要なメカニズムを提供する、ほぼ最小限のソフトウェアのことである。これらのメカニズムには、低レベルのアドレス空間管理、スレッド管理、およびプロセス間通信（IPC）が含まれる。
ハードウェアが複数のリングまたはCPU モードを提供する場合、マイクロカーネルは最も特権的なレベルで実行される唯一のソフトウェアとなる可能性があり、これは一般的にスーパーバイザモードまたはカーネルモードと呼ばれます。デバイスドライバ、プロトコルスタック、ファイルシステムなどの従来のオペレーティングシステム機能は、通常マイクロカーネルから分離され、代わりにユーザー空間で実行されます。[ 1 ]
マイクロカーネルは、モノリシックカーネルよりもソースコードが少ないことが多い。例えば、MINIX 3マイクロカーネルは、約 12,000 行のコードしかない。 [ 2 ]
マイクロカーネルの起源は、デンマークのコンピュータのパイオニアであるペル・ブリンチ・ハンセンと、彼がデンマークのコンピュータ会社Regnecentralenに在籍していた時期に遡ります。彼はそこでRC 4000コンピュータのソフトウェア開発を主導しました。[ 3 ] 1967年、RegnecentralenはポーランドのZakłady Azotowe Puławy肥料工場にRC 4000のプロトタイプを設置していました。このコンピュータは、工場のニーズに合わせて調整された小型のリアルタイムオペレーティングシステムを使用していました。ブリンチ・ハンセンと彼のチームは、RC 4000システムの汎用性と再利用性の欠如を懸念していました。彼らは、設置ごとに異なるオペレーティングシステムが必要になることを恐れ、RC 4000用のソフトウェアを作成するための斬新でより汎用的な方法を研究しました。[ 4 ] 1969年、彼らの努力はRC 4000マルチプログラミングシステム の完成につながりました。その中核は、最大 23 個の非特権プロセスに対してメッセージ パッシングに基づくプロセス間通信を提供し、そのうち 8 個は同時に互いに保護されていた。さらに、並列実行されるプログラムのタイム スライスのスケジューリング、他の実行中のプログラムからの要求によるプログラム実行の開始と制御、周辺機器との間のデータ転送の開始を実装した。これらの基本的なメカニズムの他に、プログラム実行とリソース割り当てのための組み込みの戦略はなかった。この戦略は、親プロセスが子プロセスを完全に制御し、子プロセスのオペレーティングシステムとして機能する実行プログラムの階層によって実装されることになっていた。[ 5 ] [ 6 ]
ブリンチ・ハンセンの研究に続き、マイクロカーネルは1970年代から開発されてきた。[ 7 ]マイクロカーネルという用語自体は、遅くとも1981年には初めて登場した。[ 8 ]マイクロカーネルは、コンピュータの世界の変化と、既存の「モノカーネル」をこれらの新しいシステムに適合させる際のいくつかの課題への対応として考案された。新しいデバイスドライバ、プロトコルスタック、ファイルシステム、その他の低レベルシステムが常に開発されていた。これらのコードは通常、モノリシックカーネルに配置されていたため、作業には相当な労力と慎重なコード管理が必要だった。マイクロカーネルは、これらのサービスすべてを他のプログラムと同様にユーザー空間プログラムとして実装し、モノリシックに作業して他のプログラムと同様に起動および停止できるようにするという考えに基づいて開発された。これにより、これらのサービスをより簡単に作業できるだけでなく、カーネルコードを分離して、意図しない副作用を心配することなく細かく調整することも可能になる。さらに、共通のコア上にまったく新しいオペレーティングシステムを「構築」できるようになり、OSの研究に役立つ。
マイクロカーネルは、最初の実用的なローカルエリアネットワークが導入された1980年代に話題になりました。 [ 9 ] AmigaOS Execカーネルは初期の例で、1986年に導入され、比較的商業的に成功したPCで使用されました。他の点では欠点と考えられていたメモリ保護の欠如により、このカーネルはユーザー空間プログラム間でメッセージを交換する際にデータをコピーする必要がなかったため、高いメッセージパッシング性能を実現できました。[ 10 ]
カーネルをユーザー空間に分散させることを可能にしたのと同じメカニズムにより、システムをネットワークリンク全体に分散させることも可能になった。リチャード・ラシッドによって作成された最初のマイクロカーネル、特にMachは、期待外れのパフォーマンスであることが判明したが、その本質的な利点は非常に大きいように見えたため、1990年代後半まで主要な研究分野となった。[ 11 ]しかし、この間にコンピュータの速度はネットワークシステムに比べて大幅に向上し、パフォーマンスの欠点が開発上の利点を上回るようになった。
既存システムのパフォーマンス向上を目指した多くの試みがなされたが、オーバーヘッドは常に相当なものであり、これらの取り組みのほとんどはユーザー空間プログラムをカーネルに戻す必要があった。2000年までに、大規模なMachカーネル開発の取り組みはほぼ終了したが、2001年にリリースされたAppleのmacOSは、依然としてXNUと呼ばれるハイブリッドカーネルを使用している。XNUは、大幅に改変された（ハイブリッド）OSF/1のMachカーネル（OSF MK 7.3カーネル）とBSD UNIXのコードを組み合わせたものである。[ 12 ] [ 13 ]このカーネルはiOS、tvOS、watchOSでも使用されている。Windows NTは、 NT 3.1からWindows 11まで、ハイブリッドカーネル設計を採用している。2012年現在Mach ベースのGNU Hurdも機能しており、 Arch LinuxとDebianのテスト版に含まれています。
マイクロカーネルに関する主要な研究はほぼ終了していたものの、実験者たちは開発を続けた。[ 14 ] [ 15 ]アセンブリコードを含め、通常ソフトウェアでサポートされる概念をプロセッサに強制させるという、より実用的なアプローチを採用した結果、パフォーマンスが劇的に向上した新しいマイクロカーネルシリーズが誕生した。
マイクロカーネルはエクソカーネルと密接に関連しています。[ 16 ]また、ハイパーバイザとも多くの共通点がありますが、[ 17 ]後者は最小性を主張せず、仮想マシンをサポートすることに特化しています。L4マイクロカーネルはハイパーバイザ機能でよく使用されます。
初期のオペレーティングシステムカーネルは、コンピュータのメモリ容量が限られていたこともあり、比較的小型でした。コンピュータの性能が向上するにつれて、カーネルが制御しなければならないデバイスの数も増加しました。Unixの初期の歴史を通して、カーネルは様々なデバイスドライバやファイルシステムの実装を含んでいたにもかかわらず、概して小型でした。アドレス空間が16ビットから32ビットに拡大すると、カーネル設計はハードウェアアーキテクチャの制約を受けなくなり、カーネルは大型化していきました。
UnixのBerkeley Software Distribution（BSD）は、より大規模なカーネルの時代を切り開きました。BSDは、CPU、ディスク、プリンタからなる基本システムを動作させるだけでなく、完全なTCP/IPネットワークシステムと、既存のプログラムがネットワーク上で「目に見えない」形で動作できるようにする多数の「仮想」デバイスを追加しました。この成長は何年も続き、数百万行のソースコードを持つカーネルが誕生しました。この成長の結果、カーネルはバグが発生しやすくなり、保守がますます困難になりました。
マイクロカーネルは、カーネルの肥大化とそれに伴う様々な問題に対処するために開発されました。理論的には、マイクロカーネル設計では、コードをユーザー空間サービスに分割することで、コード管理が容易になります。また、カーネルモードで実行されるコード量が減少するため、セキュリティと安定性の向上にもつながります。例えば、バッファオーバーフローによってネットワークサービスがクラッシュした場合でも、破損するのはネットワークサービスのメモリのみであり、システムの残りの部分は正常に動作します。
プロセス間通信（IPC）とは、通常はメッセージの送受信によって、別々のプロセスが互いに通信できるようにするあらゆるメカニズムのことです。厳密に言えば、共有メモリもプロセス間通信メカニズムですが、IPCという略語は通常メッセージパッシングのみを指し、マイクロカーネルにとって特に重要なのは後者です。IPCによって、オペレーティングシステムは、システム上の他のプログラムがIPCを介して呼び出して使用する、サーバと呼ばれる多数の小さなプログラムから構築されます。周辺機器のサポートのほとんどすべては、デバイスドライバ、ネットワークプロトコルスタック、ファイルシステム、グラフィックスなどのためのサーバによって、この方法で処理されます。
IPC は同期または非同期で行うことができます。非同期 IPC はネットワーク通信に似ています。送信側はメッセージを送信し、実行を継続します。受信側はメッセージの可用性を確認 (ポーリング) するか、何らかの通知メカニズムによって通知を受け取ります。非同期 IPC では、カーネルがメッセージのバッファとキューを維持し、バッファオーバーフローを処理する必要があります。また、メッセージの二重コピー (送信側からカーネル、カーネルから受信側) も必要です。同期 IPC では、最初の当事者 (送信側または受信側) は、相手側が IPC を実行する準備ができるまでブロックします。バッファリングや複数コピーは必要ありませんが、暗黙のランデブーによりプログラミングが複雑になる場合があります。ほとんどのプログラマは、非同期送信と同期受信を好みます。
第一世代のマイクロカーネルは、同期IPCと非同期IPCの両方をサポートしていましたが、IPCのパフォーマンスが低かったのが問題でした。ヨッヘン・リートケは、このパフォーマンスの低さの根本的な原因はIPCメカニズムの設計と実装にあると考えました。彼は自身のL4マイクロカーネルで、IPCコストを桁違いに削減する手法を開拓しました。[ 18 ]これには、送信と受信の両方の操作をサポートするIPCシステムコール、すべてのIPCを同期化すること、そして可能な限り多くのデータをレジスタで渡すことなどが含まれます。さらに、リートケは直接プロセススイッチの概念を導入しました。これは、IPC実行中に（不完全な）コンテキストスイッチが送信者から受信者に直接実行されるというものです。L4のように、メッセージの一部または全部がレジスタで渡される場合、この方法ではメッセージのレジスタ内の部分がコピーされることなく転送されます。さらに、スケジューラの呼び出しのオーバーヘッドが回避されます。これは、クライアントがサーバーを呼び出すリモートプロシージャコール（RPC）タイプの方法でIPCを使用する一般的なケースで特に有益です。もう一つの最適化手法である遅延スケジューリングは、IPC中にブロックするスレッドを準備完了キューに残すことで、IPC中のスケジューリングキューの走査を回避します。スケジューラが呼び出されると、そのようなスレッドは適切な待機キューに移動します。多くの場合、スレッドは次のスケジューラ呼び出し前にブロックが解除されるため、このアプローチは大幅な処理削減につながります。同様のアプローチは、その後QNXやMINIX 3にも採用されています。
一連の実験で、Chen と Bershad は、モノリシックUltrixの命令あたりのメモリ サイクル(MCPI) を、ユーザー スペースで実行される4.3BSD Unixサーバーと組み合わせたマイクロ カーネルMachの MCPI と比較しました。彼らの結果は、MCPI が高いことで Mach のパフォーマンスが劣っていることを説明し、IPC だけではシステム オーバーヘッドの大部分の原因ではないことを実証し、IPC のみに焦点を当てた最適化の効果は限定的であることを示唆しました。[ 19 ] Liedtke は後に、Ultrix と Mach の MCPI の差の大部分は容量キャッシュ ミスによるものであるという観察を行い、マイクロ カーネルのキャッシュ ワーキング セットを大幅に削減すれば問題が解決すると結論付け、Chen と Bershad の結果をさらに改良しました。[ 20 ]
クライアント/サーバシステムでは、非同期プリミティブを使用する場合でも、ほとんどの通信は基本的に同期です。これは、典型的な操作がクライアントがサーバを呼び出し、応答を待つというものであるためです。また、より効率的な実装にも適しているため、ほとんどのマイクロカーネルは一般的にL4の方式に倣い、同期IPCプリミティブのみを提供していました。非同期IPCは、ヘルパースレッドを使用することでその上に実装できます。しかし、経験上、同期IPCの有用性は疑わしいことがわかっています。同期IPCは、そうでなければ単純なシステムにマルチスレッド設計を強制し、結果として同期の複雑さを招きます。さらに、RPCのようなサーバ呼び出しはクライアントとサーバを順次実行するため、別々のコアで実行している場合は避けるべきです。そのため、商用製品に展開されているL4のバージョンでは、非同期通信をより適切にサポートするために、非同期通知メカニズムを追加する必要があることがわかりました。このシグナルのようなメカニズムはデータを伝送しないため、カーネルによるバッファリングは不要です。しかし、2種類のIPC形式を持つことで、最小性の原則に違反しています。L4の他のバージョンでは、非同期IPCに完全に切り替えています。[ 21 ]
同期IPCは、相手側が準備できるまで最初の側をブロックするため、無制限に使用するとデッドロックが発生しやすくなります。さらに、クライアントはリクエストを送信して応答を受信しようとしないことで、サーバーに対してサービス拒否攻撃を容易に仕掛けることができます。したがって、同期IPCは無期限のブロックを防ぐ手段を提供する必要があります。多くのマイクロカーネルは、IPC呼び出しにタイムアウトを設定し、ブロック時間を制限しています。実際には、適切なタイムアウト値を選択するのは難しく、システムはほぼ必然的にクライアントに対しては無限のタイムアウト、サーバーに対してはゼロのタイムアウトを使用します。その結果、任意のタイムアウトを提供するのではなく、パートナーが準備できていない場合にIPCがすぐに失敗することを示すフラグのみを提供する方向に向かっています。このアプローチは、実質的にゼロと無限の2つのタイムアウト値を選択できることを意味します。最近のバージョンのL4とMINIXはこの方向で進んでいます（古いバージョンのL4はタイムアウトを使用していました）。QNXは、クライアントがメッセージ送信呼び出しの一部として応答バッファを指定することを要求することで、この問題を回避しています。サーバーが応答すると、カーネルはクライアントが明示的に応答を受信するのを待つことなく、データをクライアントのバッファにコピーします。[ 22 ]
マイクロカーネルサーバーは、基本的に他のデーモンプログラムと同様ですが、カーネルが一部のサーバーに、通常はほとんどのプログラムがアクセスできない物理メモリの一部とやり取りするための権限を付与している点が異なります。これにより、特にデバイスドライバなどの一部のサーバーは、ハードウェアと直接やり取りすることが可能になります。
汎用マイクロカーネルの基本的なサーバー群には、ファイルシステムサーバー、デバイスドライバサーバー、ネットワークサーバー、ディスプレイサーバー、およびユーザーインターフェースデバイスサーバーが含まれます。このサーバー群（QNXから派生したもの）は、Unixのモノリシックカーネルが提供するサービス群とほぼ同等の機能を提供します。必要なサーバーはシステム起動時に起動され、ファイル、ネットワーク、デバイスへのアクセスなどのサービスを通常のアプリケーションプログラムに提供します。このようなサーバーがユーザーアプリケーションの環境で動作するため、サーバー開発はカーネル開発に必要なビルドとブートのプロセスではなく、通常のアプリケーション開発と同様のプロセスで行えます。
さらに、多くの「クラッシュ」は、サーバーを停止して再起動するだけで修正できますが、カーネル全体を再起動する必要がある場合は、これは実現不可能です。ただし、障害が発生したサーバーではシステム状態の一部が失われるため、このアプローチではアプリケーションが障害に対処する必要があります。TCP /IP接続を担当するサーバーが良い例です。このサーバーが再起動されると、アプリケーションは「切断」された接続を経験しますが、これはネットワークシステムでは通常のことです。他のサービスでは、障害はあまり想定されておらず、アプリケーションコードの変更が必要になる場合があります。QNXでは、再起動機能はQNX高可用性ツールキットとして提供されています。[ 23 ]
デバイスドライバは頻繁にダイレクトメモリアクセス（DMA）を実行するため、カーネルの様々なデータ構造を含む物理メモリの任意の場所に書き込むことができます。そのため、このようなドライバは信頼できるものでなければなりません。しかし、ドライバがカーネルの一部でなければならないという誤解がよくあります。実際には、ドライバがカーネルの一部であるかどうかによって、信頼性が本質的に高くなる、あるいは低くなるわけではありません。
デバイスドライバをユーザー空間で実行しても、不正なドライバが引き起こす損害が必ずしも軽減されるわけではありませんが、実際には、バグのある（悪意のあるものではない）ドライバが存在する場合のシステム安定性には有益です。ドライバコードによるメモリアクセス違反（デバイスによる違反ではなく）は、メモリ管理ハードウェアによって検出される可能性があります。さらに、多くのデバイスはDMAに対応していません。そのため、ドライバをユーザー空間で実行することで、ドライバを信頼できないものにすることができます。最近では、IOMMUを搭載したコンピュータが増えており、その多くはデバイスの物理メモリへのアクセスを制限するために使用できます。[ 24 ]これにより、ユーザーモードドライバも信頼できないものになります。
ユーザーモードドライバは実際にはマイクロカーネルよりも前から存在していました。 1967年にミシガン端末システム（MTS）は、その機能を備えて設計された最初のオペレーティングシステムとして、ユーザー空間ドライバ（ファイルシステムサポートを含む）をサポートしました。[ 25 ]歴史的に見ると、デバイスの数が少なく、いずれにせよ信頼できるものであったため、ドライバはそれほど問題ではありませんでした。そのため、カーネルにドライバを含めることで設計が簡素化され、潜在的なパフォーマンスの問題を回避できました。これが、Unix、[ 26 ] Linux、およびWindows NTの伝統的なカーネル内ドライバスタイルにつながりました。さまざまな種類の周辺機器が普及するにつれて、ドライバコードの量は増加し、現代のオペレーティングシステムではコードサイズでカーネルの大部分を占めるようになりました。
マイクロカーネルは、その上に任意のオペレーティングシステムサービスを構築できるようにする必要があるため、いくつかのコア機能を提供しなければなりません。最低限、これには以下が含まれます。
この最小限の設計は、ブリンチ・ハンセンのNucleusとIBMのVMのハイパーバイザによって先駆的に導入された。その後、リートケの最小性原理として体系化された。
マイクロカーネル内で概念が許容されるのは、それをカーネルの外に移動させる、つまり競合する実装を許可すると、システムの要求される機能の実装が妨げられる場合に限られる。[ 20 ]
その他の処理はすべてユーザーモードプログラムで実行できますが、一部のプロセッサアーキテクチャでは、ユーザープログラムとして実装されたデバイスドライバは、I/Oハードウェアにアクセスするために特別な権限を必要とする場合があります。
最小性原則に関連して、マイクロカーネル設計においても同様に重要なのは、メカニズムとポリシーの分離であり、これにより最小限のカーネル上に任意のシステムを構築することが可能になります。カーネルに組み込まれたポリシーはユーザーレベルで上書きできないため、マイクロカーネルの汎用性が制限されます。[ 16 ]ユーザーレベルのサーバーで実装されたポリシーは、サーバーを交換することによって変更できます（または、アプリケーションが同様のサービスを提供する競合するサーバーから選択できるようにします）。
効率化のため、ほとんどのマイクロカーネルはスケジューラを含み、タイマーを管理しているが、これは最小性原則およびポリシー・メカニズム分離原則に違反している。
マイクロカーネルベースのシステムの起動（ブート）には、カーネルの一部ではないデバイスドライバが必要です。通常、これは、ドライバがブートイメージ内のカーネルに同梱され、カーネルがドライバの場所と起動方法を定義するブートストラッププロトコルをサポートすることを意味します。これが、 L4マイクロカーネルの従来のブートストラップ手順です。LynxOSやオリジナルのMinixなどの一部のマイクロカーネルは、（最小性の原則に反して）一部の重要なドライバをカーネル内に配置することでこれを簡素化しています。ブートを簡素化するために、カーネル内にファイルシステムを含めるものさえあります。マイクロカーネルベースのシステムは、マルチブート互換のブートローダーを介して起動できます。このようなシステムは通常、静的にリンクされたサーバーをロードして初期ブートストラップを実行するか、OSイメージをマウントしてブートストラップを継続します。
マイクロカーネルの重要な構成要素は、ページフォールト処理とユーザーモードサーバにおけるスワッピングを安全に実装できる、優れたIPCシステムと仮想メモリマネージャの設計です。すべてのサービスはユーザーモードプログラムによって実行されるため、プログラム間の効率的な通信手段は、モノリシックカーネルの場合よりもはるかに重要です。IPCシステムの設計は、マイクロカーネルの成否を左右します。効果的なIPCシステムを実現するには、オーバーヘッドが低いだけでなく、CPUスケジューリングとの連携も良好でなければなりません。
ほとんどの主流プロセッサでは、マイクロカーネルベースのシステムでは、モノリシックシステムよりもサービスを取得するコストが本質的に高くなります。[ 16 ]モノリシックシステムでは、サービスは単一のシステムコールによって取得され、2 つのモードスイッチ(プロセッサのリングモードまたはCPU モードの変更) が必要です。マイクロカーネルベースのシステムでは、IPC メッセージをサーバーに送信し、サーバーから別の IPC メッセージで結果を取得することによってサービスを取得します。ドライバがプロセスとして実装されている場合はコンテキストスイッチが必要であり、プロシージャとして実装されている場合は関数呼び出しが必要です。さらに、実際のデータをサーバーに渡してサーバーから返すと、余分なコピーのオーバーヘッドが発生する可能性がありますが、モノリシックシステムではカーネルがクライアントのバッファ内のデータに直接アクセスできます。
そのため、マイクロカーネルシステムではパフォーマンスが潜在的な問題となり、MachやChorusOSなどの第一世代のマイクロカーネルは実際にパフォーマンスが低かった。[ 19 ]しかし、Jochen Liedtkeは、Machのパフォーマンスの問題は設計と実装の不備、特にMachの過剰なキャッシュフットプリントに起因することを示した。[ 20 ] Liedtkeは、自身のL4マイクロカーネルで、慎重な設計と実装、特に最小性の原則に従うことで、IPCコストをMachと比較して1桁以上削減できることを示した。L4のIPCパフォーマンスは、さまざまなアーキテクチャで依然として破られていない。[ 27 ] [ 28 ] [ 29 ]
これらの結果は、第一世代マイクロカーネルに基づくシステムの低パフォーマンスが、L4 などの第二世代カーネルを代表するものではないことを示していますが、これはマイクロカーネルベースのシステムが優れたパフォーマンスで構築できるという証明にはなりません。モノリシックな Linux サーバーを L4 に移植した場合、ネイティブ Linux に比べてオーバーヘッドがわずか数パーセントであることは示されています。[ 30 ]しかし、このような単一サーバーシステムでは、オペレーティングシステムの機能を個別のサーバーに構造化することでマイクロカーネルが提供するとされる利点はほとんど、あるいは全く得られません。
商用マルチサーバーシステムは数多く存在し、特にリアルタイムシステムであるQNXとIntegrityが挙げられる。これらのマルチサーバーシステムについて、モノリシックシステムに対するパフォーマンスの包括的な比較は発表されていない。さらに、これらの商用システムではパフォーマンスが最優先事項ではないようで、代わりに信頼性の高い高速割り込み処理応答時間（QNX）と堅牢性のためのシンプルさが重視されている。高性能マルチサーバーオペレーティングシステムを構築しようとした試みとして、IBM Sawmill Linuxプロジェクトがあった。[ 31 ]しかし、このプロジェクトは完了しなかった。
その一方で、ユーザーレベルのデバイスドライバは、ギガビットイーサネットのような高スループット、高割り込みデバイスであっても、カーネル内ドライバのパフォーマンスに匹敵することが示されています。[ 32 ]これは、高性能マルチサーバシステムが可能であることを示唆しているようです。
マイクロカーネルのセキュリティ上の利点については、これまで頻繁に議論されてきた。[ 33 ] [ 34 ]セキュリティの観点から見ると、マイクロカーネルの最小性原則は、最小特権の原則の直接的な結果であると主張する人もいる。最小特権の原則によれば、すべてのコードは、必要な機能を提供するために必要な特権のみを持つべきである。最小性では、システムの信頼できるコンピューティングベース（TCB）を最小限に保つ必要がある。カーネル（ハードウェアの特権モードで実行されるコード）は、検証されていないデータへのアクセス権限を持ち、データの完全性や機密性を侵害する可能性があるため、カーネルは常にTCBの一部である。セキュリティ主導の設計では、カーネルを最小限に抑えることが自然である。
そのため、マイクロカーネル設計は、 KeyKOS、EROS 、軍事システムなど、高度なセキュリティアプリケーション向けに設計されたシステムに採用されてきました。実際、最高レベルの保証（評価保証レベル（EAL）7）における共通基準（CC）には、評価対象が「単純」であることが明示的に求められており、複雑なシステムに対して真の信頼性を確立することが実際には不可能であることを認めています。しかし、「単純」という用語は誤解を招きやすく、定義が曖昧です。少なくとも、国防総省の信頼できるコンピュータシステム評価基準では、B3/A1クラスにおいて、より正確な表現が用いられています。
「TCBは、明確に定義されたセマンティクスを持つ、完全かつ概念的にシンプルな保護メカニズムを実装しなければならない。重要なシステムエンジニアリングは、TCBの複雑さを最小限に抑えるとともに、保護上重要でないモジュールをTCBから除外することに向けられなければならない。」
—国防総省の信頼できるコンピュータシステム評価基準
2018年にアジア太平洋システム会議で発表された論文では、当時Linuxカーネルで公開されていたすべての重大なCVEを調査することで、マイクロカーネルはモノリシックカーネルよりも明らかに安全であると主張した。この研究では、問題の40%は正式に検証されたマイクロカーネルでは全く発生せず、そのようなシステムで完全に未解決のまま残る問題はわずか4%であると結論付けた。[ 35 ]
マイクロカーネルに関する最近の研究は、カーネルAPIの形式仕様、およびAPIのセキュリティ特性と実装の正当性の形式証明に焦点を当てています。その最初の例は、EROS APIの簡略化されたモデルに基づいたEROSの隔離メカニズムの数学的証明です。[ 36 ]さらに最近（2007年） 、L4のバージョンであるseL4の保護モデルの特性に関する包括的な機械検証済み証明セットが実行されました。 [ 37 ]
これにより、第 3 世代マイクロカーネルと呼ばれるものが登場しました。[ 38 ]これは、機能によって制御されるリソース アクセスを備えたセキュリティ指向の API 、第一級の関心事としての仮想化、カーネル リソース管理への新しいアプローチ、 [ 39 ]および通常の高性能という目標に加えて、形式分析への適合性という設計目標によって特徴付けられます。例としては、 Coyotos、seL4、Nova、[ 40 ] [ 41 ] Redox、Fiasco.OC などがあります。[ 40 ] [ 42 ]
seL4 の場合、実装の完全な形式検証が達成されています。[ 38 ]つまり、カーネルの実装がその形式仕様と整合しているという数学的証明です。これにより、API について証明された特性が実際のカーネルでも実際に成り立つことが保証され、CC EAL7 を超えるレベルの保証となります。続いて、API のセキュリティ強制特性の証明、および実行可能なバイナリ コードが C 実装の正しい翻訳であることを示す証明が行われ、コンパイラが TCB から除外されました。これらの証明を合わせると、カーネルのセキュリティ特性のエンドツーエンドの証明が確立されます。[ 43 ]
マイクロカーネルの例としては、以下のようなものがあります。
ナノカーネルまたはピコカーネルという用語は、歴史的には以下を指していました。
また、ナノカーネルという用語が小さなカーネルではなく、ナノ秒のクロック分解能をサポートするカーネルを指すケースも少なくとも1つ存在する。[ 45 ]
{{cite book}}: CS1メンテナンス: 場所の発行元が見つかりません (リンク){{cite web}}: CS1 maint: url-status (リンク)