KataOS, встроенная аппаратная операционная система, ориентированная на безопасность.
Вышла новость, что Google объявила о выпуске исходного кода события, связанные с проектом Ката ОС, целью которого является создание безопасная операционная система для встраиваемого оборудования.
Система обеспечивает поддержку платформ на базе архитектур RISC-V и ARM64. Для имитации работы seL4 и среды KataOS на оборудовании во время разработки используется фреймворк Renode.
В качестве эталонной реализации предлагается программно-аппаратный комплекс Sparrow, объединяющий KataOS с защищенными чипами на базе платформы OpenTitan. Предлагаемое решение чМожно совместить ядро логически проверенная операционная система со встроенными аппаратными компонентами Root of Trust (RoT) с использованием платформы OpenTitan и архитектуры RISC-V.
Помимо кода KataOS, в будущем планируется открыть все остальные компоненты Sparrow, включая аппаратную составляющую.
В качестве основы для этой новой операционной системы мы выбрали seL4 в качестве микроядра, поскольку оно ставит безопасность на первое место; математически доказано, что он безопасен, с гарантированной конфиденциальностью, целостностью и доступностью. С помощью фреймворка seL4 CAmkES мы также можем предоставлять статически определенные и анализируемые системные компоненты. KataOS предоставляет поддающуюся проверке безопасную платформу, которая защищает конфиденциальность пользователей, поскольку приложениям логически невозможно нарушить аппаратную защиту ядра и поддающиеся проверке безопасные системные компоненты.
Платформа разрабатывается с учетом чипов особенно предназначен для запуска приложений конфиденциальности и машинного обучения которые требуют определенного уровня защиты и гарантируют отсутствие сбоев. В качестве примера таких приложений приведены системы, манипулирующие изображениями людей и голосовыми записями. Использование проверки надежности в KataOS гарантирует, что в случае сбоя в одной части системы этот сбой не распространится на остальную часть системы и, в частности, на ядро и критические части.
архитектура seL4 отлично справляется с движущимися частями для управления ресурсами ядра. в пользовательском пространстве и применять те же элементы управления доступом для этих ресурсов, что и для пользовательских ресурсов.
Микроядро не предоставляет абстракции высокого уровня готово для управления файлами, процессами, сетевыми подключениями и т. п., но предоставляет лишь минимальные механизмы для управления доступом к физическому адресному пространству, прерываниям и ресурсам процессора. Абстракции высокого уровня и драйверы для взаимодействия с оборудованием реализуются отдельно поверх микроядра в виде задач пользовательского уровня. Доступ таких задач к ресурсам, доступным микроядру, организуется через определение правил.
Для дополнительной защиты, все компоненты, кроме микроядра, изначально разрабатываются на Rust использование безопасных приемов программирования, сводящих к минимуму ошибки при работе с памятью, приводящие к таким проблемам, как доступ к области памяти после ее освобождения, разыменование нулевых указателей и переполнение буфера.
Загрузчик приложений в среде seL4, системные службы, среда разработки приложений, API для доступа к системным вызовам, диспетчер процессов, механизм динамического выделения памяти и т. д. они написаны на Rust. Для верифицируемой сборки используется инструментарий CAmkES, разработанный проектом seL4. Компоненты для CAmkES также можно создавать на Rust.
Безопасность памяти обеспечена в Rust во время компиляции, проверяя ссылки, отслеживая владение объектом и время жизни объекта (область действия), а также оценивая правильность доступа к памяти во время выполнения кода. Rust также обеспечивает защиту от целочисленного переполнения, требует инициализации переменных перед использованием, применяет концепцию неизменяемых переменных и ссылок по умолчанию и обеспечивает строгую статическую типизацию для минимизации логических ошибок.
Напоследок для интересующихся следует знать, что компоненты системы KataOS написаны на Rust и работают на микроядре seL4, для чего предоставляется математическое доказательство надежности в системах RISC-V, свидетельствующее о том, что код полностью соответствует спецификациям. указывается на формальном языке.
Код проекта открыт под лицензией Apache 2.0, подробнее об этом можно узнать в по следующей ссылке.