Насколько безопасна Embox OS?

Finally, seL4/ARM is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees.

https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html

Якобы единственное и неповторимое микроядро реального времени (hard real-time guarantees).

В seL4 ведь всего 10 тысяч строк сорцов, вероятно их не так сложно изучить и сертифицировать на безопасность (если это будет нужно) по сравнению с другими ядрами?

А нафига нам «изучат и сертифицировать микроядро sel4»? Оно же нифига не умеет, кроме как переключать процессы? Безопасность чего вы собрались сертифицировать? Сети нет, файловой системы нет, интерфейса пользователя нет даже текстового! Все это отдельные процессы в пространстве пользователя. Толку от того что микроядро продолжит работать, если упал процесс файловой системы.

В Genode уже есть готовые наработки драйверов.

Наверно что-то можно было бы выбрать оттуда?

Кстати, как на данный момент обстоят дела с поддержкой OpenSSH в Embox?

Безопасность чего вы собрались сертифицировать? Сети нет, файловой системы нет, интерфейса пользователя нет даже текстового!

Воды нет, растительности нет, населена роботами. Слава роботам!

Сети нет, файловой системы нет

В Genode ведь есть?

интерфейса пользователя нет даже текстового!

А зачем он? Мне лично интересны серверные безопасные оси, а не десктоп.

Не проще ли сделать безопасный десктоп из Trinity DE на Core2, путем выдергивания Internet шнурка?

В Genode Sculpt кстати есть какой-то GUI :) Но там пока нормально работает вроде бы только микроядро NOVA, а не seL4.

ты наверное не мне отвечай :) я только процитировал

В Genode ведь есть?

Так ты определись - размер исходников чего будем мерять? Микро-ядра sel4 или Genode? Размер исходников Genode много больше «10000 строк».

А зачем он? Мне лично интересны серверные безопасные оси, а не десктоп.

А как без интерфейса пользователя (командной строки хотя бы) ты будешь устанавливать и настраивать свой «безопасный сервер»?

Так ты определись - размер исходников чего будем мерять? Микро-ядра sel4 или Genode?

Genode ведь работает за пределами микроядра, значит его безопасность выше хотя за счет изоляции отдельных компонентов?

The formal proof of functional correctness implies the absence of whole classes of common programming errors. Provided our assumptions above are true, some of these excluded common errors are:

Buffer overflows: buffer overflows are a classic security attack against operating systems, trying to make the software crash or even to inject malicious code into the cycle. We have proved that no such attack can be successful on seL4. Null pointer dereferences: null pointer dereferences are another common issue in the C programming language. In applications they tend to lead to strange error messages and lost data. In operating systems they will usually crash the whole system. They do not occur in seL4. Pointer errors in general: in C it is possible to accidentally use a pointer to the wrong type of data. This is a common programming error. It does not happen in the seL4 kernel. Memory leaks: memory leaks occur when memory is requested, but never given back. The other direction is even worse: memory could be given back, even though it is still in use. Neither of these can happen in seL4. Arithmetic overflows and exceptions: humans and mathematics usually have a concept of numbers that can be arbitrarily big. Machines do not, they need to fit them into memory, usually into 32 or 64 bits worth of storage. Machines also generate exceptions when you attempt to do things that are undefined like dividing by zero. In the OS, such exceptions would typically crash the machine. This does not occur in seL4. Undefined behaviour: there are many static analysis and verification tools that check for the absence of undefined behaviour in C. Our proof explicitly checks that no such undefined behaviour occurs.

How are resources managed and protected in seL4?

The key idea in seL4 is that all resource management is done in userland. Access to and control over resources is controlled by capabilities. The kernel after boot hands control over all free resources to userland, and after that will never do any memory management itself. It has no heap, just a few global variables, a strictly bounded stack, and memory explicitly provided to it by userland.

А как без интерфейса пользователя (командной строки хотя бы) ты будешь устанавливать и настраивать свой «безопасный сервер»?

Я предлагал на базе seL4+Genode делать Embox.

А Embox в свою очередь, насколько я понимаю, как раз предлагает какой-то CLI и вероятно SSH?

Я предлагал на базе seL4+Genode делать Embox.

Исходники есть - делай!

В Genode Sculpt кстати есть какой-то GUI :) Но там пока нормально работает вроде бы только микроядро NOVA, а не seL4.

Т.е. ты предлагаешь сначала «починить» Genode для работы поверх sel4?

У тебя логика хромает - если Genode плохо работает на sel4, то зачем брать sel4 для Embox? Чтобы он тоже перестал «нормально работать»?

Исходники есть - делай!

