Компания Google представи софтуерно-апаратен комплекс Open Se Cura, на който целта е да бъде опростено създаването на защитени чипове, предназначени за задачи, свързани с машинно обучение и изкуствен интелект. Проектът включва операционната система CantripOS и хардуер, основаващ се на платформата OpenTitan и процесорно ядро, базирано на архитектурата RISC-V. По време на разработката Open Se Cura и CantripOS напредваха под имената Sparrow и KataOS, но за да се избегне припокриване с други проекти, финалните продукти бяха преименувани. Разработките на проекта, включително изходните кодове на системните услуги и RTL-схемите (Register Transfer Level), се разпространяват под лицензия Apache 2.0.
Операционната система CantripOS е базирана на микроядрото seL4, върху което работи системно окръжение, написано на Rust. На системи RISC-V за микроядрото seL4 е предоставено математическо доказателство за надеждност, което показва пълно съответствие на кода с определените спецификации на формален език. Архитектурата seL4 е забележителна с извеждането на части за управление на ресурсите на ядрото в потребителското пространство и използването на същите средства за контрол на достъпа, каквито се използват и за потребителските ресурси.
Микроядрото не предлага готови високонадеждни абстракции за управление на файлове, процеси, мрежови връзки и т.н., вместо това предоставя само минимални механизми за управление на достъпа до физическото адресно пространство, прекъсвания и ресурси на процесора. Високонадеждни абстракции и драйвъри за взаимодействие с хардуера са реализирани отделно върху микроядрото под формата на задачи, изпълнявани на потребителско ниво. Достъпът на тези задачи до ресурсите на микроядрото се организира чрез определяне на правила.
Всички компоненти на ОС, освен микроядрото, първоначално са написани на Rust с използване на безопасни техники за програмиране, минимизиращи грешките при работа с паметта. На Rust, наред с другото, са написани зареждачът на приложения в средата на seL4, системните услуги, рамката за разработка на приложения, API за достъп до системните повици, мениджърът на процеси и механизма за динамично разпределение на памет.
За верифицираната сборка е използван инструментариумът CAmkES, разработван от проекта seL4. За разработване на крайни приложения, които могат динамично да се зареждат от системните услуги, се препоръчва да се използва SDK AmbiML, а за изпълнение на модели за машинно обучение - инструментариумът IREE (Intermediate Representation Execution Environment). Компонентите на Rust и системните услуги са разработени с помощта на фреймуърковете Cantrip.
От области на приложение на платформата се споменават специализирани чипове, които изискват особен ниво на защита и потвърждение за отсъствие на грешки. Например, платформата може да се прилага в продукти за машинно обучение, свързани с обработка на конфиденциална информация, като системи за разпознаване на лица и обработка на гласови записи. Комбинацията от логически верифицирано ядро на операционната система с надеждни хардуерни компоненти (RoT, Root of Trust) гарантира, че в случай на грешка в една част на системата, тази грешка няма да се разпространи в останалата част на системата и в частност в ядрото и критичните части.
Освен Google в разработката на инструментариума и елементите на инфраструктурата участваха и неправителствената организация lowRISC, която координира разработката на свободен микропроцесор на базата на архитектурата RISC-V, както и компаниите Antmicro и VeriSilicon. Развиваният от организацията lowRISC процесор е използван като ядро за изграждане на надеждни хардуерни компоненти (RoT, Root of Trust). Компанията Antmicro предостави на проекта симулатор Renode, позволяващ тестване на CantripOS и микроядрото seL4 без реално оборудване. Компанията VeriSilicon сподели своя опит в областта на създаването на чипове и разработката на BSP (Board Support Package).
Източник: opennet.ru
