Google представил проект Open Se Cura для упрощения разработки защищённых систем

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

Кроме Google в разработке инструментария и элементов инфраструктуры приняли участие некоммерческая организация lowRISC, курирующая разработку свободного микропроцессора на базе архитектуры RISC-V, а также компании Antmicro и VeriSilicon. Развиваемый организацией lowRISC процессор был использован в качестве ядра для построения заслуживающих доверия аппаратных компонентов (RoT, Root of Trust). Компания Antmicro предоставила проекту симулятор Renode, позволяющий тестировать CantripOS и микроядро seL4 без реального оборудования. Компания VeriSilicon поделилась своим опытом в области создания чипов и разработки BSP (Board Support Package).

Release. Ссылка here.