Какая связь одного с другим? По твоей логике при наличии всего того богатства open-source на Github мне только и нужно, что кодить все подряд?

Т.е. ты предлагаешь сначала «починить» Genode для работы поверх sel4? - если Genode плохо работает на sel4, то зачем брать sel4 для Embox? Чтобы он тоже перестал «нормально работать»?

Я пока не знаю, почему выбрали микроядро NOVA вместо seL4 для Sculpt. Речь шла про Sculpt (граф. оболочка вокруг Genode), а не Genode standalone для создания других осей.

Genode is a free and open-source software operating system framework consisting of a microkernel abstraction layer and a set of user space components.

У тебя логика хромает

Скорее ты не понимаешь разницу между Genode и Sculpt.

Кстати, IMHO неплохо было бы Embox объединить усилия с Завалишиным, который занимается PhantomOS:

https://en.wikipedia.org/wiki/Phantom_OS

http://phantomos.org/

Чтобы у нас появилась действительно безопасная микроядерная ось с одной стороны, и хотя бы с частичной поддержкой POSIX/Linux API с другой и одновременно удобной для ООП программирования на Java и C#.

POSIX environment. There is (very simple) POSIX subsystem in Phantom. It is not persistent (yet?). As an example, Quake application is compiled for POSIX subsystem.

«Основная версия операционной системы готова к пилотным проектам. Версия для Genode пока не завершена, именно над ней и идет работа. По плану в конце года она будет готова к применению», – заявил Завалишин в разговоре с CNews.

Портированием на Genode занимается специальная рабочая группа, созданная в 2019 г. на базе «Иннополиса».

Процедура предусматривает сращивание среды исполнения программ этой операционной системы с программным ядром фреймворка, имеющим возможность поддержки многочисленных аппаратных платформ (x86, ARM, RISC-V и др.) и гипервизоров, включая формально верифицированную систему seL4. Как подчеркнул глава DZ Systems, это позволит упростить и ускорить реализацию и доработку «Фантома». Также это поможет сделать ОС более надежной и безопасной, адаптировать ее к реальному использованию в промышленной сфере.

https://www.cnews.ru/news/top/2022-01-21_rossiyane_sozdali_unikalnuyu

http://www.freezepage.com/1652506032ERVHMWOTDP

В результате получился бы неплохой конкурент для проприетарной (а значит сомнительной с точки зрения безопасности) KasperskyOS:

https://ru.wikipedia.org/wiki/KasperskyOS

Почему бы ...

Почему бы не спросить у основателя Embox abondarev ?

В seL4 ведь всего 10 тысяч строк сорцов, вероятно их не так сложно изучить и сертифицировать на безопасность (если это будет нужно) по сравнению с другими ядрами?

Сколько программ ты сертифицировал у ФСТЭКа?

Я предлагал на базе seL4+Genode делать Embox.

Кому предлагал? Писал в чат Embox-а?

Сколько ты коммитов сделал в https://github.com/embox/embox ?

Почему бы не спросить у основателя Embox abondarev ?

Приглашаю его в эту ветку :)

Сколько ты коммитов сделал в https://github.com/embox/embox ?

Зачем мне делать коммиты?

https://archive.fosdem.org/2021/schedule/event/microkernel_sel4_report/attach...

seL4 System development
RFCs for seL4 Core, seL4 Core Platform
soon: RFC for seL4 driver framework

