Завершена формальная верификация микроядра seL4 для архитектуры AArch64

Разработчики завершили масштабный проект математической формальной верификации надежности и безопасности микроядра seL4 для 64-битной процессорной архитектуры AArch64.

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

Успешное подтверждение надежности открывает возможности для применения seL4 в критически важных системах на базе процессоров ARM64, включая аэрокосмическую отрасль, медицинское оборудование, автомобильную электронику и оборонные комплексы.

Linux / Линукс 🥸