1.0 年間の開発期間を経て、Separation カーネルを開発する Muen 86 プロジェクトがリリースされました。正式な信頼性検証の数学的手法を使用して、ソース コードにエラーがないことが確認されました。 このカーネルは x64_2014 アーキテクチャで利用でき、高いレベルの信頼性と障害のない保証を必要とするミッションクリティカルなシステムで使用できます。 プロジェクトのソース コードは、Ada 言語とその検証可能な方言 SPARK 3 で書かれています。コードは GPLvXNUMX ライセンスに基づいて配布されます。
分離カーネルは、相互に分離されたコンポーネントの実行環境を提供するマイクロカーネルであり、その相互作用は所定のルールによって厳密に規制されます。 分離は Intel VT-x 仮想化拡張機能の使用に基づいており、秘密の通信チャネルの組織化をブロックするセキュリティ メカニズムが含まれています。 パーティショニング カーネルは他のマイクロカーネルよりも最小限かつ静的であるため、障害を引き起こす可能性のある状況の数が減少します。
カーネルはハイパーバイザーと同様に VMX ルート モードで実行され、他のすべてのコンポーネントはゲスト システムと同様に VMX 非ルート モードで実行されます。 機器へのアクセスは、Intel VT-d DMA 拡張機能と割り込み再マッピングを使用して行われます。これにより、Muen で実行されているコンポーネントへの PCI デバイスの安全なバインドを実装できます。
Muen の機能には、マルチコア システム、ネストされたメモリ ページ (EPT、拡張ページ テーブル)、MSI (メッセージ シグナル割り込み)、およびメモリ ページ属性テーブル (PAT、ページ属性テーブル) のサポートが含まれます。 Muen は、インテル VMX プリエンプティブ タイマーに基づく固定ラウンドロビン スケジューラ、パフォーマンスに影響を与えないコンパクトなランタイム、クラッシュ監査システム、ルールベースの静的リソース割り当てメカニズム、イベント処理システム、共有メモリ チャネルも提供します。実行中のコンポーネント内の通信。
64 ビット マシン コード、32 ビットまたは 64 ビット仮想マシン、Ada および SPARK 64 言語の 2014 ビット アプリケーション、Linux 仮想マシン、および Muen 上の MirageOS に基づく自己完結型「ユニカーネル」を使用したコンポーネントの実行をサポートします。
Muen 1.0 のリリースで提供される主な革新は次のとおりです。
- カーネル (デバイスとアーキテクチャ)、システム (システム ポリシー、Tau0 およびツールキット)、およびコンポーネントの仕様を記載した文書が公開されており、プロジェクトのあらゆる側面が文書化されています。
- Tau0 (Muen System Composer) ツールキットが追加されました。これには、システム イメージを構成し、Muen 上で実行される標準サービスを開発するための既製の検証済みコンポーネントのセットが含まれています。 提供されるコンポーネントには、AHCI (SATA) ドライバー、デバイス マネージャー (DM)、ブート ローダー、システム マネージャー、仮想ターミナルなどが含まれます。
- muenblock Linux ドライバー (Muen 共有メモリ上で実行されるブロック デバイスの実装) は、blockdev 2.0 API を使用するように変換されました。
- ネイティブ コンポーネントのライフサイクルを管理するためのツールを実装しました。
- システム イメージは、整合性を保護するために SBS (Signed Block Stream) と CSL (Command Stream Loader) を使用するように変換されています。
- SPARK 2014 言語で記述された検証済みの AHCI-DRV ドライバーが実装されており、ATA インターフェイスまたは個々のディスク パーティションをサポートするドライブをコンポーネントに接続できるようになります。
- MirageOS および Solo5 プロジェクトからのユニカーネル サポートが改善されました。
- Ada 言語ツールキットが GNAT Community 2021 リリース用に更新されました。
- 継続的統合システムは、Bochs エミュレーターから QEMU/KVM ネストされた環境に移行されました。
- Linux コンポーネント イメージは Linux 5.4.66 カーネルを使用します。
出所： オープンネット.ru