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