Apre uit ane nan devlopman, pwojè Muen 1.0 te lage, devlope nwayo a Separasyon, absans la nan erè nan kòd sous la ki te konfime lè l sèvi avèk metòd matematik nan verifikasyon fyab fòmèl. Kernel la disponib pou achitekti x86_64 la epi li ka itilize nan sistèm misyon kritik ki mande pou yon nivo ogmante fyab ak garanti pou pa gen echèk. Kòd sous pwojè a ekri nan lang Ada ak dyalèk li verifye SPARK 2014. Kòd la distribye anba lisans GPLv3.
Nwayo separasyon an se yon mikrokernel ki bay yon anviwònman pou egzekisyon konpozan izole youn ak lòt, entèraksyon an nan ki se entèdi reglemante pa règ yo bay yo. Izolasyon baze sou itilizasyon ekstansyon Virtualization Intel VT-x e li gen ladan mekanis sekirite pou bloke òganizasyon chanèl kominikasyon kache yo. Nwayo patisyon an pi minimalist ak estatik pase lòt microkernels, ki diminye kantite sitiyasyon ki ka lakòz echèk.
Kernel la kouri nan mòd rasin VMX, menm jan ak yon hypervisor, ak tout lòt konpozan kouri nan mòd VMX ki pa rasin, menm jan ak sistèm envite. Aksè nan ekipman an fèt lè l sèvi avèk ekstansyon Intel VT-d DMA ak entèwonp remapping, sa ki fè li posib aplike obligatwa sekirite nan aparèy PCI ak eleman ki kouri anba Muen.
Kapasite Muen gen ladan sipò pou sistèm milti-nwayo, paj memwa enbrike (EPT, Tablo paj pwolonje), MSI (Message Signaled Interrupts), ak tab atribi paj memwa (PAT, Page Attribute Table). Muen bay tou yon pwogramasyon fiks round-robin ki baze sou revèy prevantif Intel VMX, yon exécution kontra enfòmèl ant ki pa gen enpak sou pèfòmans, yon sistèm odit aksidan, yon mekanis ki baze sou règ estatik plasman resous, yon sistèm jere evènman, ak chanèl memwa pataje pou kominikasyon nan eleman kouri yo.
Li sipòte konpozan kouri ak kòd machin 64-bit, 32- oswa 64-bit machin vityèl, aplikasyon 64-bit nan lang Ada ak SPARK 2014, Linux machin vityèl ak endepandan "unikernels" ki baze sou MirageOS sou tèt Muen.
Inovasyon prensipal yo ofri nan liberasyon an nan Muen 1.0:
- Dokiman yo te pibliye ak espesifikasyon pou nwayo a (aparèy ak achitekti), sistèm (politik sistèm, Tau0 ak zouti) ak konpozan, ki dokimante tout aspè nan pwojè a.
- Yo te ajoute zouti Tau0 (Muen System Composer), ki gen ladann yon seri konpozan verifye pare pou konpoze imaj sistèm ak devlope sèvis estanda ki kouri sou tèt Muen. Eleman yo bay yo enkli chofè AHCI (SATA), Manadjè Aparèy (DM), loader bòt, manadjè sistèm, tèminal vityèl, elatriye.
- Chofè Linux muenblock (yon aplikasyon yon aparèy blòk kouri sou tèt memwa pataje Muen) te konvèti pou itilize API blockdev 2.0.
- Aplike zouti pou jere sik lavi konpozan natif natal yo.
- Imaj sistèm yo te konvèti pou itilize SBS (Signed Block Stream) ak CSL (Command Stream Loader) pou pwoteje entegrite.
- Yo te aplike yon chofè AHCI-DRV verifye, ki ekri nan lang SPARK 2014 la epi ki pèmèt ou konekte kondwi ki sipòte koòdone ATA oswa patisyon disk endividyèl ak konpozan yo.
- Amelyore sipò unikernel nan pwojè MirageOS ak Solo5.
- Yo mete ajou zouti pou lang Ada pou piblikasyon GNAT Community 2021.
- Sistèm entegrasyon kontinyèl la te transfere soti nan Emulation Bochs nan anviwònman QEMU / KVM enbrike.
- Imaj konpozan Linux itilize nwayo Linux 5.4.66 la.
Sous: opennet.ru