Организация RISC-V Foundation за верификация на работата на микроядрото в системи с архитектура на командния набор 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
