Исходное сообщение
"Микроядро seL4 математически верифицировано для архитектуры ..." Отправлено erthink, 10-Июн-20 14:50
В своё время L4 было прорывом, но поезд несколько продвинулся за >25 лет. Сейчас же уже есть Kaspersky OS, которая принципиально лучше L4 (конечно IMHO, ибо TL;DR): - тот-же уровень верифицируемости (посредством мат. доказательства) при необходимости. - различные модели безопасности. - поддержка POSIX. - возможность "security by design" для приложений (как сложных наборов компонентов/служб). - также поддержка жесткого реального времени (пока не из каробки, но обещают). Репутация же L4 оказалась "подмочена" дырявостью продуктов Qualcomm.