Исходное сообщение
"Микроядро seL4 математически верифицировано для архитектуры ..." Отправлено erthink, 10-Июн-20 17:48
> > при необходимости > ОЙ КАК ТОЛСТО... Видимо стоит уточнить для местных ихпёртов, которые (УВЫ) не читали, но осуждают. Логика ядра верифицирована, но в реальных применениях это мало что даёт (смотрим на факапы Qualcomm и т.п.): - без верификации всех "ассемблерных вставок" при использовании на конкретной платформе. - без верификации логики служб и приложений (с учетом взаимодействия и средств контроля ОС). Соответственно, "при необходимости" - относилось к верификации примитивов (связанных с "посадкой" ОС на какую-то конкретную платформу) и к верификации приложений. TL;DR Kaspersky OS предлагает контроль взаимодействия отдельных компонентов (служб, приложений) как с ядром, так и между собой - это принципиальное отличие от L4. Грубо говоря, принципы безопасности/надежности L4 распространяются с ядра на все приложения, службы и систему в целом.