Операционная система 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).
Источник: http://www.opennet.ru/opennews/art.shtml?num=60071