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