Завершена работа над математической формальной верификацией надёжности и безопасности работы микроядра seL4 на системах с архитектурой набора команд AArch64. Верификация сводится к математическому доказательству корректности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и гарантирующих отсутствие сбоев.
Изначально микроядро seL4 было верифицировано для 32-разрядных процессоров ARM, а позднее для 64-разрядных процессоров x86 и RISC-V. Верификация гарантирует, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и её критические части. В контексте обеспечения безопасности верификация подтверждает, что ядро обеспечивает должный уровень изоляции приложений, не позволяет им получить доступ к информации без авторизации и гарантирует, что в случае компрометации вторичных приложений, атака не распространится на критические важные приложения.
Die Architektur des Mikro-Kernels seL4 zeichnet sich dadurch aus, dass Teile zur Verwaltung der Kernressourcen in den Benutzermodus ausgelagert werden, und dass dieselben Zugriffsteuerungsmechanismen für diese Ressourcen verwendet werden wie für Benutzerräume. Der Mikro-Kernel bietet keine fertigen, hochrangigen Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw.; stattdessen stellt er lediglich minimale Mechanismen zur Verfügung, um den Zugriff auf den physischen Adressraum, Interrupts und CPU-Ressourcen zu steuern. Hochrangige Abstraktionen und Treiber zur Interaktion mit der Hardware werden separat über dem Mikro-Kernel in Form von Aufgaben implementiert, die im Benutzermodus ausgeführt werden. Der Zugriff dieser Aufgaben auf die Ressourcen des Mikro-Kernels erfolgt durch die Festlegung von Regeln.
Quelle: opennet.ru
