Izdanje Muen 1.0, mikrojezgre otvorenog koda za izgradnju vrlo pouzdanih sustava

Nakon osam godina razvoja, objavljen je projekt Muen 1.0, razvijajući Separation kernel, čija je odsutnost pogrešaka u izvornom kodu potvrđena matematičkim metodama formalne provjere pouzdanosti. Kernel je dostupan za x86_64 arhitekturu i može se koristiti u kritičnim sustavima koji zahtijevaju povećanu razinu pouzdanosti i garanciju bez kvarova. Izvorni kod projekta napisan je na jeziku Ada i njegovom provjerljivom dijalektu SPARK 2014. Kod se distribuira pod licencom GPLv3.

Jezgra razdvajanja je mikrojezgra koja pruža okruženje za izvođenje komponenti međusobno izoliranih, čija je interakcija strogo regulirana zadanim pravilima. Izolacija se temelji na korištenju virtualizacijskih proširenja Intel VT-x i uključuje sigurnosne mehanizme za blokiranje organizacije tajnih komunikacijskih kanala. Kernel za particioniranje je minimalističkiji i statičniji od drugih mikrojezgri, što smanjuje broj situacija koje mogu uzrokovati kvar.

Kernel radi u VMX root načinu, slično hipervizoru, a sve ostale komponente rade u VMX non-root načinu, slično sustavima za goste. Pristup opremi ostvaruje se pomoću Intel VT-d DMA ekstenzija i remappinga prekida, što omogućuje implementaciju sigurnog vezanja PCI uređaja na komponente koje rade pod Muenom.

Izdanje Muen 1.0, mikrojezgre otvorenog koda za izgradnju vrlo pouzdanih sustava

Muenove mogućnosti uključuju podršku za multi-core sustave, ugniježđene memorijske stranice (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) i tablice atributa memorijskih stranica (PAT, Page Attribute Table). Muen također nudi fiksni kružni raspored temeljen na Intel VMX preemptive timeru, kompaktno vrijeme izvođenja koje ne utječe na performanse, sustav revizije rušenja, mehanizam dodjele statičkih resursa temeljen na pravilima, sustav za rukovanje događajima i dijeljene memorijske kanale za komunikacija unutar aktivnih komponenti.

Podržava pokretanje komponenti sa 64-bitnim strojnim kodom, 32- ili 64-bitnim virtualnim strojevima, 64-bitnim aplikacijama na jezicima Ada i SPARK 2014, Linux virtualnim strojevima i samostalnim "unikernelima" temeljenim na MirageOS-u na vrhu Muen.

Glavne inovacije ponuđene u izdanju Muen 1.0:

  • Objavljeni su dokumenti sa specifikacijama za kernel (uređaj i arhitektura), sustav (politike sustava, Tau0 i set alata) i komponente, koji dokumentiraju sve aspekte projekta.
  • Dodan je skup alata Tau0 (Muen System Composer), koji uključuje skup gotovih provjerenih komponenti za sastavljanje slika sustava i razvoj standardnih servisa koji rade povrh Muena. Isporučene komponente uključuju AHCI (SATA) upravljački program, Upravitelj uređaja (DM), pokretački program, upravitelj sustava, virtualni terminal itd.
  • Pokretački program za muenblock Linux (implementacija blok uređaja koji radi na Muen dijeljenoj memoriji) pretvoren je za korištenje API-ja blockdev 2.0.
  • Implementirani alati za upravljanje životnim ciklusom izvornih komponenti.
  • Slike sustava su pretvorene da koriste SBS (Signed Block Stream) i CSL (Command Stream Loader) radi zaštite integriteta.
  • Implementiran je provjereni AHCI-DRV upravljački program, napisan na SPARK 2014 jeziku i koji vam omogućuje povezivanje pogona koji podržavaju ATA sučelje ili pojedinačne particije diska na komponente.
  • Poboljšana unikenel podrška iz MirageOS i Solo5 projekata.
  • Jezični alat Ada ažuriran je za izdanje GNAT zajednice 2021.
  • Sustav kontinuirane integracije prebačen je iz Bochs emulatora u QEMU/KVM ugniježđena okruženja.
  • Slike komponenti Linuxa koriste jezgru Linuxa 5.4.66.

Izvor: opennet.ru

Dodajte komentar