RISC-V перевірив мікроядро seL4 на своїх процесорах RV64

Фонд RISC-V оголосив, що перевірив як працює мікроядро seL4 в системах з архітектура набору інструкцій RISC-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І пізніше для x86 64-розрядних процесорів.

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

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

Але навіть коли така специфікація існує, і вона є формальною (тобто перетвореною на математичний формалізм, що підтримує математичні міркування про її властивості), як ми можемо знати, що вона насправді фіксує поведінку обладнання? 

Реальність така, що ми можемо бути впевнені, що це не так. Апаратне забезпечення нічим не відрізняється від програмного забезпечення тим, що обидва вони глючать.

Але наявність відкритого ISA має переваги, які виходять за рамки безкоштовної оплати. Один з них полягає в тому, що він дозволяє реалізувати обладнання з відкритим кодом.

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

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

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