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