Компанія Google оголосила про відкриття напрацювань, пов'язаних з проектом KataOS, націленим на створення захищеної операційної системи для вбудованого обладнання. Системні компоненти KataOS написані мовою Rust та виконуються поверх мікроядра seL4, для якого на системах RISC-V надано математичний доказ надійності, що свідчить про повну відповідність коду специфікаціям, заданим формальною мовою. Код проекту відкрито за ліцензією Apache 2.0.
У системі забезпечено підтримку платформ на базі архітектур RISC-V та ARM64. Для симуляції роботи seL4 та оточення KataOS поверх обладнання у процесі розробки використовується фреймворк Renode. Як еталонну реалізацію запропонований програмно-апаратний комплекс Sparrow, що комбінує KataOS із захищеними чіпами на базі платформи OpenTitan. Запропоноване рішення дозволяє поєднати логічно верифіковане ядро операційної системи з апаратними компонентами (RoT, Root of Trust), що заслуговують на довіру, побудованими з використанням платформи OpenTitan і архітектури RISC-V. Крім коду KataOS надалі планується відкриття й решти компонентів Sparrow, включаючи апаратну складову.
Платформа розвивається з огляду на застосування в спеціалізованих чіпах, розрахованих на виконання додатків для машинного навчання та обробки конфіденційної інформації, яким потрібний особливий рівень захисту та підтвердження відсутності збоїв. Як приклад таких додатків наводяться системи, що маніпулюють зображеннями людей і голосовими записами. Використання в KataOS верифікації надійності гарантує, що у разі збою в одній частині системи цей збій не пошириться на решту системи і, зокрема, на ядро та критичні частини.
Архітектура seL4 примітна виносом частин для управління ресурсами ядра в простір користувача та застосування для таких ресурсів тих самих засобів розмежування доступу, як для ресурсів користувача. Мікроядро не надає готових високорівневих абстракцій для керування файлами, процесами, мережевими з'єднаннями тощо, натомість воно надає лише мінімальні механізми для керування доступом до фізичного адресного простору, переривань і ресурсів процесора. Високорівневі абстракції та драйвери для взаємодії з обладнанням реалізуються окремо поверх мікроядра у формі завдань, що виконуються на рівні користувача. Доступ таких завдань до наявних у мікроядра ресурсів організується через визначення правил.
Для додаткового захисту всі компоненти, крім мікроядра, спочатку розвиваються мовою Rust з використанням безпечних прийомів програмування, що мінімізують помилки при роботі з пам'яттю, що призводять до таких проблем як звернення до області пам'яті після її звільнення, розіменування нульових покажчиків та вихід за межі буфера. На Rust зокрема написані завантажувач додатків в оточенні seL4, системні сервіси, фреймворк для розробки додатків, API для доступу до системних викликів, менеджер процесів, механізм динамічного розподілу пам'яті тощо. Для верифікованого складання задіяний інструментарій CAmkES, що розвивається проектом seL4. Компоненти для CAmkES також можуть створюватися мовою Rust.
Безпечна робота з пам'яттю забезпечується в Rust під час компіляції через перевірку посилань, відстеження володіння об'єктами та облік часу життя об'єктів (області видимості), а також оцінку коректності доступу до пам'яті під час виконання коду. Rust також надає засоби захисту від цілих переповнень, вимагає обов'язкової ініціалізації значень змінних перед використанням, застосовує концепцію незмінності (immutable) посилань і змінних за умовчанням, пропонує сильну статичну типізацію для мінімізації логічних помилок.
Джерело: opennet.ru