= ВОСЬМАЯ ЕРШОВСКАЯ КОНФЕРЕНЦИЯ ПО ИНФОРМАТИКЕ (ПСИ'11) =
УДК 681.3.06
ИСПОЛЬЗОВАНИЕ ДРАЙВЕРОВ УСТРОЙСТВ ОПЕРАЦИОННОЙ СИСТЕМЫ LINUX ДЛЯ СРАВНЕНИЯ ИНСТРУМЕНТОВ СТАТИЧЕСКОЙ ВЕРИФИКАЦИИ
© 2012 г. М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов, П.Е. Швед
Институт системного программирования РАН
109004 Москва, ул. А.Солженицына, 25 E-mail: mandrykin@ispras.ru, mutilin@ispras.ru, joker@ispras.ru, khoroshilov@ispras.ru, shved@ispras.ru Поступила в редакцию 13.12.2011
Система верификации Linux Driver Verification предназначена для статического анализа исходного кода драйверов устройств операционной системы Linux. В настоящей статье описывается архитектура системы верификации, включая средства интеграции сторонних инструментов статической верификации Си программ. Рассматриваются характеристики исходного кода драйверов Linux, интересные с точки зрения алгоритмов верификации, приводятся примеры проведения сравнительного анализа различных инструментов верификации, а также различных версий и конфигураций одного инструмента.
1. ВВЕДЕНИЕ 1
Статический анализ кода позволяет проверять выполнимость определенных свойств программ на основе некоторого представления их исходного кода без необходимости реального выполнения программ. Основными преимуществами данного подхода являются то, что во-первых, статический анализ не требует подготовки специального тестового окружения и тестовых данных и может осуществляться сразу после написания исходного кода программы; во-вторых, статический анализ позволяет рассмотреть сразу все пути выполнения программы, в том числе, редко встречающиеся и сложно воспроизводимые при динамическом тестировании.
Практическое применение статического анализа кода имеет некоторые ограничения. Наиболее существенным ограничением при
1 Работа частично поддержана ФЦП "Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2013 годы" (контракт № 07.514.11.4104).
использовании статического анализа кода является время проведения анализа. Дело в том, что современные программы являются очень большими и сложными. В свою очередь это приводит к тому, что выполнение полного статического анализа реальных приложений за разумное время практически невозможно, также как и проведение любого вида исчерпывающего тестирования. Поэтому при практическом применении статического анализа используются различные методы упрощения анализируемых моделей программ и эвристики, которые позволяют получить результат за приемлемое время за счет снижения качества анализа. Ключевыми характеристиками качества статического анализа являются число ложных предупреждений и число пропущенных ошибок искомого вида. В зависимости от степени упрощения и целевого времени работы в рамках статического анализа кода можно условно выделить легковесные и тяжеловесные подходы.
Легковесные подходы нацелены на то, чтобы получать результаты быстро, сравнимо по
порядку величины со временем компиляции анализируемого приложения. Для достижения такой высокой скорости данные подходы обычно используют анализ графа потока данных в сопровождении со множеством различных эвристик, что в конечном итоге отрицательно сказывается на качестве анализа, как в плане количества пропущенных ошибок, так и в плане количества ложных предупреждений. Уменьшение числа ложных предупреждений часто имеет больший приоритет, чем обнаружение всех ошибок, так как опыт использования инструментов статического анализа показывает, что при большом проценте ложных предупреждений общая эффективность их применения значительно падает. Несмотря на это, на сегодняшний день легковесные подходы развиты достаточно хорошо. Существует большое количество различных инструментов, которые их реализуют и широко применяются в промышленной разработке программ. К наиболее успешным коммерческим инструментам относятся Coverity [1] и Klocwork Insight [2], академическим - Svace [3, 4, 5], Saturn [6], FindBugs [7], Splint [8] и др.
При использовании тяжеловесных подходов ограничению по времени работы придается существенно меньшее значение, хотя, тем не менее, время проверки должно оставаться в разумных пределах. Это позволяет использовать значительно меньше эвристик при интерпретации исходного кода программ и, соответственно, применять более качественные методы статического анализа кода, что в свою очередь приводит как к уменьшению числа ложных срабатываний, так и к увеличению числа обнаруживаемых ошибок. На сегодняшний день тяжеловесные подходы мало используются при анализе реальных приложений. Существует большое количество академических проектов, которые предлагают различные реализации тяжеловесных подходов, например, инструменты статической верификации BLAST [9, 10], CPAchec-ker [11], CBMC [12], ARMC [13] и др. Но в промышленности тяжеловесные методы нашли свое применение только в проекте Microsoft SDV [14], использующем тяжеловесный инструмент статической верификации
SLAM [15]. Этот проект следует выделить особо, так как он предоставляет полноценный набор инструментов, позволяющих проводить тяжеловесный статический анализ кода драйверов операционной системы (ОС) Microsoft Windows. Предлагаемые инструменты используются в процессе сертификации драйверов и включены в состав Microsoft Windows Driver Developer Kit, начиная с 2006 года. Проект Microsoft SDV наглядно демонстрирует возможность применения тяжеловесного подхода для верификации реальных программ. Однако, Microsoft SDV является, во-первых, узкоспециализированным, так как по сути нацелен на применение только для драйверов ОС Microsoft Windows, а во-вторых, закрытым, что не позволяет ни расширять область его применения, ни использовать для экспериментов в области алгоритмов статического анализа.
Применение других существующих тяжеловесных инструментов статической верификации на практике носит фрагментарный характер. По сути не существует площадки, на которой можно было бы сравнить характеристики различных инструментов анализа на исходном коде программ, активно используемых в промышленности. В проекте Linux Driver Vérification [16, 17, 18, 19, 20] сделана попытка построить такую площадку для инструментов (в первую очередь, тяжеловесных), предназначенных для статического анализа программ на языке Си, на примере драйверов устройств ОС Linux. В настоящей статье исследуются требования и предлагается архитектура такой площадки, кроторая позволит как сравнивать различные инструменты верификации между собой, так и сравнивать различные конфигурации одного инструмента верификации.
Настоящая статья построена следующим образом. В разделе 2 сформулированы требования к открытой системе верификации драйверов устройств ОС Linux. В разделе 3 проведен анализ существующих систем статической верификации драйверов для ОС Linux и Microsoft Windows. Раздел 4 содержит подробное описание предложенной архитектуры предложенной системы верификации Linux Driver Vérification. В разделе 5 обсуждается
использование построенной системы верификации для сравнения инструментов статической верификации.
2. ТРЕБОВАНИЯ К ОТКРЫТОЙ СИСТЕМЕ ВЕРИФИКАЦИИ
Одной из основных целей проекта Linux Driver Verification является построение открытой площадки для экспериментов с различными методами статического анализа кода, в первую очередь, тяжеловесными, при верификации реальных программ. Для достижения этой цели система верификации должна предоставлять удобные средства для интеграции новых инструментов статической верификации и сравнительного анализа их работы с различными настройками. В качестве целевых программ в проекте рассматриваются драйвера ОС Linux, тем не менее, архитектура инструментария должна предусматривать возможность последующего расширения и на другие приложения.
Драверы ОС Linux являются весьма важными целевыми программами для верификации по следующим причинам:
• Драйверов устройств ОС Linux достаточно много и скорость их появления только возрастает с непрерывно растущей популярностью ОС Linux. Драйверы составляют до 70% исходного кода ядра ОС Linux [21, 22].
• Корректность драйверов является важной составляющей безопасности систем, так как драйверы работают с тем же уровнем привилегий, что и остальное ядро. Более 85% различных ошибок, приводящих к некорректной работе всей ОС, зависаниям и падениям находятся именно в драйверах [21, 22, 23].
Обеспечивать надежность драйверов Linux вручную, даже несмотря на большое количество разработчиков (более 1000 человек на сегодняшний день [24]), весьма затруднительно ввиду огромного количества достаточно сложного исходного кода (более 13 млн строк кода [24]), который должен удовлетворять достаточно большому числу разнообразных
правил корректности, начиная от общих правил, которым должны подчиняться все программы на Си, и заканчивая специфичными правилами, которые говорят о том, как драйверы должны использовать интерфейс ядра.
Драйвера ОС Linux имеют ряд преимуществ с точки зрения применения статического анализа:
• Большинство драйверов публикуются вместе с исходным кодом, который является необходимым для большинства инструментов статического анализа.
• Драйверы не используют арифметику с плавающей точкой, редко используют рекурсивные функции.
• Драйверы достаточно небольшие по размеру, а потому можно предположить, что время проверки одного драйвера будет сравнительно невелико.
Для успешного применения системы верификации к драйверам устройств ядра ОС Linux требуется, чтобы система была готова к промышленному применению. Это означает, что должно быть минимизировано участие человека в настройке инструментов и предоставлен максимально удобный интерфейс для использования системы. С точки зрения минимизации участия человека, в первую очередь, необходимо автоматизировать извлечение информации о составе драйвера и настройках его компиляции из уже имеющихся данных, предназначенных для сборки драйвера. При этом важно учитывать, что с одной стороны у драйверов есть много различных зависимостей, а с другой - что для эффективного применения статического анализа количество строк кода до
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.