Google отвори кода за защитената операционна система KataOS

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 също осигурява защита срещу препълване на цели числа, изисква стойностите на променливите да бъдат инициализирани преди употреба, използва концепцията за неизменни препратки и променливи по подразбиране и предлага силно статично въвеждане за минимизиране на логическите грешки.

Източник: opennet.ru