Завершено роботу над математичною формальною верифікацією надійності та безпеки роботи мікроядра seL4 на системах з архітектурою набору команд AArch64. Верифікація зводиться до математичного доказу коректності роботи seL4, який свідчить про повну відповідність заданим формальною мовою специфікаціям. Доказ надійності дозволяє використовувати seL4 у критично важливих системах на базі процесорів ARM64, які потребують підвищеного рівня безпеки та гарантують відсутність збоїв.
Спочатку мікроядро seL4 було верифіковано для 32-розрядних процесорів ARM, а пізніше для 64-розрядних процесорів x86 та RISC-V. Верифікація гарантує, що у разі збою в одній частині системи, цей збій не пошириться на іншу систему та її критичні частини. У контексті забезпечення безпеки верифікація підтверджує, що ядро забезпечує належний рівень ізоляції додатків, не дозволяє їм отримати доступ до інформації без авторизації та гарантує, що у разі компрометації вторинних додатків атака не пошириться на критичні важливі додатки.
Архітектура мікроядра seL4 примітна виносом частин для управління ресурсами ядра в простір користувача та застосування для таких ресурсів тих самих засобів розмежування доступу, як для ресурсів користувача. Мікроядро не надає готових високорівневих абстракцій для керування файлами, процесами, мережевими з'єднаннями тощо, натомість воно надає лише мінімальні механізми для керування доступом до фізичного адресного простору, переривань і ресурсів процесора. Високорівневі абстракції та драйвери для взаємодії з обладнанням реалізуються окремо поверх мікроядра у формі завдань, що виконуються на рівні користувача. Доступ таких завдань до наявних у мікроядра ресурсів організується через визначення правил.
Джерело: opennet.ru