Кстати, почему обсуждение в этой теме открыто не для всех ? :(

Хм, не знаю, но возможно в текущей политической систуации, может очень большой срач начаться :(

Кстати, как на данный момент обстоят дела с поддержкой OpenSSH в Embox?

OpenSSH нет, но есть dropbear (реализация ssh).

Почему бы не попытаться делать Embox или его форк на базе безопасного микроядра типа seL4 + возможно на части Genode?

Разные цели. Embox предлагает решение части проблем у Линукс. Это не обязательно микроядро, да и микроядер уже много.

Genode тоже имеет другие цели, хотя действительно, если говорить, об генерации ядра, но это очень похоже на идею Embox, делать ОС под задачу. Но опять же генерация ядра (на самом деле целого дистрибутива с сетью файловой системой библиотеками и т.д.) является решением, а не целью Embox.

То есть, я к тому, что почему бы не сделать форк Embox на Embox:) Если нужны какие то специфичные требования. В последнее время многие предлагают сделать свою ОС (лицензия позволяет, разработчики есть) хотя бы для критически важной инфраструктуры.

А Embox в свою очередь, насколько я понимаю, как раз предлагает какой-то CLI и вероятно SSH?

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

Собственно мы общаемся с Дмитрием Завалишиным и давно хотим объединить усилия, но пока не очень понятно как это можно сделать на практике.

об генерации ядра, но это очень похоже на идею Embox, делать ОС под задачу.

Разве это не Unikernel?

http://unikernel.org/projects/

https://en.wikipedia.org/wiki/Unikernel

Хм, не знаю, но возможно в текущей политической систуации, может очень большой срач начаться :(

Из-за вот таких:

переход на российский Linux: грандиозный успех, но... (комментарий)

некомпетентных с технической точки зрения клоунов?

Сила есть ума не надо, как говорится. Только увы, давно уже все с точностью до наоборот, тем более в 2022-ом году.

Может быть, хотя бы залинковать эту ветку в вашей, чтобы привлечь заинтересованных к обсуждению?

Вы имеете в виду добавить комментарий в новость про соглашение между Embox и МЦСТ или что то другое? Если комментарий, то добавил и поставил ссылку на эту ветку

Благодарю.

Разные цели. Embox предлагает решение части проблем у Линукс. Это не обязательно микроядро, да и микроядер уже много.

Судя по:

https://github.com/embox/embox

Embox is a configurable RTOS designed for resource constrained and embedded systems.

seL4 - ядро как раз для подобных систем, уникальное своей надежностью и безопасностью, аналоги которому вы наврядли найдете среди других микроядер.

VoIP phone on STM32F7Discovery based on PJSIP project
Qt on STM32F7Discovery
OpenCV on STM32F769i board
A lot of programming languages available: Python, Lisp, Java (phoneme), TCL, Ruby, Lua
SSHD based on Dropbear project
Mesa3d
Quake3
zeromq, qpid

Для осей на базе seL4, которые пока относительно в вакууме IMHO, как раз перечисленного вами и не хватает :)

Embox main idea is using Linux software without Linux.

Именно это и нужно для оси на базе seL4.

Когда-то пытались портировать ядро Hurd для GNU дистрибутивов на ядро L4:

https://news.slashdot.org/story/05/02/04/028220/first-program-executed-on-l4-...

«The GNU Project was working on a new OS kernel called HURD from 1990, using the GNU Mach microkernel. However, when HURD-Mach was able to run a GUI and a browser, the developers decided to start from scratch and port the project to the high-performance L4 microkernel.

Но увы, они не шмогли ...

Кстати, почему обсуждение в этой теме открыто не для всех ? :(

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

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

Ааа, это те, которые пиарят зонды тех, имя кого произносить нельзя ? :)

Именно это и нужно для оси на базе seL4.

Ну может быть для базы seL4 именно это и нужно, но у Embox есть свой планировщик, который можно перестраивать в зависимости от задач, как и все остальное. Если делать только чистое микроядро, то невозможно (или ну очень сложно) добиться результатов как у Embox. То есть, в одних местах это прекрасные свойства, но в других, будет надежно но медленно, графика например на микроядре говорят очень сильно тормозит (перекачка памяти нужна).

Ну и да, конечно мы знаем про seL4, и про Minix, и про GNU Hurd.

медленно

seL4 - одно из самых скоростных микроядер.

графика например на микроядре говорят очень сильно тормозит (перекачка памяти нужна)

Хотя бы без графики, для серверных задач.

Хотя бы дополнительный форк Embox, оставив в основном все как есть. Может быть, возможная какая-то универсальность Embox типа Genode или GNU (Linux vs Hurd), чтобы ядро было на выбор?

Просто не очень понятно:

1) Как обеспечить безопасность без микроядра?

2) Зачем еще один микролинукс частично совместимый с GNU софтом, в котором как обычно не решены проблемы безопасности ?

1. Как обеспечить безопасность без микроядра?

Ну как бы надежность (наверное про нее речь) может быть обеспечена разными способами, один (довольно эффективный в некотором случае) это принцип микроядра. Но повторюсь есть куча микроядерных ОСей, смысл делать еще одну? И опять, в Embox есть все, чтобы сделать микроядерных вариант!

Может быть, возможная какая-то универсальность Embox типа Genode или GNU (Linux vs Hurd), чтобы ядро было на выбор?

Хм, об этом не думали. По идее ядро, как и все остальное конфигурируется чтобы получить нужные свойства, это в какой то степени можно рассматривать как выбор ядра.

Ну как бы надежность (наверное про нее речь) может быть обеспечена разными способами, один (довольно эффективный в некотором случае) это принцип микроядра.

Речь в первую очередь про безопасность, т.е. защищенность от взлома через дыры в дровах и оборудовании (не через зонды, а именно ошибки):

Насколько безопасна Embox OS? (комментарий)

Но повторюсь есть куча микроядерных ОСей, смысл делать еще одну?

