Микроядро 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.
Источник: http://www.opennet.ru/opennews/art.shtml? num=53129
© OpenNet
