Izdanje Muen 1.0, otvorenog mikrokernela za izgradnju visoko pouzdanih sistema

Nakon osam godina razvoja, objavljen je projekat Muen 1.0, razvijajući jezgro za razdvajanje, čije je odsustvo grešaka u izvornom kodu potvrđeno matematičkim metodama formalne verifikacije pouzdanosti. Kernel je dostupan za arhitekturu x86_64 i može se koristiti u kritičnim sistemima koji zahtijevaju povećan nivo pouzdanosti i garanciju da nema kvarova. Izvorni kod projekta je napisan na jeziku Ada i njegovom provjerljivom dijalektu SPARK 2014. Kod se distribuira pod GPLv3 licencom.

Jezgro za razdvajanje je mikrokernel koje obezbeđuje okruženje za izvršavanje komponenti izolovanih jedna od druge, čija je interakcija strogo regulisana datim pravilima. Izolacija se zasniva na korišćenju ekstenzija za virtuelizaciju Intel VT-x i uključuje sigurnosne mehanizme za blokiranje organizacije prikrivenih kanala komunikacije. Jezgro za particioniranje je minimalističkije i statičnije od ostalih mikrokernela, što smanjuje broj situacija koje mogu uzrokovati neuspjeh.

Kernel radi u VMX root modu, slično kao hipervizor, a sve ostale komponente rade u VMX non-root modu, slično gostujućim sistemima. Pristup opremi se ostvaruje pomoću Intel VT-d DMA ekstenzija i remappinga prekida, što omogućava implementaciju sigurnog vezivanja PCI uređaja za komponente koje rade pod Muen-om.

Izdanje Muen 1.0, otvorenog mikrokernela za izgradnju visoko pouzdanih sistema

Muen-ove mogućnosti uključuju podršku za sisteme sa više jezgara, ugniježđene memorijske stranice (EPT, proširene tabele stranica), MSI (prekidi signalizirane poruke) i tablice atributa memorijske stranice (PAT, tablica atributa stranice). Muen takođe nudi fiksni round-robin planer zasnovan na Intel VMX preventivnom tajmeru, kompaktno vreme izvođenja koje ne utiče na performanse, sistem revizije pada, mehanizam za dodelu statičkog resursa zasnovan na pravilima, sistem za rukovanje događajima i deljene memorijske kanale za komunikacija unutar aktivnih komponenti.

Podržava komponente sa 64-bitnim mašinskim kodom, 32- ili 64-bitne virtuelne mašine, 64-bitne aplikacije na Ada i SPARK 2014 jezicima, Linux virtuelne mašine i samostalne „unikernele“ zasnovane na MirageOS-u na vrhu Muena.

Glavne inovacije ponuđene u izdanju Muen 1.0:

  • Objavljeni su dokumenti sa specifikacijama za kernel (uređaj i arhitekturu), sistem (sistemske politike, Tau0 i alat) i komponente, koje dokumentuju sve aspekte projekta.
  • Dodan je komplet alata Tau0 (Muen System Composer), koji uključuje skup gotovih provjerenih komponenti za sastavljanje slika sistema i razvoj standardnih usluga koje rade na vrhu Muen-a. Obezbeđene komponente uključuju AHCI (SATA) drajver, Device Manager (DM), pokretač sistema, sistemski menadžer, virtuelni terminal, itd.
  • Muenblock Linux drajver (implementacija blok uređaja koji radi na Muen dijeljenoj memoriji) je konvertiran da koristi blockdev 2.0 API.
  • Implementirani alati za upravljanje životnim ciklusom izvornih komponenti.
  • Slike sistema su konvertovane da koriste SBS (Signed Block Stream) i CSL (Command Stream Loader) za zaštitu integriteta.
  • Implementiran je verifikovani AHCI-DRV drajver, napisan na jeziku SPARK 2014 i koji vam omogućava da povežete diskove koji podržavaju ATA interfejs ili pojedinačne particije diska na komponente.
  • Poboljšana podrška unikernela od MirageOS i Solo5 projekata.
  • Ada jezički alat je ažuriran za izdanje GNAT Community 2021.
  • Sistem kontinuirane integracije prebačen je sa Bochs emulatora u QEMU/KVM ugniježđena okruženja.
  • Slike Linux komponenti koriste jezgro Linuxa 5.4.66.

izvor: opennet.ru

Dodajte komentar