Завершена работа над математической формальной верификацией надёжности и безопасности работы микроядра seL4 на системах с архитектурой набора команд AArch64. Верификация сводится к математическому доказательству корректности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и гарантирующих отсутствие сбоев. Изначально микроядро seL4 было верифицировано для 32-разрядных процессоров ARM, а позднее для 64-разрядных процессоров x86 и RISC-V. Верификация гарантирует, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и её критические части. В контексте обеспечения безопасности верификация подтверждает, что ядро обеспечивает должный уровень изоляции приложений, не позволяет им получить доступ к информации без авторизации и гарантирует, что в случае компрометации вторичных приложений, атака не распространится на критические важные приложения. Архитектура микроядра seL4 примечательна выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Микроядро не предоставляет готовых высокоуровневых абстракций для управления файлами, процессами, сетевыми соединениями и т.п., вместо этого оно предоставляет лишь минимальные механизмы для управления доступом к физическому адресному пространству, прерываниям и ресурсам процессора. Высокоуровневые абстракции и драйверы для взаимодействия с оборудованием реализуются отдельно поверх микроядра в форме задач, выполняемых на пользовательском уровне. Доступ таких задач к имеющимся у микроядра ресурсам организуется через определение правил.
Источник: https://www.opennet.ru/opennews/art.shtml?num=66127
Источник: https://www.opennet.ru/opennews/art.shtml?num=66127