seL4: доказательства безопасности завершены для AArch64
SeL4 security proofs now complete on AArch64
Proofcraft объявила о завершении формального доказательства конфиденциальности для микроядра seL4 на архитектуре AArch64. Это последний элемент в стеке доказательств безопасности, который уже включает функциональную корректность и целостность. Таким образом, seL4 теперь математически гарантирует изоляцию приложений, предотвращая несанкционированный доступ к данным. Работа выполнена при поддержке NCSC и укрепляет позиции seL4 как самой защищённой операционной системы.
Этот рубеж завершает формальное доказательство того, что реализация seL4 на AArch64 обеспечивает безопасную изоляцию приложений, работающих поверх неё.
- StilesCrisis
Скоро выйдет атака по стороннему каналу, которая полностью аннулирует этот результат.
- i_am_a_peasant
Читайте мелкий шрифт: "non-MCS (mixed criticality systems), unicore".
- kvuj
Какие операционные системы используют SeL4? Я знаю о следующих:
- GenodeOS
- LionsOS
- Один китайский автопроизводитель использовал его в качестве гипервизора в своих автомобилях, если я правильно помню.
- Что ещё? Есть ли частные развертывания, о которых вы знаете?
- avadodin
Встраиваемые и военные рынки могут продолжать финансировать их в обозримом будущем, но им нужен нативный seL4/Linux, если они хотят честно заявлять, что улучшают безопасность систем с помощью своей модели возможностей.
Платформы виртуализации с безопасной загрузкой сейчас на каждом шагу.