LINUX.ORG.RU

Muen SK 1.1.0

 , muen, separation kernel, ,


0

2

Состоялся выпуск разделительного ядра (separation kernel) Muen, развиваемого швейцарской компанией Codelabs.

Muen поддерживает только платформы Intel x86_64 и позволяет гарантировать, что запущенные в нём ядра ОС и приложения не могут получить доступ к ресурсам сверх выделенной для них квоты. Это касается, в том числе, оперативной памяти, процессорного времени и доступа к устройствам ввода-вывода.

В качестве гостевых приложений поддерживаются ядро Linux, программы на Ada/SPARK, а также библиотечные ОС, написанные с использованием фреймворка Solo5 (например, MirageOS на OCaml). Для Linux предоставлены драйверы ядра для ускорения доступа к PCI и другим ресурсам хоста.

Сам Muen целиком реализован на SPARK – безопасном подмножестве языка Ada – и прошёл верификацию на отсутствие ошибок времени выполнения. Код распространяется под лицензией GPLv3.

>>> Подробности

★★★★★

Проверено: hobbit ()
Последнее исправление: hobbit (всего исправлений: 5)

По описанию похоже на виртуалочный гипервизор, в чём отличия, почему называется по-другому?

firkax ★★★★★
()
Ответ на: комментарий от gns

Он и есть. Только гости ходят под конвоем и в сопровождении диетолога :)

И у всех конвоиров и диетологов есть бумажечка, что они правда умеют делать свою работу. Сертифицированные, так сказать, специалисты. :)

AndreyKl ★★★★★
()
Ответ на: комментарий от AndreyKl

Ну да, ну да... Sertified & Verified тэсэзэть... :)

gns ★★★★★
()

Да, ребята... На этом коде надо учиться как программы писать надо. Уж оформлять, так точно! Но нам немецкого занудства не хватит и швейцарской точности.

gns ★★★★★
()
Ответ на: комментарий от Smacker

Не знаю, но каждому свое обеспечивают :)

gns ★★★★★
()

программы на Ada/SPARK, а также библиотечные ОС, написанные с
использованием фреймворка Solo5 (например, MirageOS на OCaml)
Сам Muen целиком реализован на SPARK – безопасном подмножестве языка Ada – и прошёл верификацию на отсутствие ошибок времени выполнения.

звучит интересно, как там с блобами в сторону актуального железа?

etwrq ★★★★★
()
Ответ на: комментарий от etwrq

Весь код открыт, хоть апизучайся! :)

gns ★★★★★
()
Ответ на: комментарий от cumvillain

Нет, это именно что очень специализированный гипервизор с API для запуска специально написанных для него ядер. Ближе всего тут будет Xen, но эта штука ориентирована на безопасность и корректность.

hateyoufeel ★★★★★
() автор топика
Ответ на: комментарий от firkax

Потому что концепт появился раньше чем виртуалки. В данном случае, то что гости исполняются как виртуалки – особенность реализации.

hateyoufeel ★★★★★
() автор топика
Ответ на: комментарий от gns

Да, ребята… На этом коде надо учиться как программы писать надо. Уж оформлять, так точно! Но нам немецкого занудства не хватит и швейцарской точности.

Самое интересное тут в том, что проект родился как магистерская работа двух чуваков. Которые потом сделали компанию и до сих пор это пилят, но уже за деньги.

А теперь вспомни магистерские в своём ВУЗе и горько всплакни.

hateyoufeel ★★★★★
() автор топика
Ответ на: комментарий от gns

немецкого занудства не хватит

Я видел много немецкого софта, да хоть от того же Siemens - настолько кривые и вырвиглазные приложения не делает никто.

Turbid ★★★★★
()
Ответ на: комментарий от hateyoufeel

Ну я в качестве магистерской сдал рабочий проект эмулятора HSMа от Eracom. Не ТНБ весть что, но штука полезная. У буржуев тупо больше времени на учебу, и о хлебе насущном в среднем думать не надо. Ну и ребята с головой походу, видимо, получили оплачиваемую стажировку у упомянутых немецких безопасников со всеми вытекающими. Ну молодцы, чо!

Осталось это куда-нибудь поставить и оценить практическую применимость.

gns ★★★★★
()
Последнее исправление: gns (всего исправлений: 1)
Ответ на: комментарий от Turbid

Ну там тоже много «эффективных менеджеров», зааутсорсить что-либо у индусов много ума не надо.

gns ★★★★★
()
Ответ на: комментарий от gns

У буржуев тупо больше времени на учебу, и о хлебе насущном в среднем думать не надо. Ну и ребята с головой походу, видимо, получили оплачиваемую стажировку у упомянутых немецких безопасников со всеми вытекающими. Ну молодцы, чо!

Дело не в хлебе насущном. В моём ВУЗе (один из ведущих в РФ лол) основной мантрой было чтобы «студент был всё время за%*?н». Ну и качество преподавания было тоже так себе.

А стажировки и у нас были, даже оплачиваемые, с этим как бы нет проблем.

Осталось это куда-нибудь поставить и оценить практическую применимость.

Практическая применимость уже оценена. Я в Solo5 и около немного участвую, оттуда об этом и узнал. Как замена Xen в сценариях с unikernels эта штука прямо отлично подходит, чтобы аж целый лялекс на железке не запускать.

hateyoufeel ★★★★★
() автор топика
Последнее исправление: hateyoufeel (всего исправлений: 1)
Ответ на: комментарий от Turbid

немецкого занудства не хватит

Я видел много немецкого софта, да хоть от того же Siemens - настолько кривые и вырвиглазные приложения не делает никто.

Три буквы: SAP

hateyoufeel ★★★★★
() автор топика
Ответ на: комментарий от hateyoufeel

