Издание на Muen 1.0, микрокернел со отворен код за градење високо доверливи системи

По осум години развој, беше објавен проектот Muen 1.0, развивајќи го кернелот Separation, чие отсуство на грешки во изворниот код беше потврдено со помош на математички методи за формална проверка на веродостојноста. Јадрото е достапно за архитектурата x86_64 и може да се користи во системи кои се критични за мисијата кои бараат зголемено ниво на доверливост и гаранција за без дефекти. Изворниот код на проектот е напишан на јазикот Ада и на неговиот проверлив дијалект SPARK 2014. Кодот се дистрибуира под лиценцата GPLv3.

Сепарационото јадро е микрокернел кој обезбедува средина за извршување на компоненти изолирани едни од други, чија интеракција е строго регулирана со дадени правила. Изолацијата се заснова на употреба на екстензии за виртуелизација на Intel VT-x и вклучува безбедносни механизми за блокирање на организацијата на тајните комуникациски канали. Јадрото за партиционирање е поминималистички и статично од другите микрокернели, што го намалува бројот на ситуации кои можат да предизвикаат неуспех.

Јадрото работи во VMX root режим, слично на хипервизорот, а сите други компоненти работат во VMX не-root режим, слично на гостинските системи. Пристапот до опремата е направен со помош на екстензии на Intel VT-d DMA и повторно мапирање на прекини, што овозможува да се имплементира безбедно поврзување на уредите PCI со компоненти што работат под Muen.

Можностите на Muen вклучуваат поддршка за повеќејадрени системи, страници со вгнездена меморија (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) и табели за атрибути на мемориски страници (PAT, Page Attribute Table). Muen, исто така, обезбедува фиксен распоредувач за кругови базиран на превентивниот тајмер Intel VMX, компактно време на работа што не влијае на перформансите, систем за ревизија на падови, механизам за доделување статички ресурси заснован на правила, систем за справување со настани и споделени мемориски канали за комуникација во рамките на активните компоненти.

Поддржува работи со компоненти со 64-битен машински код, 32- или 64-битни виртуелни машини, 64-битни апликации на јазиците Ada и SPARK 2014, виртуелни машини Линукс и самостојни „уникернели“ базирани на MirageOS на врвот на Muen.

Главните иновации понудени во објавувањето на Muen 1.0:

• Објавени се документи со спецификации за кернелот (уред и архитектура), системот (системски политики, Tau0 и комплет алатки) и компоненти, кои ги документираат сите аспекти на проектот.
• Додадена е алатката Tau0 (Muen System Composer), која вклучува сет на готови потврдени компоненти за составување слики на системот и развој на стандардни услуги кои работат на врвот на Muen. Обезбедените компоненти вклучуваат драјвер за AHCI (SATA), Управувач со уреди (DM), подигнувач, системски менаџер, виртуелен терминал итн.
• Возачот на muenblock Linux (имплементација на блок-уред што работи на врвот на споделената меморија Muen) е конвертиран да го користи blockdev 2.0 API.
• Имплементирани алатки за управување со животниот циклус на природните компоненти.
• Сликите на системот се конвертирани за да користат SBS (Потпишан блок проток) и CSL (Command Stream Loader) за заштита на интегритетот.
• Имплементиран е потврден драјвер за AHCI-DRV, напишан на јазикот SPARK 2014 и ви овозможува да поврзете дискови што поддржуваат интерфејс ATA или поединечни партиции на дискот со компонентите.
• Подобрена поддршка за уникернел од проектите MirageOS и Solo5.
• Јазичниот алатник Ada е ажуриран за изданието GNAT Community 2021 година.
• Системот за континуирана интеграција е префрлен од емулаторот Bochs во вгнездени средини QEMU/KVM.
• Сликите на компонентата на Linux го користат кернелот Linux 5.4.66.

Извор: opennet.ru