Операционные системы реального времени

В системе VINO [SS97] также применяется программная локализация неисправностей. В этой системе каждое расширение в ядре имеет свои собственные стек и область памяти. Защиту памяти гарантирует программная локализация неисправностей. Кроме того, VINO использует систему облегченных транзакций для управления выполнением расширений и использованием ресурсов. Наращиваемость в VINO можно осуществить двумя способами:

• приложение может заменить реализацию метода некоторого объекта ядра (ресурса), если это разрешено, – это позволяет изменять стандартное поведение ресурсов,
• приложение может зарегистрировать в ядре обработчик некоего события, такого как подключение в сети к конкретному порту, что позволяет инсталлировать в ядре новые сервисы.

К недостаткам метода программной локализации неисправностей можно отнести то обстоятельство, что каждый раз перед выполнением ненадежной инструкции должны выполняться накладные инструкции.

.4.2.2.1.2 Безопасные языки

Другим распространенным способом сохранения целостности ядра является наложение ограничений на абстракции языка программирования. Наиболее интересным механизмом такого типа является метод проверки типов (type checking), который подразумевает, что безопасные языки являются типизированными и обладают типовой безопасностью.

Безопасные языки, широко используемые в исследовательских проектах, – это Modula-3, Java и ML. Язык ML имеет формальную типовую систему, известную как систему Hindley-Milner, и дает возможность осуществлять статическую проверку типов. Языки Modula-3 и Java обладают меньшим формализмом, поэтому, чтобы гарантировать в них политику безопасности, необходимо выполнять многочисленные проверки типов во время выполнения. Однако ML, как декларативный язык, обеспечивает недостаточную эффективность во время выполнения.

Система SPIN основана на языке Modula-3 [BSP95]. Все взаимодействия между приложением и ядром осуществляются с помощью расширений. Каждое расширение связывается с событием. Расширение должно быть зарегистрировано диспетчером, который инсталлирует расширения и передает события расширениям. С отдельным событием может быть связано несколько расширений. Расширения замещаются или добавляются диспетчером. Modula-3, в основном, используется для гарантирования защиты памяти. Дополнительные ограничения накладываются диспетчером и стандартными расширениями. Динамический компоновщик гарантирует, что расширение видит только санкционированные события.

Очевидным недостатком таких систем является их жесткая привязанность к определенному языку – весь системный код и расширения должны быть написаны на этом языке. Еще один недостаток состоит в том, что политика безопасности фиксирована и определяется выбранным языком. Кроме того, многочисленные проверки во время выполнения сильно понижают производительность системы.

4.2.2.2. Автоматическая верификация

Метод автоматической верификации основан на представлении кода в определенном формате, называемом PCC (Proof-Carrying Code) [Nec97]. PCC-модуль содержит формальное доказательство соответствия кода данной политике безопасности. Истинность доказательства гарантирует безопасность кода, и программный модуль может выполняться без проверок во время выполнения. Политика безопасности ядра описывается с помощью аксиом и правил вывода в доказательствах, а также формулируется в виде предикатов логики первого порядка для каждой инструкции, в которых указывается, при каких обстоятельствах выполнение каждой инструкции будет оставаться безопасным. Приложение использует предикаты политики безопасности для вычисления предиката безопасности. Затем доказывается безопасность этого предиката по правилам логики первого порядка с использованием аксиом и правил вывода политики безопасности. Доказательство присоединяется к расширению. Ядро, в свою очередь, также вычисляет предикат безопасности и проверяет истинность ассоциированного доказательства для этого предиката. Проверка достоверности может быть сделана через простую и эффективную проверку типов (type checking).

Несмотря на привлекательность этого подхода, применимость его пока остается проблемой. Большие трудности возникают при попытках автоматизировать генерацию доказательств и использовать доказательства для языков высокого уровня.

4.3. Автоматическая адаптация

Автоматической адаптацией является адаптация, инициированная самой ОС. Можно рассматривать переносимость, реализуемую через условную компиляцию, как статическую форму автоматической адаптации. Обнаружив, на какой платформе операционная система должна быть скомпонована, система сама способна конфигурироваться, например, с помощью C препроцессора.

Наиболее интересную категорию составляют ОС, которые сами динамически или статически адаптируются к выполняющимся приложениям. С этой целью ОС должна быть способна отслеживать и анализировать приложения и автоматически изменять свое поведение, чтобы поддерживать приложения наилучшим образом. Промышленные ОС обычно поддерживают ограниченную форму динамической автоматической адаптации в специфических и хорошо понятных подсистемах, например, в файловой системе, которая может контролировать поведение пользовательских приложений для оптимизации своей производительности.

Создание автоматической динамически настраиваемой ОС общего назначения можно рассматривать как конечную цель исследований в области настраиваемости ОС. Однако в связи с трудностями, возникающими при компоновке таких систем, пока еще ничего не слышно об автоматических системах в полном смысле этого слова. Пока можно говорить только о нескольких проектах, обсуждаемых далее.

Система Synthetix предназначена для обеспечения специализированных реализаций сервисов операционной системы, генерируемых во время выполнения, на основании частичной оценки [CBK96]. Степень детализации и широта настраиваемости ограничены – проектировщик решает, какой сервис может быть конкретизирован и выбирает параметры конкретизации. Параметры сервиса вводятся с помощью инвариантов, с которыми связаны блоки защиты (guards). После проверки корректности параметров модуль сервиса замещается реализацией с новыми параметрами. Например, системный вызов открытия файла может возвращать конкретизированный код, обеспечивающий чтение файла. Такой код мог бы иметь инварианты, такие как размер блока на диске, последовательный доступ, монопольный доступ и т.п. Когда тот же самый файл позже открывается другим приложением, инвариант монопольного доступа становится некорректным из-за нарушения блока защиты, связанного с системным вызовом открытия файла.

Автоматический подход к настраиваемости исследовался в проекте VINO [SS97], который уже рассматривался выше, однако этот подход в VINO не был реализован. По мнению авторов для осуществления автоматической адаптации поведения системы необходимо получать сведения из следующих трех источников:

• периодическая статистика от каждой подсистемы VINO,
• специализированный компилятор,
• трассы и журналы, которые регистрируют входящие запросы и произведенные результаты.

Вся информация собирается в реальных обстоятельствах, во время выполнения приложения. Затем эта информация анализируется с целью обнаружения чрезвычайных обстоятельств – например, ситуаций, когда потребление ресурсов превышает ожидаемую норму. В таких ситуациях адаптация проводится согласно известным эвристикам. Например, пусть некое приложение интенсивно листает страницы; тогда создаются трассы для запрашиваемых страниц. Результирующие трассы исследуются на предмет совпадения с хорошо известными моделями подкачки страниц. Если такая модель находится, инсталлируется соответствующий алгоритм. Проект VINO интересен тем, что в нем используются эвристики для хорошо известных случаев. В отличие от системы Synthetix, в которой адаптируются только функции и параметры, определенные проектировщиком, VINO поддерживает механизм, с помощью которого система могла бы разрабатывать и тестировать новые алгоритмы для вновь возникающих проблем.  

5. Сводные таблицы характеристик  свойств ОСРВ

Ниже следуют 4 таблицы.

Таблица 1. Характеристики ОСРВ