Завершена работа над математической формальной верификацией надёжности и безопасности работы микроядра seL4 на системах с архитектурой набора команд AArch64. Верификация сводится к математическому доказательству корректности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров ARM64, требующих повышенного уровня безопасности и гарантирующих отсутствие сбоев.
Изначально микроядро seL4 было верифицировано для 32-разрядных процессоров ARM, а позднее для 64-разрядных процессоров x86 и RISC-V. Верификация гарантирует, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и её критические части. В контексте обеспечения безопасности верификация подтверждает, что ядро обеспечивает должный уровень изоляции приложений, не позволяет им получить доступ к информации без авторизации и гарантирует, что в случае компрометации вторичных приложений, атака не распространится на критические важные приложения.
Arkitektura e mikrogrimcës seL4 shquhet për ndarjen e pjesëve për menaxhimin e burimeve të kernels në hapësirën përdoruese dhe përdorimin e të njëjtave mjete ndarjeje për këto burime si për burimet përdoruese. Mikrogrimca nuk ofron abstraksione të gatshme me nivele të larta për menaxhimin e skedarëve, procedurave, lidhjeve rrjetore etj., por ofron vetëm mekanizma minimalë për menaxhimin e qasjes në hapësirën fizike adresuese, interruptet dhe burimet e procesorit. Abstraksionet e nivelit të lartë dhe drejtuesit për ndërveprimin me pajisjet realizohen veçmas mbi mikrogrimcë në formën e detyrave që ekzekutohen në nivelin përdorues. Qasja e këtyre detyrave në burimet ekzistuese të mikrogrimcës organizohet përmes përcaktimit të rregullave.
Burimi: opennet.ru
