經過八年的開發，Muen 1.0專案發布，開發了Separation內核，並透過形式可靠性驗證的數學方法確認了原始程式碼不存在錯誤。此核心適用於 x86_64 架構，可用於需要更高層級的可靠性並保證無故障的關鍵任務系統。該專案的源代碼是用Ada語言及其可驗證方言SPARK 2014編寫的。該程式碼在GPLv3許可證下分發。
分離內核是一個微內核，為相互隔離的元件提供執行環境，元件之間的交互受到給定規則的嚴格控制。隔離基於 Intel VT-x 虛擬化擴充的使用，並包括阻止秘密通訊通道組織的安全機制。分區內核比其他微內核更加簡約和靜態，從而減少了可能導致失敗的情況。
核心以 VMX 根模式運行，類似於虛擬機器管理程序，所有其他元件以 VMX 非根模式運行，類似於來賓系統。使用 Intel VT-d DMA 擴展和中斷重新映射對設備進行訪問，從而可以實現 PCI 設備與 Muen 下運行的組件的安全綁定。
Muen 的功能包括支援多核心系統、巢狀記憶體頁面（EPT，擴充頁表）、MSI（訊息訊號中斷）和記憶體頁面屬性表（PAT，頁面屬性表）。 Muen 還提供基於 Intel VMX 搶佔式計時器的固定循環調度程序、不影響性能的緊湊運行時、崩潰審核系統、基於規則的靜態資源分配機制、事件處理系統以及共享內存通道。運行組件內的通訊。
它支援運行具有 64 位元機器代碼的元件、32 位元或 64 位元虛擬機、Ada 和 SPARK 64 語言的 2014 位元應用程式、Linux 虛擬機以及基於 Muen 之上的 MirageOS 的獨立「unikernels」。
Muen 1.0版本中提供的主要創新：
- 已發布包含核心（設備和架構）、系統（系統策略、Tau0 和工具包）和組件規範的文檔，記錄了該專案的各個方面。
- 新增了 Tau0（Muen System Composer）工具包，其中包括一組現成的經過驗證的元件，用於建立系統映像和開發在 Muen 之上運行的標準服務。提供的元件包括AHCI（SATA）驅動程式、裝置管理員（DM）、引導程式、系統管理員、虛擬終端機等。
- muenblock Linux 驅動程式（在 Muen 共享記憶體之上運行的區塊裝置的實作）已轉換為使用 blockdev 2.0 API。
- 實現了用於管理本機元件生命週期的工具。
- 系統映像已轉換為使用 SBS（簽章區塊流）和 CSL（命令流載入器）來保護完整性。
- 已實施經過驗證的 AHCI-DRV 驅動程序，該驅動程式以 SPARK 2014 語言編寫，可讓您將支援 ATA 介面或單一磁碟分割的磁碟機連接到元件。
- 改進了 MirageOS 和 Solo5 專案的 unikernel 支援。
- Ada 語言工具包已針對 GNAT Community 2021 版本進行了更新。
- 持續整合系統已從Bochs模擬器轉移到QEMU/KVM嵌套環境。
- Linux 元件映像使用 Linux 5.4.66 核心。
來源： opennet.ru