Google открыл код защищённой операционной системы KataOS
Автор
Сообщение
news_bot ®
Стаж: 6 лет 11 месяцев
Сообщений: 27286
Компания 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) ссылок и переменных по умолчанию, предлагает сильную статическую типизацию для минимизации логических ошибок.
===========
Источник:
OpenNet.RU
===========
Похожие новости
- Главная ссылка к новости (https://opensource.googleblog....)
- OpenNews: Google представил открытый проект OpenTitan для создания заслуживающих доверия чипов
- OpenNews: Прототип отечественной ОС Phantom на базе Genode будет готов до конца года
- OpenNews: Открыт код сверхнадёжного микроядра seL4
- OpenNews: Проект Neptune OS развивает слой совместимости с Windows на базе микроядра seL4
- OpenNews: Микроядро seL4 математически верифицировано для архитектуры RISC-V
Похожие новости:
- Проект Neptune OS развивает слой совместимости с Windows на базе микроядра seL4
- Микроядро seL4 математически верифицировано для архитектуры RISC-V
- Google представил открытый проект OpenTitan для создания заслуживающих доверия чипов
- [Информационная безопасность] Создание системы формальной верификации с нуля. Часть 1: символьная виртуальная машина на PHP и Python
Теги для поиска: #_kataos, #_opentitan, #_sel4
Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете голосовать в опросах
Вы не можете прикреплять файлы к сообщениям
Вы не можете скачивать файлы
Текущее время: 03-Фев 23:16
Часовой пояс: UTC + 5
| Автор | Сообщение |
|---|---|
|
news_bot ®
Стаж: 6 лет 11 месяцев |
|
|
Компания 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) ссылок и переменных по умолчанию, предлагает сильную статическую типизацию для минимизации логических ошибок. =========== Источник: OpenNet.RU =========== Похожие новости
|
|
Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете голосовать в опросах
Вы не можете прикреплять файлы к сообщениям
Вы не можете скачивать файлы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете голосовать в опросах
Вы не можете прикреплять файлы к сообщениям
Вы не можете скачивать файлы
Текущее время: 03-Фев 23:16
Часовой пояс: UTC + 5