Eldono de Muen 1.0, malfermkoda mikrokerno por konstrui tre fidindajn sistemojn

Post ok jaroj da evoluo, la projekto Muen 1.0 estis publikigita, evoluigante la Separation-kernon, kies foresto de eraroj en kies fontkodo estis konfirmita uzante matematikajn metodojn de formala fidindeco-konfirmo. La kerno disponeblas por la arkitekturo x86_64 kaj uzeblas en misi-kritikaj sistemoj, kiuj postulas pliigitan fidindecon kaj garantion de neniu fiasko. La fontkodo de la projekto estas skribita en la lingvo Ada kaj ĝia kontrolebla dialekto SPARK 2014. La kodo estas distribuita laŭ la permesilo GPLv3.

La apartkerno estas mikrokerno kiu disponigas medion por la ekzekuto de komponentoj izolitaj unu de la alia, kies interagado estas strikte reguligita per donitaj reguloj. Izoliĝo baziĝas sur la uzo de Intel VT-x-virtualigaj etendaĵoj kaj inkluzivas sekurecajn mekanismojn por bloki la organizon de kaŝaj komunikadkanaloj. La dispartigo-kerno estas pli minimumisma kaj senmova ol aliaj mikrokernoj, kio reduktas la nombron da situacioj kiuj povas kaŭzi fiaskon.

La kerno funkcias en VMX-radika reĝimo, simila al hiperviziero, kaj ĉiuj aliaj komponentoj funkcias en VMX-ne-radika reĝimo, simile al gastsistemoj. Aliro al la ekipaĵo estas farita per etendaĵoj de Intel VT-d DMA kaj interrompa remapado, kio ebligas efektivigi sekuran ligon de PCI-aparatoj al komponantoj kurantaj sub Muen.

Eldono de Muen 1.0, malfermkoda mikrokerno por konstrui tre fidindajn sistemojn

La kapabloj de Muen inkludas subtenon por plurkernaj sistemoj, nestitajn memorpaĝojn (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), kaj memorpaĝajn atributtablojn (PAT, Page Attribute Table). Muen ankaŭ disponigas fiksan cirkla-subskribolistan planilon bazitan sur la Intel VMX antaŭtempa tempigilo, kompaktan rultempon kiu ne influas efikecon, kraŝrevizian sistemon, regul-bazitan senmovan asignomekanismon, okazaĵtraktadsistemon, kaj komunajn memorkanalojn por komunikado ene de kurantaj komponantoj.

Ĝi subtenas kurantajn komponantojn kun 64-bita maŝinkodo, 32- aŭ 64-bitaj virtualaj maŝinoj, 64-bitaj aplikoj en lingvoj Ada kaj SPARK 2014, Linukso-virtualaj maŝinoj kaj memstaraj "unikernels" bazitaj sur MirageOS aldone al Muen.

La ĉefaj novigoj ofertitaj en la liberigo de Muen 1.0:

  • Dokumentoj estis publikigitaj kun specifoj por la kerno (aparato kaj arkitekturo), sistemo (sistemaj politikoj, Tau0 kaj ilaro) kaj komponentoj, kiuj dokumentas ĉiujn aspektojn de la projekto.
  • La ilaro Tau0 (Muen System Composer) estis aldonita, kiu inkluzivas aron de pretaj kontrolitaj komponantoj por verki sistemajn bildojn kaj disvolvi normajn servojn, kiuj funkcias super Muen. Komponantoj provizitaj inkluzivas AHCI (SATA) ŝoforon, Device Manager (DM), ekŝargilon, sistemmanaĝeron, virtualan terminalon, ktp.
  • La muenblock Linukso-ŝoforo (efektivigo de bloka aparato funkcianta aldone al la komuna memoro Muen) estis konvertita por uzi la blockdev 2.0 API.
  • Efektivigitaj iloj por administri la vivociklon de indiĝenaj komponantoj.
  • Sistembildoj estis konvertitaj por uzi SBS (Signed Block Stream) kaj CSL (Command Stream Loader) por protekti integrecon.
  • Kontrolita AHCI-DRV-ŝoforo estis efektivigita, skribita en la lingvo SPARK 2014 kaj permesanta vin konekti diskojn, kiuj subtenas la ATA-interfacon aŭ individuajn disksekciojn al la komponantoj.
  • Plibonigita unukerna subteno de MirageOS kaj Solo5-projektoj.
  • La Ada-lingva ilaro estis ĝisdatigita por la eldono de GNAT Community 2021.
  • La kontinua integriga sistemo estis translokigita de la Bochs-emulilo al QEMU/KVM nestitaj medioj.
  • Linuksaj komponentbildoj uzas la Linukso 5.4.66-kernon.

fonto: opennet.ru

Aldoni komenton