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

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