Издање Муен 1.0, микрокернела отвореног кода за изградњу високо поузданих система

После осам година развоја, пуштен је пројекат Муен 1.0, развијајући језгро за раздвајање, чије је одсуство грешака у изворном коду потврђено коришћењем математичких метода формалне верификације поузданости. Језгро је доступно за архитектуру к86_64 и може се користити у критичним системима који захтевају повећан ниво поузданости и гаранцију да нема кварова. Изворни код пројекта је написан на језику Ада и његовом проверљивом дијалекту СПАРК 2014. Код се дистрибуира под ГПЛв3 лиценцом.

Језгро за раздвајање је микројезгро које обезбеђује окружење за извршавање компоненти изолованих једна од друге, чија је интеракција строго регулисана датим правилима. Изолација се заснива на коришћењу екстензија за виртуелизацију Интел ВТ-к и укључује сигурносне механизме за блокирање организације прикривених комуникационих канала. Партиционо језгро је минималистичкије и статичније од осталих микро језгара, што смањује број ситуација које могу да изазову неуспех.

Кернел ради у ВМКС роот режиму, слично као хипервизор, а све остале компоненте раде у ВМКС нон-роот режиму, слично као гостујући системи. Приступ опреми се остварује коришћењем Интел ВТ-д ДМА екстензија и ремапирањем прекида, што омогућава имплементацију безбедног везивања ПЦИ уређаја за компоненте које раде под Муен-ом.

Издање Муен 1.0, микрокернела отвореног кода за изградњу високо поузданих система

Муен-ове могућности обухватају подршку за системе са више језгара, угнежђене меморијске странице (ЕПТ, проширене табеле страница), МСИ (прекиди сигнализованих порукама) и табеле атрибута меморијске странице (ПАТ, табела атрибута странице). Муен такође обезбеђује фиксни роунд-робин планер заснован на Интел ВМКС превентивном тајмеру, компактно време рада које не утиче на перформансе, систем ревизије пада, механизам за доделу статичког ресурса заснован на правилима, систем за руковање догађајима и дељене меморијске канале за комуникација унутар активних компоненти.

Подржава компоненте за покретање са 64-битним машинским кодом, 32- или 64-битне виртуелне машине, 64-битне апликације на Ада и СПАРК 2014 језицима, Линук виртуелне машине и самосталне „уникернеле“ засноване на МирагеОС-у на врху Муен-а.

Главне иновације понуђене у издању Муен 1.0:

  • Објављени су документи са спецификацијама за језгро (уређај и архитектура), систем (системске политике, Тау0 и комплет алата) и компоненте, које документују све аспекте пројекта.
  • Додан је комплет алата Тау0 (Муен Систем Цомпосер), који укључује скуп готових верификованих компоненти за састављање слика система и развој стандардних услуга које раде на врху Муен-а. Достављене компоненте укључују АХЦИ (САТА) драјвер, Девице Манагер (ДМ), покретач система, системски менаџер, виртуелни терминал, итд.
  • Муенблоцк Линук драјвер (имплементација блок уређаја који ради на Муен дељеној меморији) је конвертован да користи блоцкдев 2.0 АПИ.
  • Имплементирани алати за управљање животним циклусом изворних компоненти.
  • Слике система су конвертоване да користе СБС (Сигнед Блоцк Стреам) и ЦСЛ (Цомманд Стреам Лоадер) за заштиту интегритета.
  • Имплементиран је верификовани АХЦИ-ДРВ драјвер, написан на језику СПАРК 2014 и који вам омогућава да повежете диск јединице које подржавају АТА интерфејс или појединачне партиције диска на компоненте.
  • Побољшана подршка уникернела од МирагеОС и Соло5 пројеката.
  • Ада језички алат је ажуриран за издање ГНАТ Цоммунити 2021.
  • Систем континуиране интеграције је пренет са Боцхс емулатора у КЕМУ/КВМ угнежђена окружења.
  • Слике Линук компоненти користе језгро Линука 5.4.66.

Извор: опеннет.ру

Додај коментар