Izdaja Muen 1.0, odprtokodnega mikrojedra za gradnjo zelo zanesljivih sistemov

Po osmih letih razvoja je bil izdan projekt Muen 1.0, ki razvija jedro Separation, katerega odsotnost napak v izvorni kodi je bila potrjena z matematičnimi metodami formalnega preverjanja zanesljivosti. Jedro je na voljo za arhitekturo x86_64 in se lahko uporablja v kritičnih sistemih, ki zahtevajo večjo stopnjo zanesljivosti in garancijo brez okvar. Izvorna koda projekta je napisana v jeziku Ada in njegovem preverljivem dialektu SPARK 2014. Koda se distribuira pod licenco GPLv3.

Ločevalno jedro je mikrojedro, ki zagotavlja okolje za izvajanje med seboj izoliranih komponent, katerih interakcija je strogo regulirana z danimi pravili. Izolacija temelji na uporabi virtualizacijskih razširitev Intel VT-x in vključuje varnostne mehanizme za blokiranje organizacije prikritih komunikacijskih kanalov. Jedro za razdelitev je bolj minimalistično in statično kot druga mikrojedra, kar zmanjša število situacij, ki lahko povzročijo okvaro.

Jedro deluje v korenskem načinu VMX, podobno kot hipervizor, vse druge komponente pa v nekorenskem načinu VMX, podobno kot sistemi za goste. Dostop do opreme je izveden z uporabo razširitev Intel VT-d DMA in preslikave prekinitev, kar omogoča implementacijo varne vezave naprav PCI na komponente, ki se izvajajo pod Muen.

Izdaja Muen 1.0, odprtokodnega mikrojedra za gradnjo zelo zanesljivih sistemov

Zmogljivosti Muena vključujejo podporo za večjedrne sisteme, ugnezdene pomnilniške strani (EPT, razširjene tabele strani), MSI (sporočilno signalizirane prekinitve) in tabele atributov pomnilniških strani (PAT, tabela atributov strani). Muen ponuja tudi fiksni krožni razporejevalnik, ki temelji na vnaprejšnjem časovniku Intel VMX, kompakten čas izvajanja, ki ne vpliva na zmogljivost, sistem za nadzor zrušitev, mehanizem za dodeljevanje statičnih virov na podlagi pravil, sistem za obravnavanje dogodkov in skupne pomnilniške kanale za komunikacijo znotraj tekočih komponent.

Podpira delujoče komponente s 64-bitno strojno kodo, 32- ali 64-bitne navidezne stroje, 64-bitne aplikacije v jezikih Ada in SPARK 2014, virtualne stroje Linux in samostojna »enojna jedra«, ki temeljijo na MirageOS na vrhu Muen.

Glavne novosti, ki jih ponuja izdaja Muen 1.0:

  • Objavljeni so bili dokumenti s specifikacijami za jedro (naprava in arhitektura), sistem (sistemske politike, Tau0 in komplet orodij) in komponente, ki dokumentirajo vse vidike projekta.
  • Dodan je komplet orodij Tau0 (Muen System Composer), ki vključuje nabor že pripravljenih preverjenih komponent za sestavljanje slik sistema in razvoj standardnih storitev, ki delujejo na vrhu Muena. Priložene komponente vključujejo gonilnik AHCI (SATA), upravitelja naprav (DM), zagonski nalagalnik, sistemskega upravitelja, virtualni terminal itd.
  • Gonilnik muenblock Linux (izvedba blokovne naprave, ki se izvaja na vrhu skupnega pomnilnika Muen) je bil pretvorjen za uporabo API-ja blockdev 2.0.
  • Implementirana orodja za upravljanje življenjskega cikla izvornih komponent.
  • Sistemske slike so bile pretvorjene za uporabo SBS (Signed Block Stream) in CSL (Command Stream Loader) za zaščito celovitosti.
  • Implementiran je bil preverjen gonilnik AHCI-DRV, ki je napisan v jeziku SPARK 2014 in omogoča povezavo diskov, ki podpirajo vmesnik ATA ali posameznih diskovnih particij na komponente.
  • Izboljšana podpora za eno jedro iz projektov MirageOS in Solo5.
  • Komplet orodij za jezik Ada je bil posodobljen za izdajo skupnosti GNAT 2021.
  • Sistem neprekinjene integracije je bil prenesen iz emulatorja Bochs v ugnezdena okolja QEMU/KVM.
  • Slike komponent Linuxa uporabljajo jedro Linuxa 5.4.66.

Vir: opennet.ru

Dodaj komentar