О том и речь, что микроядер, сравнимых по безопасности с seL4, на сегодняшний день нет. Его разработка, включая остальные ядра Liedtke (предшественники L1, L2, L3 и собственно L4), заняла около 30 (тридцати) лет:

https://en.wikipedia.org/wiki/L4_microkernel_family

И опять, в Embox есть все, чтобы сделать микроядерных вариант!

Вы хотите повторить их успех со своим мегабюджетом?

Ядро seL4 полностью open source. Аналогов нет в области безопасности на самом деле и это не пустые слова.

IMHO интегрировать готовое намного проще, и найти зловреда в 10K LoC (объем сорцов seL4) намного проще, чем в монолите Linux на 30.000+ K LoC

Разница в 3 тысячи раз. Дрова для seL4 конечно добавят сколько то тысяч LoC, но они работают в другом контексте от основного ядра.

Вы хотите повторить их успех со своим мегабюджетом?

Конечно нет. Если бы идея заключалась в создании безопасной ОС, обязательно нужно было рассмотреть seL4. И конечно мы рассматриваем и изучаем опыт других проектов. Но идея Embox в том что прекрасный Linux имеет несколько проблемных моментов (гиганский объем кода например) и мы пошли путем вынесения в статику максимального количества проверок и получили свойства которые интересны в практической плоскости. Вы же сами сказали, что само ядро не особо интересно, драйвера нужны прикладное ПО…

Конечно нет. Если бы идея заключалась в создании безопасной ОС, обязательно нужно было рассмотреть seL4. И конечно мы рассматриваем и изучаем опыт других проектов. Но идея Embox в том что прекрасный Linux имеет несколько проблемных моментов (гиганский объем кода например) и мы пошли путем вынесения в статику максимального количества проверок и получили свойства которые интересны в практической плоскости.

А разве нет других уже готовых микролинуксов с сильно обезжиренным ядром? К примеру:

https://en.m.wikipedia.org/wiki/Embeddable_Linux_Kernel_Subset

https://en.wikipedia.org/wiki/LibreCMC

https://en.wikipedia.org/wiki/Emdebian_Grip

https://en.wikipedia.org/wiki/OpenEmbedded

https://web.archive.org/web/20181113230737/http://www.uclinux.org/

https://en.m.wikipedia.org/wiki/ΜClinux

https://ru.wikipedia.org/wiki/Picotux

и т.п.

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

Вы же сами сказали, что само ядро не особо интересно, драйвера нужны прикладное ПО…

Драйвера для seL4 уже есть в Genode, можно вероятно что-то было бы попытаться портировать из ваших готовых ядер.

Не хватает в Genode именно слоя совместимости с Linux API, это как раз то, что развивается у вас. POSIX кстати у них есть в какой-то степени. IMHO лучше было бы сосредоточиться на этаком LINE (по аналогии с WINE :), который работал бы на Genode.

А также поверх этого сделать бы вот такое:

Идея проекта безопасного гипервизора или эмулятора

А разве нет других уже готовых микролинуксов с сильно обезжиренным ядром?

не знаю почему Вы их называете микролинуксами и почему ядро обезжиренное. обычные ядра, разве что uCLinux, но это NOMMU режим ядра по сути дела. Да они сконфигурированны с более скромными требованиями чем десктопы, но сути дела это не меняет. Embox запускается на 32кб ПЗУ и 4 кб ОЗУ https://habr.com/ru/company/embox/blog/537408/

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

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

Embox увеличивает безопасность, поскольку внешний код (не для этой конфигурации ОС не будет работать) сколько бы вы там не делали рам дисков, запустить код вы сможете только если это разрешено, да и по условным сисколам это будет не совместимо. Ну и да, один из вариантов это радикальное уменьшение количество строчек кода, причем не только в условном ядре.

IMHO лучше было бы сосредоточиться на этаком LINE (по аналогии с WINE :), который работал бы на Genode.

:) Ну кто же мешает, сосредотачивайтесь:)

Embox запускается на 32кб ПЗУ и 4 кб ОЗУ

А чтобы запустить вот это:

VoIP phone on STM32F7Discovery based on PJSIP project
Qt on STM32F7Discovery
OpenCV on STM32F769i board
A lot of programming languages available: Python, Lisp, Java (phoneme), TCL, Ruby, Lua
SSHD based on Dropbear project
Mesa3d
Quake3
zeromq, qpid

сколько нужно ОЗУ?

:) Ну кто же мешает, сосредотачивайтесь:)

Я не системный программист, а скриптописатель.

Хотя в юности увлекался C++ и даже немного асмом x86.

