Викиновости

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

10 июня 2020 года

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

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

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

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

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

Источники править

 
 
Creative Commons
Эта статья содержит материалы из статьи «Микроядро seL4 математически верифицировано для архитектуры RISC-V», опубликованной OpenNET и распространяющейся на условиях лицензии Creative Commons Attribution (CC BY) — указание автора, источник и лицензию.
 
Эта статья загружена автоматически ботом NewsBots и ещё не проверялась редакторами Викиновостей.
Любой участник может оформить статью: добавить иллюстрации, викифицировать, заполнить шаблоны и добавить категории.
Любой редактор может снять этот шаблон после оформления и проверки.

Комментарии

Викиновости и Wikimedia Foundation не несут ответственности за любые материалы и точки зрения, находящиеся на странице и в разделе комментариев.



Источник — https://ru.wikinews.org/w/index.php?title=Микроядро_seL4_математически_верифицировано_для_архитектуры_RISC-V&oldid=16141183