Компания 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) ссылок и переменных по умолчанию, предлагает сильную статическую типизацию для минимизации логических ошибок.