Muen 1.0 шығарылымы, жоғары сенімді жүйелерді құруға арналған ашық бастапқы микроядро

Сегіз жылдық дамудан кейін Separation ядросын әзірлейтін Muen 1.0 жобасы шығарылды, оның бастапқы кодында қателердің жоқтығы формальды сенімділікті тексерудің математикалық әдістерімен расталды. Ядро x86_64 архитектурасы үшін қол жетімді және сенімділіктің жоғары деңгейін және сәтсіздікке кепілдік беруді талап ететін маңызды жүйелерде қолданылуы мүмкін. Жобаның бастапқы коды Ada тілінде және оның тексерілетін SPARK 2014 диалектінде жазылған. Код GPLv3 лицензиясы бойынша таратылады.

Бөлу ядросы – бір-бірінен оқшауланған компоненттердің орындалу ортасын қамтамасыз ететін, өзара әрекеті берілген ережелермен қатаң реттелетін микроядро. Оқшаулау Intel VT-x виртуалдандыру кеңейтімдерін пайдалануға негізделген және жасырын байланыс арналарын ұйымдастыруды блоктау үшін қауіпсіздік механизмдерін қамтиды. Бөлу ядросы басқа микроядроларға қарағанда минималистік және статикалық болып табылады, бұл сәтсіздікке әкелетін жағдайлардың санын азайтады.

Ядро гипервизорға ұқсас VMX түбірлік режимінде жұмыс істейді және барлық басқа компоненттер қонақтық жүйелерге ұқсас VMX түбірлік емес режимде жұмыс істейді. Жабдыққа кіру Intel VT-d DMA кеңейтімдері мен үзілістерді қайта құру арқылы жүзеге асырылады, бұл PCI құрылғыларын Muen астында жұмыс істейтін құрамдастарға қауіпсіз байланыстыруды жүзеге асыруға мүмкіндік береді.

Muen 1.0 шығарылымы, жоғары сенімді жүйелерді құруға арналған ашық бастапқы микроядро

Muen мүмкіндіктеріне көп ядролы жүйелерді, кірістірілген жад беттерін (EPT, кеңейтілген бет кестелері), MSI (хабарлама сигналдық үзілістері) және жад бетінің төлсипат кестелерін (PAT, бет төлсипаттары кестесі) қолдау кіреді. Muen сонымен қатар Intel VMX алдын ала таймеріне негізделген тұрақты айналымды жоспарлаушыны, өнімділікке әсер етпейтін ықшам жұмыс уақытын, апатты тексеру жүйесін, ережеге негізделген статикалық ресурс тағайындау механизмін, оқиғаларды өңдеу жүйесін және ортақ жад арналарын ұсынады. іске қосылған құрамдастардың ішіндегі байланыс.

Ол 64-биттік машина коды, 32- немесе 64-биттік виртуалды машиналар, Ada және SPARK 64 тілдеріндегі 2014-биттік қолданбалар, Linux виртуалды машиналары және Muen үстіңгі жағындағы MirageOS негізіндегі дербес "unikernels" бар іске қосылған компоненттерді қолдайды.

Muen 1.0 шығарылымында ұсынылатын негізгі инновациялар:

  • Құжаттар жобаның барлық аспектілерін құжаттайтын ядроға (құрылғы және архитектура), жүйеге (жүйелік саясаттар, Tau0 және құралдар жинағы) және құрамдастарға арналған спецификацияларымен жарияланды.
  • Tau0 (Muen System Composer) құралдар жинағы қосылды, ол жүйелік кескіндерді құрастыруға және Muen үстінде жұмыс істейтін стандартты қызметтерді әзірлеуге арналған дайын тексерілген құрамдастарды қамтиды. Берілген құрамдастарға AHCI (SATA) драйвері, құрылғы менеджері (DM), жүктеуші, жүйе менеджері, виртуалды терминал және т.б.
  • muenblock Linux драйвері (Muen ортақ жадының үстінде жұмыс істейтін блок құрылғысының іске асуы) blockdev 2.0 API пайдалану үшін түрлендірілді.
  • Жергілікті компоненттердің өмірлік циклін басқаруға арналған құралдар енгізілді.
  • Жүйе кескіндері тұтастықты қорғау үшін SBS (Signed Block Stream) және CSL (Command Stream Loader) пайдалану үшін түрлендірілді.
  • SPARK 2014 тілінде жазылған және құрамдастарға ATA интерфейсін немесе жеке диск бөлімдерін қолдайтын дискілерді қосуға мүмкіндік беретін тексерілген AHCI-DRV драйвері енгізілді.
  • MirageOS және Solo5 жобаларынан жақсартылған unikernel қолдауы.
  • Ada тілінің құралдар жинағы GNAT қауымдастығы 2021 шығарылымы үшін жаңартылды.
  • Үздіксіз интеграция жүйесі Bochs эмуляторынан QEMU/KVM кірістірілген орталарына ауыстырылды.
  • Linux құрамдас кескіндері Linux 5.4.66 ядросын пайдаланады.

Ақпарат көзі: opennet.ru

пікір қалдыру