Выполнена формальная верификация безопасности микроядра seL4 для архитектуры AArch64

Завершена работа над математической формальной верификацией надёжности и безопасности работы микроядра seL4 на системах с архитектурой набора команд AArch64. Верификация сводится к математическому доказательству корректности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и гарантирующих отсутствие сбоев.

Изначально микроядро seL4 было верифицировано для 32-разрядных процессоров ARM, а позднее для 64-разрядных процессоров x86 и RISC-V. Верификация гарантирует, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и её критические части. В контексте обеспечения безопасности верификация подтверждает, что ядро обеспечивает должный уровень изоляции приложений, не позволяет им получить доступ к информации без авторизации и гарантирует, что в случае компрометации вторичных приложений, атака не распространится на критические важные приложения.

Архитектурата на микроядрото seL4 е забележителна с изнасянето на частите за управление на ресурсите на ядрото в пространството на потребителя и приложението на същите средства за разграничаване на достъпа за тези ресурси, както за потребителските ресурси. Микроядрото не предоставя готови високоуредени абстракции за управление на файлове, процеси, мрежови съединения и т.н., вместо това то предлага единствено минимални механизми за управление на достъпа до физическото адресно пространство, прекъсванията и ресурсите на процесора. Високоуредени абстракции и драйвери за взаимодействие с хардуера се реализират отделно над микроядрото под формата на задачи, изпълнявани на потребителско ниво. Достъпът на тези задачи до ресурсите, налични на микроядрото, се организира чрез определяне на правила.

Източник: opennet.ru