Хорошо бы вкратце давать пояснения что расположено по ссылке, в частности неясно что такое "seL4".

seL4: В 2006 году началась разработка микроядра третьего поколения, получившего название «seL4»

Отредактировано atzx (2019-06-22 19:23:18)

Там перечислено:

Переполнения буфера, разыменование нулевых указателей, отсутствие ошибок с указателями, отсутствие утечек памяти, отсутствие числовых переполнений, неопределённое поведение.

Ну, это в общем-то достаточно негусто и не гарантирует неуязвимость данной системы. При этом переполнения буфера можно исключить полностью за счёт выбора другого ЯП, разыменование нулевых указателей - это один из возможных способов сигнализировать об ошибке. Если мы сигнализируем об ошибке иным способом, то это не делает нашу программу абсолютно надёжной. Например, можно вместо простого a = *some_pointer писать

if (!some_pointer) {
  exit(1)
};
a = *some_pointer;

Да, разыменования нулевого указателя не будет. Но программа может неожиданно завершить свою работу, а мы в это время как раз летим на самолёте под управлением этой программы (я читал про центральный мозг, который хотят (прости господи, матерное слово на ум навернулось) наши продвинутые специалисты устанавливать в самолёты. А ведь даже у человека есть отдельный головной и спинной мозг и явно есть какие-то автономные мозги у отдельных органов, раз человек может жить со сломанным позвоночником. Ну да ладно.

Отсутствие ошибок с указателями - есть в других языках. Отсутствие утечек памяти - это интересно только, если речь идёт о логических утечках памяти. Физических утечек (потеря указателя без free) можно избежать в расте и в языках со сборкой мусора.

Отсутствие числовых переполнений - это действительно круто. Неопределённое поведение - может быть, имеет смысл, хотя я не знаю. Тут для начала нужно понять, какие варианты неопределённого поведения возникли из исторических причин, а какие объективно нужны. Например, состояние гонки - это объективная проблема. А вот использование неинициализированной переменной - это исключительно особенность Си, которая есть не во всех языках.

Соответственно, половина или больше классов ошибок, отсутствие которых они доказали, вообще исчезает при выборе более нормального ЯП.

Отредактировано БудДен (2019-07-10 16:11:08)

тебе википедию процитировать?
"В начале 2012 года было продано более 1.5 миллиарда устройств, оснащённых реализацией микроядра L4"

Куда можно "выйти" из ядра - тоже ещё тот вопрос. В синий экран?

Но это, конечно, если к словам придираться. Так-то понятно, что там return должно быть написано, ну или, страшно сказать, goto.

Отредактировано Лис (2019-07-10 18:32:37)

На безрыбье и рак рыба. Да проверок не много. Но всё же они провели те которые необходимы для ядра.

Основные проблемы ядра это DeadLock при переключении задач и их планировании.
Есть ещё проблема с передачи параметров в ядро там тоже DeadLock может быть.
И переполнение стека.
Переполнение хендлов и утечка ресурсов.

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