Организация 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
