No aacht Joer Entwécklung gouf de Muen 1.0 Projet verëffentlecht, de Separatiounskär entwéckelt, d'Feele vu Feeler am Quellcode vun deem mat mathematesch Methode vun der formell Zouverlässegkeet Verifizéierung bestätegt gouf. De Kernel ass verfügbar fir d'x86_64 Architektur a kann a missionskritesch Systemer benotzt ginn, déi e verstäerkten Niveau vun Zouverlässegkeet erfuerderen a Garantie vu keng Feeler. De Quellcode vum Projet ass an der Ada Sprooch a sengem verifizéierbare Dialekt SPARK 2014 geschriwwen. De Code gëtt ënner der GPLv3 Lizenz verdeelt.
De Trennungskär ass e Mikrokernel deen en Ëmfeld ubitt fir d'Ausféierung vu Komponenten isoléiert vuneneen, d'Interaktioun vun deenen strikt duerch bestëmmte Reegele reglementéiert ass. Isolatioun baséiert op der Notzung vun Intel VT-x Virtualiséierungsverlängerungen an enthält Sécherheetsmechanismen fir d'Organisatioun vu geheime Kommunikatiounskanäl ze blockéieren. De Partitioning Kernel ass méi minimalistesch a statesch wéi aner Mikrokernelen, wat d'Zuel vun de Situatiounen reduzéiert déi Versoen verursaache kënnen.
De Kernel leeft am VMX Root Modus, ähnlech wéi en Hypervisor, an all aner Komponenten lafen am VMX Net-root Modus, ähnlech wéi Gaaschtsystemer. Zougang zu der Ausrüstung gëtt benotzt Intel VT-d DMA Extensiounen an Ënnerbriechung remapping, déi mécht et méiglech sécher Bindung vun PCI Apparater ze Komponente Lafen ënner Muen ëmsetzen.
Dem Muen seng Fäegkeeten enthalen Ënnerstëtzung fir Multi-Core Systemer, Nested Memory Säiten (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), an Memory Page Attribut Tabellen (PAT, Page Attribute Table). Muen bitt och e fixe Round-Robin Scheduler baséiert op dem Intel VMX preemptive Timer, e kompakten Runtime deen net d'Performance beaflosst, e Crash Audit System, e Regel-baséiert statesche Ressource Assignment Mechanismus, en Event Handling System, a gemeinsame Memory Channels fir Kommunikatioun bannent Lafen Komponente.
Et ënnerstëtzt Lafen Komponenten mat 64-Bit Maschinn Code, 32- oder 64-Bit virtuell Maschinnen, 64-Bit Uwendungen an Ada an SPARK 2014 Sproochen, Linux virtuell Maschinnen an Self-contained "Unikernels" baséiert op MirageOS uewen op Muen.
D'Haaptinnovatiounen ugebueden an der Verëffentlechung vu Muen 1.0:
- Dokumenter goufen publizéiert mat Spezifikatioune fir de Kernel (Apparat an Architektur), System (System Politiken, Tau0 an Toolkit) a Komponenten, déi all Aspekter vum Projet dokumentéieren.
- Den Tau0 (Muen System Composer) Toolkit gouf bäigefüügt, deen e Set vu fäerdege verifizéiert Komponenten enthält fir Systembilder ze komponéieren an Standardservicer z'entwéckelen déi uewen op Muen lafen. Komponente geliwwert enthalen AHCI (SATA) Chauffer, Device Manager (DM), Bootloader, Systemmanager, virtuelle Terminal, etc.
- De muenblock Linux Chauffer (eng Implementatioun vun engem Blockapparat, deen uewen op der Muen Shared Memory leeft) gouf ëmgewandelt fir de blockdev 2.0 API ze benotzen.
- Implementéiert Tools fir de Liewenszyklus vun gebiertege Komponenten ze managen.
- Systembilder goufen ëmgewandelt fir SBS (Signed Block Stream) an CSL (Command Stream Loader) ze benotzen fir d'Integritéit ze schützen.
- E verifizéiert AHCI-DRV Chauffer gouf implementéiert, geschriwwe an der SPARK 2014 Sprooch an erlaabt Iech Drive ze verbannen, déi d'ATA Interface oder individuell Diskpartitionen un d'Komponenten ënnerstëtzen.
- Verbesserte unikernel Ënnerstëtzung vu MirageOS a Solo5 Projeten.
- Den Ada Sproochtoolkit gouf fir d'GNAT Community 2021 Verëffentlechung aktualiséiert.
- De kontinuéierleche Integratiounssystem gouf vum Bochs Emulator op QEMU / KVM nestéiert Ëmfeld transferéiert.
- Linux Komponent Biller benotzen de Linux 5.4.66 Kernel.
Source: opennet.ru