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

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

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

L'architettura del microkernel seL4 è notevole per l'allocazione delle parti di gestione delle risorse del kernel nello spazio utente, utilizzando gli stessi strumenti di separazione degli accessi per tali risorse come per le risorse utente. Il microkernel non offre astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; al contrario, fornisce solo meccanismi minimi per la gestione dell'accesso allo spazio di indirizzamento fisico, alle interruzioni e alle risorse della CPU. Le astrazioni di alto livello e i driver per l'interazione con l'hardware vengono implementati separatamente sopra il microkernel in forma di task eseguiti a livello utente. L'accesso di tali task alle risorse disponibili del microkernel è organizzato attraverso la definizione di regole.

Fonte: opennet.ru