RISC-V проверил микроядро seL4 на своих процессорах RV64

Фонд RISC-V объявил, что подтвердил как работает микроядро seL4 в системах с архитектура набора команд РИСК-V. В котором процесс проверки сводится к математическому тесту надежности seL4, который указывает на полное соответствие спецификациям, указанным на формальном языке.

Тестирование надежности позволяет использовать seL4 в критически важных системах на базе процессоров RISC-V RV64, что требует более высокого уровня надежности и не гарантирует отказа.

Разработчики программного обеспечения, работающие на ядре 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.

О тестировании микроядра seL4

Изначально микроядро seL4 был проверен для 32-битных процессоров ARM, y позже для 86-битных процессоров x64.

Замечено, что сочетание открытой аппаратной архитектуры RISC-V с открытым микроядром seL4 выйдет на новый уровень безопасностипоскольку компоненты оборудования в будущем также могут быть полностью проверены, чего невозможно достичь для проприетарных аппаратных архитектур.

Когда мы проверяем seL4, мы должны предполагать, что оборудование работает правильно (то есть, как указано). Это предполагает, что в первую очередь существует недвусмысленная спецификация, что характерно не для всего оборудования. 

Но даже если такая спецификация существует и носит формальный характер (то есть оформленная в математический формализм, который поддерживает математические рассуждения о ее свойствах), как мы узнаем, что она действительно отражает поведение оборудования? 

В действительности мы можем быть уверены, что это не так. Аппаратное обеспечение не отличается от программного обеспечения тем, что оба содержат ошибки.

Но наличие открытого ISA имеет преимущества, выходящие за рамки бесплатного использования. Во-первых, он позволяет реализовывать оборудование с открытым исходным кодом.

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

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

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