Пасля васьмі гадоў распрацоўкі ўбачыў свет выпуск праекта Muen 1.0, які развівае ядро падзелу (Separation kernel), адсутнасць памылак у зыходных тэкстах якога пацверджана пры дапамозе матэматычных метадаў фармальнай верыфікацыі надзейнасці. Ядро даступна для архітэктуры x86_64 і можа прымяняцца ў крытычна важных сістэмах, якія патрабуюць павышанага ўзроўню надзейнасці і гарантыі адсутнасці збояў. Зыходныя тэксты праекта напісаны на мове Ада і яго верыфікаваным дыялекце SPARK 2014. Код распаўсюджваецца пад ліцэнзіяй GPLv3.
Ядро падзелу ўяўляе сабой мікраядро, якое прадстаўляе асяроддзе для выканання ізаляваных сябар ад сябра кампанентаў, узаемадзеянне якіх цвёрда рэгулююцца зададзенымі правіламі. Ізаляцыя заснавана на ўжыванні пашырэнняў віртуалізацыі Intel VT-x і прадугледжвае ў тым ліку механізмы абароны для блакавання арганізацыі ўтоеных каналаў сувязі. Ядро падзелу больш мінімалістычна і статычна ў параўнанні з іншымі мікраядрамі, што дазваляе скараціць колькасць сітуацый, здольных прывесці да збою.
Ядро выконваецца ў каранёвым рэжыме VMX па аналогіі з гіпервізарам, а ўсе астатнія кампаненты ў некаранёвым рэжыме VMX па аналогіі з гасцёўнямі сістэмамі. Доступ да абсталявання вырабляецца з выкарыстаннем пашырэнняў Intel VT-d DMA і ремапінга перапыненняў, што дае магчымасць рэалізаваць бяспечную прывязку PCI-прылад да кампанентаў, якія запускаюцца пад кіраваннем Muen.
З магчымасцяў Muen адзначаецца падтрымка шмат'ядравых сістэм, укладзеных старонак памяці (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), табліц атрыбутаў старонак памяці (PAT, Page Attribute Table). Muen таксама дае фіксаваны цыклічны планавальнік на базе выцясняльнага таймера Intel VMX, кампактны runtime, які не ўплывае на прадукцыйнасць, сістэму аўдыту крахаў, механізм статычнага прызначэння рэсурсаў на аснове правіл, сістэму апрацоўкі падзей і каналы падзялянай памяці для ўзаемадзеяння ўнутры запускаюцца кампанентаў.
Падтрымліваецца запуск па-над Muen кампанентаў з 64-разрадным машынным кодам, 32- ці 64-разрадных віртуальных машын, 64-разрадных прыкладанняў на мовах Ada і SPARK 2014, віртуальных машын з Linux і самадастатковых "unikernel" на базе MirageOS.
Асноўныя навіны, прапанаваныя ў выпуску Muen 1.0:
- Апублікаваны дакументы са спецыфікацыямі ядра (прылада і архітэктура), сістэмы (сістэмныя палітыкі, Tau0 і інструментарый) і кампанентаў, у якіх дакументаваны ўсе аспекты працы праекта.
- Дададзены інструментар Tau0 (Muen System Composer), які ўключае набор гатовых верыфікаваных кампанентаў для кампаноўкі сістэмных выяў і распрацоўкі тыпавых сэрвісаў, якія запускаюцца па-над Muen. Сярод якія прадстаўляюцца кампанентаў драйвер AHCI (SATA), Device Manager (DM), загрузнік, сістэмны мэнэджар, віртуальны тэрмінал і да т.п.
- Linux-драйвер muenblock (рэалізацыя блокавай прылады, які працуе па-над падзялянай памяці Muen) пераведзены на выкарыстанне API blockdev 2.0.
- Рэалізаваны інструменты для кіравання жыццёвым цыклам натыўных кампанентаў.
- Сістэмныя выявы перакладзены на выкарыстанне SBS (Signed Block Stream) і CSL (Command Stream Loader) для абароны цэласнасці.
- Рэалізаваны верыфікаваны драйвер AHCI-DRV, напісаны на мове SPARK 2014 і які дазваляе падлучаць да кампанентаў назапашвальнікі, якія падтрымліваюць інтэрфейс ATA, або асобныя дыскавыя часткі.
- Палепшана падтрымка unikernel ад праектаў MirageOS і Solo5.
- Інструментарый для мовы Ада абноўлены да выпуску GNAT Community 2021.
- Сістэма бесперапыннай інтэграцыі пераведзена з эмулятара Bochs на ўкладзеныя асяроддзі QEMU / KVM.
- У выявах кампанентаў з Linux задзейнічана ядро Linux 5.4.66.
Крыніца: opennet.ru