seL4: доказательства безопасности завершены для AArch64
SeL4 security proofs now complete on AArch64
Proofcraft объявила о завершении формального доказательства конфиденциальности для микроядра seL4 на архитектуре AArch64. Это последний элемент в стеке доказательств безопасности, который уже включает функциональную корректность и целостность. Таким образом, seL4 теперь математически гарантирует изоляцию приложений, предотвращая несанкционированный доступ к данным. Работа выполнена при поддержке NCSC и укрепляет позиции seL4 как самой защищённой операционной системы.
Этот рубеж завершает формальное доказательство того, что реализация seL4 на AArch64 обеспечивает безопасную изоляцию приложений, работающих поверх неё.