SIP в Singularity – это процессы ОС. Весь код за пределами ядра исполняется в SIP-ах. SIP отличаются от обычных процессов ОС следующим:
• SIP-ы – это закрытые объектные, а не адресные пространства. Два процесса Singularity не могут одновременно получить доступ к объекту.
• SIP-ы – это закрытые пространства кода. Процесс не может динамически загружать или генерировать код.
• SIP-ы не используют для изоляции аппаратное управление памятью. В физическом или виртуальном адресном пространстве может находиться несколько SIP.
• Связь между SIP осуществляется через двунаправленные, строго типизированные высокоуровневые каналы. Канал определяется коммуникационным протоколом и передаваемыми значениями, оба аспекта проверяются.
• SIP-ы недорого создавать, а накладные расходы при коммуникациях между SIP-ами незначительны. Низкая стоимость делает практичным использование SIP-ов на более детальном уровне изоляции и в механизме расширения.
• SIP-ы создаются и уничтожаются операционной системой. Поэтому при их уничтожении ресурсы, занятые SIP-ами гарантированно освобождаются.
• SIP-ы исполняются независимо. Они могут иметь разные раскладки данных, исполняющие системы и сборщики мусора.
SIP-ы не просто используются для инкапсуляции расширений приложений. Вместо обычного применения разных механизмов для процессов и динамической загрузки кода Singularity использует единый механизм для расширяемости и защиты. Как следствие, Singularity нужна только одна модель восстановления после сбоев, один механизм коммуникаций, одна политика безопасности и одна модель программирования вместо слоев или частично избыточных механизмов и политик, применяемых в современных системах. Сутью эксперимента с Singularity является создание целой ОС с использованием SIP и демонстрация того, что результирующая система более надежна, чем традиционные.
Ядро Singularity практически полностью состоит из безопасного (safe) кода, а остальная часть системы, исполняемая в SIP, состоит только из проверяемого безопасного (verifiably safe) кода, включая все драйверы устройств, системные процессы и приложения. В то время, как весь untrusted-код должен быть проверяем и безопасен, части ядра Singularity и исполняющей системы, именуемые доверенной основой (trusted base) не контролируемо безопасны. Безопасность языков защищает эту проверенную основу от непроверенного кода.
Целостность SIP-ов зависит от безопасности языков и от распространяющегося на всю систему инварианта, говорящего, что процесс не может содержать ссылок на объектное пространство другого процесса.
Очевидно, что обеспечение безопасности кода крайне существенно. В настоящее время Singularity полагается на проверку исходного и промежуточного кода компилятором. В будущем типизированный ассемблер (Typed Assembly Language, TAL) позволит Singularity проверять безопасность скомпилированного кода. TAL требует, чтобы исполняемый модуль программы предоставлял доказательства своей типобезопасности (что в случае безопасных языков может делаться компилятором автоматически). Проверка корректности таких доказательств и того, что они применимы для инструкций в исполняемом модуле – прямолинейная задача для простого верификатора из нескольких тысяч строк кода. Такая стратегия сквозной проверки исключает компилятор – большую, сложную программу – из проверенной основы Singularity. Верификатор должен быть тщательно продуман, реализован и проверен, но эти задачи вполне выполнимы благодаря его простоте и размеру.
Инвариант независимости памяти (memory independence invariant), запрещающий использование указателей между объектными пространствами, служит нескольким целям. Во-первых, он улучшает абстракцию данных и изоляцию процесса, скрывая детали реализации и предотвращая появление висячих указателей (dangling pointers) на выгруженные процессы. Во-вторых, он ослабляет ограничения при реализации, позволяя процессам использовать разные исполняющие системы и их сборщики мусора. В-третьих, он делает прозрачными учет и восстановление ресурсов, благодаря однозначно монопольному использованию памяти процессом. Наконец, это упрощает интерфейс ядра, устраняя потребность управлять множеством типов указателей и адресных пространств.
Главное возражение против такой архитектуры – сложность коммуникаций посредством передачи сообщений по сравнению с гибкостью совместного использования данных. В Singularity эта проблема решается использованием эффективной системы сообщений, расширений языков программирования, сжато описывающих коммуникацию через каналы, и средств верификации.
Russia Усть-Илимск