Ближе всего тут будет Xen, но эта штука ориентирована на безопасность и корректность.

Я не вижу у них эмуляции железа и платформы, там все выглядит как проброс.

cumvillain
()
Ответ на: комментарий от cumvillain

Ближе всего тут будет Xen, но эта штука ориентирована на безопасность и корректность.

Я не вижу у них эмуляции железа и платформы, там все выглядит как проброс.

У Xen этого тоже особо не было. У Xen вообще специальный API для гостей для паравиртуализации (т.е. проброса) есть, как и тут.

Если не считать запуска Linux, эта штука расчитана на гостей, которым в среднем посрать на железо кроме случаев проброса. В минимальном случае, гость не знает о железе вообще ничего и не завязан на детали реализации IBM PC и подобной срани. Типичный сценарий для unikernels.

hateyoufeel ★★★★★
() автор топика
Последнее исправление: hateyoufeel (всего исправлений: 1)
Ответ на: комментарий от hateyoufeel

Если не считать запуска Linux, эта штука расчитана на гостей, которым в среднем посрать на железо кроме случаев проброса. В минимальном случае, гость не знает о железе вообще ничего и не завязан на детали реализации IBM PC и подобной срани. Типичный сценарий для unikernels.

Да, я это и подразумеваю, когда про докер говорю. Цель запустить условный nginx, на предоставить виртуальную машину.

cumvillain
()
Ответ на: комментарий от cumvillain

Если не считать запуска Linux, эта штука расчитана на гостей, которым в среднем посрать на железо кроме случаев проброса. В минимальном случае, гость не знает о железе вообще ничего и не завязан на детали реализации IBM PC и подобной срани. Типичный сценарий для unikernels.

Да, я это и подразумеваю, когда про докер говорю. Цель запустить условный nginx, на предоставить виртуальную машину.

У тебя очень странные понятия о докере. Докер – пакетный менеджер, позволяющий заодно запускать всякую срань в изоляции с доступом к лялексовому ведру. Здесь нет ни пакетного менеджмента, ни лялексового ведра (кроме как гостя, но другие гости об этом не будут знать).

Это буквально очень специализированный аналог Xen. Тусовка, к слову, тоже примерно та же: всякие поехавшие окамлщики и прочие хачкеллисты (у Xen первый тулинг на окамле был), двинутые в сторону безопасности.

hateyoufeel ★★★★★
() автор топика
Последнее исправление: hateyoufeel (всего исправлений: 1)
Ответ на: комментарий от hateyoufeel

ну, у нас в универе в эпоху моей молодости на 3м курсе чувачок между делом драйверы и другой разный системный код для фряхи писал, коммитил, в рамках курсовой, так что прямо сильно этим ты меня не поразил. Да и всякие бывали у нас дипломные работы…

Alphaer ★★
()
Последнее исправление: Alphaer (всего исправлений: 3)
Ответ на: комментарий от hateyoufeel

Три буквы: SAP

Как-то в сообществе эту штуку принято хвалить, если отвалили много денег на кастомизацию. Сам не видел. Так это про хорошо или про плохо?

gns ★★★★★
()
Ответ на: комментарий от hateyoufeel

Ну тащемта интересная тусовочка, например. Я б поучаствовал, если б хаскель с окамлом умел бы чуть получше. Надо у Леши Отта про этих людей поспрашивать, может он что знает.

gns ★★★★★
()
Ответ на: комментарий от gns

Ну тащемта интересная тусовочка, например. Я б поучаствовал, если б хаскель с окамлом умел бы чуть получше. Надо у Леши Отта про этих людей поспрашивать, может он что знает.

Это не обязательно, руст и сишка там тоже есть. Solo5 почти целиком на C, например (кроме биндингов к OCaml для MirageOS, но их можно игнорировать по большей части).

hateyoufeel ★★★★★
() автор топика

десять лет пилят, давно что-то не слышно было новостей от них

sartakov
()
Ответ на: комментарий от cumvillain

Это больше докер, чем гипервизор.

А ты смешной. Давай, представишь сначала, как докер будет работать без ядра?

GFORGX ★★★
()

Хм, интересный проект. Спасибо за новость! Любопытно будет код глянуть.

GFORGX ★★★
()
Ответ на: комментарий от GFORGX

Еще раз: он похож на докер (или xen, если больше нравится) тем, что не предоставляет тебе виртуальную машину, не эмулирует оборудование, нет acpi таблиц и прочего говна.

cumvillain
()
Ответ на: комментарий от cumvillain

Еще раз: он похож на докер (или xen, если больше нравится) тем, что не предоставляет тебе виртуальную машину, не эмулирует оборудование, нет acpi таблиц и прочего говна.

«Когда всё, что у тебя есть, это член, всё вокруг выглядит как анус».

Не знаю почему, но вспомнилось.

hateyoufeel ★★★★★
() автор топика
Ответ на: комментарий от Turbid

Сименсы, Эриксоны и тому подобные - это куча разных контор, причем в одной даже у уборщицы - степень MIT, а в другой - генеральный директор, какой-нибудь Заебиджан Ебальдурай и в подчиненных половина его деревни. Просто задачи решают разные и на совершенно разном уровне.

bdrbt
()
Ответ на: комментарий от hateyoufeel

В моём ВУЗе (один из ведущих в РФ лол) основной мантрой было чтобы «студент был всё время за%*?н»

А можно поинтересоваться, в каком конкретно?

Werenter ★★★
()
Ответ на: комментарий от gns

Ну доцентом же остался. Научное звание же никто не отнимал :)

Это да.

cumvillain
()
Для того чтобы оставить комментарий войдите или зарегистрируйтесь.