Компания 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, включително хардуерната част.
Платформата се развива с оглед на използването в специализирани чипове, предназначени за изпълнение на приложения за машинно обучение и обработка на чувствителна информация, за които е необходим специален niveau на защита и потвърждение за отсъствие на сривове. Като примери за подобни приложения се посочват системи, манипулиращи изображения на хора и аудиозаписи. Използването на верификация на надеждността в KataOS гарантира, че в случай на срив в една част на системата, този срив няма да се разпространи в останалата част на системата и, в частност, на ядрото и критичните части.
Архитектура seL4 е забележителна с изнасянето на частите за управление на ресурсите на ядрото в пространството на потребителя и приложението на същите средства за разграничаване на достъпа за тези ресурси, каквито се използват за ресурсите на потребителя. Микроядрото не предоставя готови високостепенни абстракции за управление на файлове, процеси, мрежови връзки и т.н., вместо това предоставя само минимални механизми за управление на достъпа до физическото адресно пространство, прекъсвания и ресурси на процесора. Високостепенните абстракции и драйверите за взаимодействие с хардуера се реализират отделно върху микроядрото под формата на задачи, изпълнявани на потребителско ниво. Достъпът на тези задачи до ресурсите, налични на микроядрото, се организира чрез дефиниране на правила.
За допълнителна защита всички компоненти, освен микроядрото, първоначално се разработват на езика Rust, използвайки безопасни техники на програмиране, минимизиращи грешките при работа с паметта, които водят до проблеми като достъп до памет след нейното освобождаване, разыменоване на нулеви указатели и излизане извън границите на буфера. На Rust са написани и зареждачът на приложения в околната среда seL4, системни услуги, фреймуърк за разработка на приложения, API за достъп до системни повици, мениджър на процеси, механизъм за динамично разпределение на паметта и т.н. За проверена версия се използва инструментарият CAmkES, разработван от проекта seL4. Компонентите за CAmkES също могат да бъдат създавани на езика Rust.
Безопасната работа с паметта се осигурява в Rust по време на компилация чрез проверка на връзките, проследяване на собствеността на обектите и отчитане на времето на живот на обектите (области на видимост), а също и чрез оценка на правилността на достъпа до паметта по време на изпълнението на кода. Rust също предоставя средства за защита от препълване с цели числа, изисква задължителна инициализация на стойностите на променливите преди употреба, прилага концепцията за неизменяемост на връзките и променливите по подразбиране и предлага силна статична типизация за минимизиране на логическите грешки.
Източник: opennet.ru