сколько нужно ОЗУ? Сильно по разному.

• VoIP phone on STM32F7Discovery Влезает во внутреннюю память МК 380кб, никакой uCLinux не влезает, а сверху uCLinux еще нужен PJSIP ну и другие приложения и либы.

С другими примерами все конечно хуже… Но это уже не ОС, а сами приложения жирные, с Линукс будет тоже самое, плюс Линукс

У нас идея, подумать что нужно в системе и только это и оставить…

Я не системный программист, а скриптописатель.

А я системный. Возможно у меня больше опыта и я понимаю почему не прошел подход, взять микроядро и сделать безопасную ОС? Ну не просто же так просто никто не хочет делать по хорошему?:)

А я системный. Возможно у меня больше опыта

Я даже не пытаюсь оспорить ваши знания и умения в качестве разработчика RTOS.

не прошел подход, взять микроядро и сделать безопасную ОС?

Все таки Debian GNU и GUIX позволяют вместо ядра Linux использовать микроядро Hurd, верно? Аналогично альтернативному ядру kFreeBSD.

Ну не просто же так просто никто не хочет делать по хорошему?:)

К сожалению попытки с микроядрами M4 оказались менее успешными. Ходят слухи, что им просто не хватило квалификации, мол нужные спецы стоят уж очень дорого, а делать просто так немотивированы. Я даже не исключаю, что их работодатели (вероятно из военных лабораторий) очень хорошо демотивировали их помогать свободным community для интеграции M4 с ширпотреб осями в своих NDA и других трудовых соглашениях.

Но это уже не ОС

Embox запускается на 32кб ПЗУ и 4 кб ОЗУ

Слой эмуляции Linux сколько ОЗУ у вас потребляет в среднем от и до?

Слой эмуляции Linux сколько ОЗУ у вас потребляет в среднем от и до?

Нету слоя эмуляции:) Есть библиотеки совместимости POSIX (ну и немного Линукс), но и их нет, это просто нетивное API, и все конфигурируется. То есть, если нужны сигналы, нужно предусмотреть в структуре процесса потока соотвествующие поля, ну и так далее.

Я же говорю, мы не писали очередную ОС, потому что остальные написаны не нами, у нас были какие то идеи, которые трудно (или невозможно) было сделать с текущим подходом. Берем микроядро, берем стандартную библиотеку, потом пакеты и т.д.

Берем микроядро, берем стандартную библиотеку, потом пакеты и т.д.

Вероятно ваше ядро микро по размеру, но не по архитектуре?

https://blogs.windriver.com/wind_river_blog/2021/05/monolithic-kernel-or-micr...

У вас с архитектурной точки зрения монолитное ядро (как и Linux, BSD, Solaris, etc.)?

Нету слоя эмуляции:) Есть библиотеки совместимости POSIX (ну и немного Линукс), но и их нет, это просто нетивное API, и все конфигурируется. То есть, если нужны сигналы, нужно предусмотреть в структуре процесса потока соотвествующие поля, ну и так далее.

Я имел ввиду что-то похожее на:

https://wiki.freebsd.org/Linuxulator

Т.е. у вас любые Linux программы нужно самостоятельно портировать. В принципе понятно, что Unikernel вероятно обычно не позволяет запускать дополнительные не включенные в него executables, хотя с внешних носителей, может быть, и позволяет при наличии механизма указания пути (наверно это был бы уже минус к безопасности)?

У вас с архитектурной точки зрения монолитное ядро (как и Linux, BSD, Solaris, etc.)?

Ну пусть будет монолитное :)

Т.е. у вас любые Linux программы нужно самостоятельно портировать.

Да, в обычном режиме бинарной совместимости нет. Есть попытка добавить LKL https://github.com/embox/embox/pull/2561, но пока не понятно что из этого выйдет. И имеет ли это смысл.

В принципе понятно, что Unikernel вероятно обычно не позволяет запускать дополнительные не включенные в него executables, хотя с внешних носителей, может быть, и позволяет при наличии механизма указания пути (наверно это был бы уже минус к безопасности)?

Да, есть идеи близкие к unikernel, но опять же на полностью. Скорее из Embox можно прекрасный unikernel сделать, причем с множеством приложений.

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

Ну пусть будет монолитное :)

А оно по определению менее безопасное, чем архитектурно микроядро, тем более такое как seL4, которое сейчас используют в General Dynamics для различных очень critical cases.

А оно по определению менее безопасное, чем архитектурно микроядро, тем более такое как seL4, которое сейчас используют в General Dynamics для различных очень critical cases.

Я тоже так думаю! Но это касается только ядра, а нужно рассматривать систему в целом!