Микроядро seL4 математически верифицировано для архитектуры RISC-V

Организация RISC-V Foundation сообщила о верификации работы микроядра seL4 на системах с архитектурой набора команд RISC-V. Верификация сводится к математическому доказательству надёжности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров RISC-V RV64, требующих повышенного уровня надёжности и гарантирующих отсутствие сбоев. Разработчики ПО, работающего поверх ядра seL4, могут быть полностью уверены, что в случае сбоя в одной части системы, данный сбой не распространится на остальную систему и, в частности, её критические части.

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

При верификации seL4 предполагается, что оборудование работает как заявлено и спецификация полностью описывает поведение системы, но на деле оборудование не избавлено от ошибок, что хорошо демонстрируется всплывающими регулярно проблемами в механизме спекулятивного выполнения инструкций. Открытые аппаратные платформы упрощают интеграцию связанных с безопасностью изменений — например, для блокирования всех возможных каналов утечки по сторонним каналам, в которых гораздо эффективней избавиться от проблемы аппаратно, чем пытаться искать обходные пути программно.

Напомним, что ахитектура seL4 примечательна выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Микроядро не предоставляет готовых высокоуровневых абстракций для управления файлами, процессами, сетевыми соединениями и т.п., вместо этого оно предоставляет лишь минимальные механизмы для управления доступом к физическому адресному пространству, прерываниям и ресурсам процессора. Высокоуровневые абстракции и драйверы для взаимодействия с оборудованием реализуются отдельно поверх микроядра в форме задач, выполняемых на пользовательском уровне. Доступ таких задач к имеющимся у микроядра ресурсам организуется через определение правил.

RISC-V предоставляет открытую и гибкую систему машинных инструкций, позволяющую создавать микропроцессоры для произвольных областей применения, не требуя при этом отчислений и не налагая условий на использование. RISC-V позволяет создавать полностью открытые SoC и процессоры. В настоящее время на базе спецификации RISC-V разными компаниями и сообществами под различными свободными лицензиями (BSD, MIT, Apache 2.0) развивается несколько десятков вариантов ядер микропроцессоров, SoC и уже производимых чипов. Поддержка RISC-V присутствует начиная с выпусков Glibc 2.27, binutils 2.30, gcc 7 и ядра Linux 4.15.

Источник: opennet.ru