БЕЗОПАСНОСТЬ И ЗАЩИТА
УДК 681.3.06
КОНФИГУРИРУЕМАЯ СИСТЕМА СТАТИЧЕСКОИ ВЕРИФИКАЦИИ МОДУЛЕЙ ЯДРА ОПЕРАЦИОННЫХ
СИСТЕМ *
© 2015 г. И.С. Захаров, М.У. Мандрыкин, B.C. Мутилин, Е.М. Новиков,
А.К. Петренко, A.B. Хорошилов
Институт системного программирования РАН 109004 Москва, ул. А. Солженицына, 25 E-mail: {ilja.zakharov, mandrykin, mutilin, novikov, petrenko, khoroshilov}@ispras.ru
Поступила в редакцию 12.09.2014
Ядро операционной системы (ОС) представляет собой критичную в отношении надежности и производительности программную систему. Качество ядра современных ОС уже находится на достаточно высоком уровне. Иначе обстоит дело с модулями ядра, например, драйверами устройств, которые по ряду причин имеют существенно более низкий уровень качества. Одними из наиболее критичных и распространенных ошибок в модулях ядра являются нарушения правил корректного использования программного интерфейса ядра ОС. Выявить все такие нарушения в модулях или доказать их корректность потенциально можно с помощью инструментов статической верификации, которым для проведения анализа необходимо предоставить контрактные спецификации, описывающие формальным образом обязательства ядра и модулей по отношению друг к другу. В статье рассматриваются существующие методы и системы статической верификации модулей ядра различных ОС. Предлагается новый метод статической верификации модулей ядра ОС Linux, который позволяет конфигурировать процесс проверки на каждом из его этапов. Показывается, каким образом данный метод может быть адаптирован для проверки компонентов ядра других ОС. Описывается архитектура конфигурируемой системы статической верификации модулей ядра ОС Linux, реализующей предложенный метод, и демонстрируются результаты ее практического применения. В заключении рассматриваются направления дальнейшего развития.
1. ВВЕДЕНИЕ
Надежность и производительность ядра операционной системы (ОС) являются важными характеристиками его качества, поскольку ядро лежит в основе ОС и на результаты его работы во многом полагаются все пользовательские приложения. В ядре большинства современных ОС реализуется только основная функциональность, например, планирование процессорного времени, управление памятью и межпроцессным взаимодействием. Благодаря этому ядро, с одной стороны, является достаточно небольшим по
* Исследование проводилось при финансовой поддержке Мпнобрнаукп РФ (уникальный идентификатор проекта - 11РМЕР160414Х0051).
объему, а с другой стороны, представляет собой программную систему, высокое качество которой формировалось в течение длительного периода времени в разнообразных сценариях использования.
В большинстве ОС набор функций ядра можно расширить путем динамической загрузки модулей. Типичным примером модуля ядра служит драйвер устройства, необходимость в котором может возникнуть при подключении данного устройства. Также в виде модулей часто реализуют файловые системы, сетевые протоколы, аудиокодеки и т.д. Объем исходного кода модулей, поставляемых вместе с ядром ОС, может существенно превышать объем последнего, например, для ядра ОС Linux примерно
в 8 раз. Кроме того, многие разработчики по разным причинам не предоставляют доступ к исходному коду некоторых из своих модулей, а распространяют их в виде бинарного кода, что существенно затрудняет применение некоторых подходов обеспечения качества. Не все модули ядра могут использоваться активно, например, если это драйверы специфичных устройств. Все это приводит к тому, что модули ядра различных ОС имеют существенно меньший уровень качества по сравнению с самим ядром. Это подтверждается исследованиями, которые показали, что в тех модулях, чей исходный код доступен для анализа, содержится примерно в 7 раз больше ошибок, чем в ядре ОС [1-3].
Высокая производительность модулей ядра ОС обеспечивается за счет того, что большинство из них работают в том же адресном пространстве и с тем же уровнем привилегий, что и ядро. Из-за этого ошибки в модулях могут привести к ненадежной работе и снижению производительности ядра, а также и ОС в целом. Анализ изменений в модулях ядра ОС Linux за год разработки показал, что нарушения правил корректного использования программного интерфейса ядра в модулях являются источником около половины ошибок, которые не связаны с нарушениями спецификаций аппаратного обеспечения, сетевых протоколов, аудиокодеков и т.д. [4]. Для других ОС авторам недоступна подобная статистика, но существующие направления исследований также демонстрируют достаточно высокий интерес к ошибкам данного типа [5].
1.1. Подходы, к обнаружению нарушений правил корректного использования программного интерфейса ядра ОС в модулях
Выявлять нарушения правил корректного использования программного интерфейса ядра ОС в модулях можно различными способами. На практике наиболее часто используются экспертиза кода и тестирование. Благодаря использованию данных подходов удается обнаружить и исправить достаточно большое количество ошибок в модулях. Однако они не позволяют выявить все возможные ошибки [6]. Тщательная экспертиза кода требует больших трудозатрат, а
потому она в полной мере проводится только для ядра ОС, но не для такой большой, сложной и динамично развивающейся программной системы, как модули ядра. Тестирование обычно проводится автоматизированным образом, что позволяет сократить трудозатраты по сравнению с экспертизой кода. Однако данный подход требует подготовки тестового окружения, что, например, в случае драйверов устройств бывает достаточно затруднительно. Кроме того, с помощью тестирования можно тщательно проверить только небольшие программные системы.
В последнее время основной тенденцией в проверке программных систем является применение методов и инструментов статического анализа кода, т.е. анализа кода без его реального выполнения (как правило, анализируется исходный код программных систем). На практике преимущественно применяются так называемые легковесные подходы, которые благодаря использованию ряда эвристик позволяют проверять код больших программных систем за время, сравнимое по порядку со временем компиляции. Негативными последствиями использования эвристик является то, что инструменты, которые реализуют данные подходы статического анализа кода, с одной стороны, пропускают ошибки, а с другой стороны, выдают большое количество ложных сообщений об ошибках. Эти инструменты преимущественно применяются для поиска нарушений общих правил безопасного программирования, таких как разыменования нулевых указателей, выход за границу массива и т.д. [7, 8]. Некоторые инструменты были использованы для проверки правил корректного использования программного интерфейса ядра ОС Linux в модулях [9].
Выявить все ошибки искомого вида в программных системах или доказать их корректность потенциально можно с помощью тщательного статического анализа - статической верификации. Современные инструменты статической верификации, которые реализуют, например, метод уточнения абстракции по контрпримерам [10], уже позволяют доказывать выполнимость специфицированных свойств для средних по размеру программных систем за приемлемое время. В частности, с помощью
данных инструментов можно верифицировать отдельные компоненты ядра ОС, такие как модули ядра (для ядра ОС Linux размер большинства модулей составляет несколько тысяч строк кода).
Сами по себе инструменты статической верификации не способны искать нарушения правил корректного использования программного интерфейса ядра ОС в модулях - они позволяют решать задачу достижимости. Как правило, инструменты позволяют определить возможность достижимости некоторого оператора, помеченного заданной меткой, от указанной точки входа. Поэтому необходимо некоторым образом свести задачу обнаружения нарушений проверяемых правил к задачам достижимости. Для этого требуется разработать спецификации пра,вил корректного использования программного интерфейса ядра ОС, которые устанавливают соответствие между нарушениями правил и достижимостью оператора, помеченного заданной меткой. Кроме того, исследования показали, что для того, чтобы получить приемлемые результаты статической верификации модулей ядра (найти ошибки искомого вида при умеренном количестве ложных сообщений об ошибках), инструментам требуется достаточно точная модель окружения, которая должна описывать те же сценарии взаимодействия ядра и модулей, которые возможны при их работе в реальном окружении [11].
Таким образом, инструментам статической верификации для поиска нарушений правил корректного использования программного интерфейса ядра ОС в модулях необходимо предоставить контрактные спецификации, которые формальным образом описывают обязательства ядра и модулей по отношению друг к другу. Со стороны ядра контрактные спецификации должны задавать множество возможных сценариев взаимодействий с модулями корректным и полным образом, а также предоставлять модель программного интерфейса ядра, используемого модулями. Со стороны модулей контрактные спецификации должны задавать, какие обращения модулей к ядру являются корректными, а какие - нет.
В настоящее время инструменты статической верификации активно развиваются в универси-
тетах и научно-исследовательских институтах по всему миру. С каждым годом список инструментов пополняется [12-14]. Инструменты статической верификации реализуют различные подходы, что позволяет применять их для доказательства выполнимости различных специфицированных свойств. Среди этих инструментов нет однозначного лидера, так как они используют разные техники и нацелены на разные классы ошибок. Поэтому в долгосрочной перспективе важно иметь возможность использовать различные инструменты статической верификации.
В данной статье будут рассматриваться только те инструменты статической верификации, которые позволяют проверять программные системы на языке Си, поскольку модули ядра большинства ОС разрабатываются на языке Си.
1.2. Особенности процесса разработки ядра различных ОС
При разработке контрактных спецификаций и проведении статической верификации модулей необходимо учитывать особенности
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.