Завершена работа над математической формальной верификацией надёжности и безопасности работы микроядра seL4 на системах с архитектурой набора команд AArch64. Верификация сводится к математическому доказательству корректности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и гарантирующих отсутствие сбоев.
Изначально микроядро seL4 было верифицировано для 32-разрядных процессоров ARM, а позднее для 64-разрядных процессоров x86 и RISC-V. Верификация гарантирует, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и её критические части. В контексте обеспечения безопасности верификация подтверждает, что ядро обеспечивает должный уровень изоляции приложений, не позволяет им получить доступ к информации без авторизации и гарантирует, что в случае компрометации вторичных приложений, атака не распространится на критические важные приложения.
seL4 mikrokernel'i arhitektuur paistab silma selle poolest, et osad tuumast, mis haldavad ressursside haldamist, on viidud kasutajaruumis ja nende ressursside jaoks kasutatakse samu juurdepääsukontrolli vahendeid nagu kasutajaressursside jaoks. Mikrokernel ei paku valmis kõrgtasemel abstraktsioone failide, protsesside, võrguühenduste jne haldamiseks, vaid ainult minimaalset mehhanismide kogumit füüsilise aadressiruumi, katkestuste ja CPU ressursside haldamiseks. Kõrgtasemel abstraktsioonid ja seadme draiverid, mis suhtlevad riistvaraga, rakendatakse eraldi mikrokernel'i peal ülesannete kujul, mis töötavad kasutajaruumis. Selliste ülesannete juurdepääs mikrokernel'il olevatele ressurssidele organiseeritakse reeglite määratlemise kaudu.
Allikas: opennet.ru
