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И позже для 86-битных процессоров x64.

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

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

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

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

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

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

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

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


Содержание статьи соответствует нашим принципам редакционная этика. Чтобы сообщить об ошибке, нажмите здесь.

2 комментариев, оставьте свой

Оставьте свой комментарий

Ваш электронный адрес не будет опубликован. Обязательные для заполнения поля помечены *

*

*

  1. Ответственный за данные: Мигель Анхель Гатон
  2. Назначение данных: контроль спама, управление комментариями.
  3. Легитимация: ваше согласие
  4. Передача данных: данные не будут переданы третьим лицам, кроме как по закону.
  5. Хранение данных: база данных, размещенная в Occentus Networks (ЕС)
  6. Права: в любое время вы можете ограничить, восстановить и удалить свою информацию.

  1.   один из некоторых сказал

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

    Проблема с ARM - это то, что меня пищит, вы уже видели, что случилось с Huawei с санкциями. Я уверен, что для моего RISC-V это гораздо лучшее решение на всех уровнях. На данный момент Huawei уже присмотрелся к нему и, возможно, в будущем у них появится оборудование с этим микро. Если так, то наверняка будет больше компаний, которые его примут, и для меня это было бы идеалом, и, прежде всего, поддержка дистрибутивов, а не только ARM, как это происходит с большинством.

    1.    Грегори Рос сказал

      +10