автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Верификация драйверов операционной системы Linux при помощи предикатных абстракций

Федеральное государственное бюджетное учреждение науки Институт системного программирования Российской академии наук

УДК 519.685 На правах рукописи

005054413

Мутилин Вадим Сергеевич

Верификация драйверов операционной системы Linux при помощи предикатных абстракций

Специальность 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

4

Москва 2012

- 8 НОЯ 2012

005054413

Работа выполнена в Федеральном государственном бюджетном учреждении науки Институте системного программирования РАН.

Научный руководитель: Официальные оппоненты:

Ведущая организация:

профессор, доктор физико-математических наук

Петренко Александр Константинович профессор, доктор физико-математических наук

Ломазова Ирина Александровна кандидат физико-математических наук

Романенко Сергей Анатольевич Федеральное государственное бюджетное учреждение науки Научно-исследовательский институт системных исследований Российской академии наук (НИИСИ РАН)

Защита диссертации состоится «_15 » ноября 2012 г. в 16 часов на заседании диссертационного совета Д.002.087.01 при Федеральном государственном бюджетном учреждении науки Институте системного программирования Российской академии наук по адресу: 109004, Москва, ул. Александра Солженицына, д.25.

С диссертацией можно ознакомиться в библиотеке Федерального государственного бюджетного учреждения науки Институте системного программирования Российской академии наук.

Автореферат разослан « »_20_г.

Ученый секретарь диссертационного совета канд.физ .-мат.наук

у

/Прохоров С.П./

Актуальность темы

В работе ставится задача верификации драйверов операционной системы (ОС) Linux. Обеспечение надежности и, в частности, информационной безопасности программных и программно-аппаратных систем является одной из главных задач современных информационных технологий. Особый вклад в решение этой задачи вносят работы по верификации системного программного обеспечения, в первую очередь операционных систем. Верификация драйверов ОС Linux является критически важной задачей, так как:

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

• Драйверы ОС Linux, входящие в ядро, это большой, стремительно растущий класс программных систем. На данный момент суммарный объем драйверов составляет более 9 миллионов строк исходного кода. За последний год он увеличился на полмиллиона строк.

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

Для драйверов, которые входят в состав ядра, обеспечение качества проводится силами разработчиков ядра. По данным Linux Foundation, на сегодняшний день в разработке каждой версии ядра, выходящей раз в 2-3 месяца, участвуют более 1000 человек, представляющих более 200 различных организаций. Несмотря на такое большое количество разработчиков, значительное число изменений в уже выпущенных и новых версиях ядра связано с исправлением ошибок в драйверах. Так, например, анализ изменений в драйверах стабильных версий ядра за год разработки с 26.10.10 по 26.10.11

J

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

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

Перспективным направлением является разработка высокоточных инструментов статической верификации при помощи предикатных абстракций. Примерами являются инструменты BLAST, CPAchecker, SLAM. За счет построения предикатных абстракций они позволяют показать не только наличие ошибок, но и их отсутствие для заданного правила.

Ключевым свойством высокоточных инструментов для проверки специфических правил является возможность итеративного уточнения абстракции по методу CEGAR (Counter Example Guided Abstraction-Refinement), что позволяет подстраивать абстракцию как под произвольное правило корректности, так и для конкретного драйвера. Это выгодно отличает такие инструменты от общецелевых, в которых настройка под правило корректности требует реализации соответствующей функциональности в инструменте статического анализа.

Применение инструментов высокоточного статического анализа к

драйверам ОС Linux имеет хорошие предпосылки. Высокоточные методы в

4

настоящее время имеют ограничения по размеру анализируемого кода (до 50100 тыс. строк). В случае драйверов это ограничение приемлемо. Размер драйверов, входящих в состав ядра ОС Linux, не превышает 50 тысяч строк, а в среднем составляет порядка 2-3 тыс. строк кода. Кроме того, важно, что большинство драйверов публикуется вместе с исходным кодом, который является необходимым для большинства инструментов статического анализа.

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

Таким образом, задача верификации драйверов ОС Linux является актуальной, для ее решения требуется разработка нового метода верификации.

Цель и задачи работы

Цель работы - разработка метода верификации драйверов устройств операционных систем для проверки выполнения правил корректного взаимодействия драйверов с ядром операционной системы. Для достижения цели работы были поставлены следующие задачи:

1. Провести анализ существующих методов верификации драйверов;

2. Провести анализ ошибок в драйверах ОС Linux, приводящих к некорректному взаимодействую с ядром ОС;

3. Разработать метод верификации и архитектуру системы верификации драйверов ОС Linux при помощи предикатных абстракций, обеспечивающий:

• верификацию драйверов в условиях непрерывного развития ядра;

• возможности расширения (конфигурируемости) системы верификации драйверов за счет пополнения набора правил корректности и набора инструментов верификации.

4. Разработать систему верификации, реализующую метод;

5. Оценить реализацию метода на практике, дать оценку области применимости метода.

Научная новизна работы

Научной новизной обладают следующие результаты работы:

1. Метод построения моделей окружения драйверов устройств ОС Linux;

2. Метод построения конфигурируемой системы верификации;

3. Математическое доказательство адекватности предложенного метода формализации правил корректности в рамках заданного класса правил работы со структурами обработчиков событий;

4. Методы оптимизации предикатной абстракции в BLAST.

Практическая значимость

На основе разработанного метода была создана система верификации драйверов ОС Linux LDV (Linux Driver Verification). Система LDV позволяет находить нарушения правил корректности взаимодействия с ядром ОС для драйверов, входящих в поставку ядер ОС Linux с версии 2.6.31 по 3.4. По состоянию на 25.09.2012 было найдено более 60 ошибок, которые признаны

разработчиками ядра и уже исправлены или будут исправлены в последующих версиях.

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

Доклады и публикации

По теме диссертации автором опубликовано 14 работ (из них 5 в изданиях из перечня ВАК), список которых приведен в конце автореферата.

Основные положения работы докладывались на следующих конференциях и семинарах:

• Весенний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE: Spring Young Researchers Colloquium on Software Engineering, г. Санкт-Петербург, 2008 г.);

• Общероссийская научно-техническая конференция «Методы и технические средства обеспечения безопасности информации» (г. Санкт-Петербург, 2008 г.);

• Международный семинар «Принципы и технические средства сертификации свободного программного обеспечения» (OpenCert: International Workshop on Foundations and Techniques for Open Source Software Certification, г. Милан, 2008 г.);

• Конференция разработчиков свободных программ на Протве (г. Обнинск, 2009 г.);

• Международная конференция памяти академика А.П. Ершова «Перспективы систем информатики» (PSI: Perspectives of System informatics, г. Новосибирск, 2011 г.);

• Международная конференция по инструментам и алгоритмам создания и анализа систем (TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, г. Таллин, 2012 г.);

• Семинар «День свободного программного и аппаратного обеспечения» (г. Москва, 2012 г.);

• Семинар Института системного программирования РАН (г. Москва, 2012 г.).

Структура и объем диссертации

Работа состоит из введения, семи глав, заключения и списка литературы (55 наименований). Основной текст диссертации (без приложений и списка литературы) занимает 115 страниц.

Краткое содержание диссертации

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

В первой главе приводится анализ работ в области верификации драйверов операционных систем.

Описывается специфика задачи верификации драйверов операционных систем. Драйвер — это программа, которая работает в привилегированном режиме (в ОС Windows, Linux и многих других) и имеет событийный интерфейс, т.е. не только она обращается к функциям-интерфейсам ядра ОС, но и само ядро при наступлении определенных событий обращается к драйверам для выполнения соответствующей обработки. Дисциплина взаимодействия

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

Анализируются техники и инструменты, которые используются для верификации драйверов устройств, и указывается их область применимости. Рассматриваются техники тестирования (динамической верификации), общецелевые техники статического анализа, специализированные системы верификации драйверов.

Инструменты тестирования (динамической верификации). Данные, необходимые для анализа, в этих инструментах собираются во время исполнения кода драйвера, а поэтому инструменты требуют наличия оборудования, для которого предназначен драйвер, или эмуляции этого оборудования. С другой стороны, исходный код анализируемых драйверов обычно не требуется. Это позволяет анализировать драйверы с закрытым исходным кодом. Инструменты динамической верификации обычно дают меньше ложных срабатываний, чем системы статического анализа, однако проверяют только один путь исполнения в данный момент времени. Инструменты статического анализа, напротив, одновременно проверяют многие (или даже все) пути исполнения в коде драйвера, но ложные срабатывания в них более вероятны, чем при использовании динамического анализа.

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

Инструмент Sparse развивается внутри ядра Linux и находит такие

ошибки как, например, использование указателей из неподходящего адресного

9

пространства и другие. В проверках инструмент опирается на аннотации в исходном коде ядра с использстванием расширений GCC. Известно, что с помощью инструмента Sparse было найдено не менее 140 ошибок в ядрах версий 2.6.25, 2.6.29, 2.6.30.

Инструмент Coverity находит такие типы ошибок, как наличие недостижимого кода, разыменование нулевых указателей, использование до сравнения, переполнение буфера, утечки ресурсов, небезопасное использование возвращаемых значений, несовпадение размеров типа и выделяемой памяти, чтение не инициализированных переменных и использование памяти после освобождения. Существуют адаптации данных типов ошибок под различные интерфейсы, например, в ядре Linux в качестве функции выделения ресурсов рассматривается функция выделения памяти под структуру urb подсистемы usb.

Инструмент применялся к ядру ОС Linux в промежутке между 2006 и 2009 годами, в рамках контракта с Департаментом безопасности США. В работах приводятся сведения о том, что из всех предупреждений было отобрано 2,125. Все эти предупреждения были отправлены разработчикам ядра. Однако лишь 61% из них было принято в обработку. Сведения о количестве ложных предупреждений и исправленных ошибках не приводятся.

Описываются также и другие общецелевые инструменты статического анализа, такие как Klocwork Insight, PREfast, Svace.

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

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

10

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

Наиболее развитой системой верификации драйверов операционных систем является система Microsoft SDV, позволяющая проводить статическую верификацию драйверов операционной системы Microsoft Windows. Она используется в процессе сертификации драйверов и включена в состав Microsoft Windows Driver Developer Kit, начиная с 2006 года. Система Microsoft SDV наглядно демонстрирует возможность применения верификации реальных программ.

В системе SDV для создания окружения от пользователя требуется вручную аннотировать исходный код драйверов, указав в нем роли каждой из функций обработчиков. Проверяемые правила корректности формализуются с помощью языка SLIC, в котором связь с исходным кодом драйвера задается с помощью аспектно-ориентированных конструкций, перехватывающих вызовы функций ядра. В настоящее время уже выделен набор из примерно 200 правил, а в исследовательской версии была добавлена возможность добавления новых правил. В систему интегрированы инструменты статической верификации SLAM и Yogi. В виду того, что интерфейс между драйвером и ОС Windows изменяется крайне редко, при разработке архитектуры системы не требовалось учитывать возможность постоянного развития интерфейса между драйверами и ядром ОС.

Существуют также системы верификации драйверов ядра ОС Linux: Avinux, разработка университета города Тюбинген (Германия) и DDVerify, разработка университета Оксфорд (Англия). Разработка систем была нацелена во многом на апробацию новых возможностей инструментов верификации и не учитывала ряд особенностей, необходимых для промышленного использования, в настоящее их разработка не ведется. Например, в системе Avinux требуется ручное задание последовательности вызовов обработчиков драйвера, и не поддерживаются драйверы, состоящие из нескольких файлов. DDVerify требует

II

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

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

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

Делается вывод, что требуется разработка нового метода и архитектуры системы верификации, учитывающих особенности верификации драйверов ОС Linux.

Вторая глава описывает новый метод верификации драйверов.

Рис. 1. Компоненты архитектуры и шаги метода верификации

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

Архитектура схематично изображена на Рис. 1. Компоненты архитектуры изображены в центре. Стрелки указывают порядок, в котором соответствующие компоненты обрабатывают входные данные. Слева изображены входные данные. Справа показан порядок формирования отчета по результатам верификации.

Компонент LDV-Core (шаг 1) осуществляет подготовку ядра ОС Linux

(компонент Kernel Manager), извлечение исходного кода драйверов (Build Cmd Extractor) и генерацию модели окружения драйвера (Driver Environment Generator).

Компонент Domain Specific С Verifier (шаг 2) уже не должен учитывать специфику конструкции драйвера, поданный ему на вход программный код может быть и произвольной программой на языке программирования Си. Данный компонент принимает программу на языке программирования Си и передает ее компоненту Rule Instrumentor, чтобы тот встроил в нее код проверок указанных правил корректности. Затем Domain Specific С Verifier, используя Reachability С Verifier, передает код конкретному инструменту верификации.

Инструмент статической верификации (шаг 3) выносит вердикт. По ходу этого процесса вердикт дополняется отчетами о работе других компонентов, после чего формируется финальный отчет о проверке всего задания, который затем анализируется.

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

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

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

Затем осуществляется генерация окружения драйвера, моделирующего

14

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

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

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

Для построения моделей правил корректности используется подход

аспектно-ориентированного программирования (АОП). Правило формализуется

в аспекте, специальном отдельном модуле. Аспект состоит из набора так

называемых рекомендаг/ий, каждая из которых состоит из множества точек

соединения - точек в программе, к которым осуществляется привязка, и тела

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

для точек соединения. Также в рекомендации указывается, должны ли эти

действия быть выполнены до (англ. before), после (англ. after) или вместо (англ.

around) выполнения точки соединения программы. Тело рекомендации

15

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

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

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

На третьем шаге запускаются инструменты статической верификации Собственно инструменты и анализ результатов верификации описаны в четвертой главе.

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

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

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

Третья глава описывает метод генерации окружения целевого драйвера.

Как уже упоминалось, для работы статических верификаторов драйвер нужно заключить в некоторое "окружение" с тем, чтобы программный код был замкнутым. Такое окружение будем называть "синтезируемым окружением". К синтезируемому окружению предъявляются две группы требований. Первая — связана с тем, что оно должно воспроизводить те же сценарии взаимодействия с драйвером, что и реальное окружение драйвера в операционной системе. Вторая группа требований определяет ограничения на конструкцию (структуру) синтезируемого окружения, обусловленную возможностями современных средств статической верификации.

Предлагаемый метод построения состоит из двух шагов. Сначала

строится логическая модель реального окружения (с учетом специфики каждого

вида драйверов). Эта модель учитывает многопоточность окружения и

асинхронность взаимодействия драйвера с окружением. Для описания модели

используется я-исчисление (The Polyadic л -Calculus: a Tutorial, Robin Milner,

October 1991). Затем строится Си-программа, которая соответствует данной

модели, и при этом является однопоточной и отвечает ограничениям

М

инструментов верификации.

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

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

В диссертации сформулирована и доказана теорема о том, что для каждого драйвера логическая модель окружения эквивалентна синтезированному окружению для того же самого драйвера.

Четвертая глава описывает методы оптимизации анализа при помощи предикатных абстракций.

Описываются предложенные диссертантом методы оптимизации, использованные в инструменте BLAST 2.7, в частности:

• Настройка автоматического управления памятью в языке OCaml позволила уменьшить время, затрачиваемое на операции с памятью, что дало 20% прироста в количестве посещённых точек проверяемой программы на затраченную единицу памяти.

• В синтаксическом анализаторе CIL, используемым инструментом BLAST, были внесены исправления, которые позволили успешно анализировать до 98% драйверов ядра (измерено на версии 2.6.37), и лишь около 2% приводят к ошибкам разбора. До этого BLAST 2.5 не мог разобрать ни одного драйвера в ядре 2.6.31.

• Была улучшена работа с решателями, получающими на вход формулы в формате SMTLIB, за счет снижения накладных расходов при конвертации формул из внутреннего представления.

• Оптимизирован алгоритм фильтрации формулы пути, который

осуществляет удаление частей формулы, не влияющих на

18

получение интерполянта. Время работы алгоритма стало 0(log N), вместо 0(N).

• Был реализован новый алгоритм анализа алиасов, который позволяет анализировать программы, использующие указатели на базовые типы и структуры.

Данные улучшения позволили инструменту BLAST 2.7 занять первое место в категории DeviceDrivers64 и третье в категории DeviceDrivers32 на международных соревнованиях по верификации программ SV-COMP 2012.

Пятая глава описывает систему верификации драйверов ОС Linux (Linux Driver Verification), являющуюся реализацией метода верификации.

Разработанная система верификации обладает следующими важными особенностями:

• Система интегрирована с процессом сборки ядра, поэтому вся необходимая информация о составе и настройках сборки драйверов извлекается автоматически.

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

• Система позволяет добавлять новые правила корректности с помощью аспектно-ориентированного расширения языка программирования Си.

• Система поддерживает встраивание внешних инструментов статической верификации с помощью написания адаптеров.

• Для анализа трасс ошибок и сравнительного анализа результатов система предоставляет специальные компоненты с Веб-интерфейсом.

Шестая глава описывает методику выявления и классификации правил корректности.

В первой части описывается способ выбора источника. Описываются различные источники. Достаточно много информации можно найти в

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

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

В качестве еще одного источника для выявления правил можно рассмотреть список рассылки ядра Linux (от англ. Linux Kernel Mailing List, LKML). В данном списке рассылки обсуждаются различные актуальные вопросы разработки ядра, в том числе вопросы, связанные с исправлением ошибок. На основании этих обсуждений можно выявить множество общих и специфичных правил, но анализ сообщений в LKML достаточно трудоемок, поскольку сообщений много и они содержат большое количество информации, причем не только технической. Кроме того, много ошибок обсуждается в других списках рассылок, на форумах, системах отслеживания ошибок и т.д.

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

Каждое изменение содержит в себе достаточно подробную информацию, включающую сведения об авторе, краткое название изменения, подробное описание (возможно, со ссылками на соответствующие обсуждения), изменение исходного кода драйверов и/или ядра ОС Linux и различную вспомогательную информацию.

В заключение в качестве основного источника для выявления правил

предлагается использовать журнал изменений.

20

Во второй части описываются шаги методики анализа журнала изменений.

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

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

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

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

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

В третьей части описывается разработанная классификация ошибок

21

взаимодействия драйверов с ядром ОС Linux, разработанная в рамках исследований. Были проанализированы изменения в драйверах стабильных версий ядра с 2.6.35 по 3.0 за время с 26.10.10 по 26.10.11. Среди исправлений выявлялись ошибки, для которых можно сформулировать правило корректности взаимодействия драйвера с сердцевиной ядра. Таких ошибок было выделено 176, что составляет 14,9% от общего количества ошибок (1182).

Список классов ошибок представлен в Табл. 2.

Табл. 2. Описание классов ошибок взаимодействия в драйверах ОС Linux

№ Класс Краткое описание класса

1 specific:re source Утечки ресурсов и использование после освобождения

2 specific:check_params Нарушение ограничений на входные параметры

3 specificxontext Вызовы функций в недопустимых контекстах

4 specific:uninit Некорректная инициализация специфичных объектов

5 specific:lock Некорректное использование механизмов синхронизации

6 specificistyle Нарушение стиля оформления драйверов ядра ОС Linux

7 specificrnet Некорректное использование интерфейса сетевой подсистемы

8 specific:usb Некорректное использование интерфейса USB подсистемы

9 specific:check_ret_val Отсутствие проверок возвращаемых значений

10 specific:dma Некорректное использование интерфейса подсистемы прямого доступа к памяти

11 specific:device Некорректное использование интерфейса общей модели драйвера

12 specific:misc Разное

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

Седьмая глава описывает практические результаты.

Система верификации выносит один из трех вердиктов: Safe, Unsafe и Unknown. Вердикт Safe означает отсутствие нарушений проверяемого правила корректности. Вердикт Unsafe говорит об обнаружении нарушения правила и сопровождается трассой ошибки, которая показывает путь выполнения программы, приводящий к ошибочному состоянию. Вердикт Unknown означает, что система по тем или иным причинам (например, нехватка памяти или времени) не смогла найти однозначного ответа на поставленный вопрос.

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

Система верификации предоставляет возможность сохранять результаты анализа вердиктов Unsafe в базе знаний. База знаний позволяет автоматически отображать количество истинных вердиктов Unsafe (True unsafe), ложных вердиктов Unsafe (False unsafe) и непроанализированных или не до конца изученных вердиктов Unsafe (Unknown unsafe).

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

В качестве иллюстрации приводится фрагмент из отчета по результатам верификации драйверов ядра ОС Linux linux-3.4 в мае 2012 года на моделях правил 32_7, 39_7, 43_1а, при ограничении на память 6Gb, ограничении на анализ одного драйвера 15 мин (Рис. 2).

Rule . Total Safe • ipsa -s^m Unsafe Unknown Vf.-[diets

M ': '- True.False ?

32 7 3441 2998 44 399 4 ¿(2 -

39 7 3441 3002 399 11 22 -

43_1а 3441 2965 10 466 2 7 1

Рис. 2. Результаты верификации драйверов ядра ОС Linux версии 3.4.

В данном запуске системы верификации было проверено 3441 модуля драйверов. Количество положительных вердиктов Safe или Unsafe от 86,5% до 88,4% (в среднем 87,5%). В среднем получено от 11,6% до 13,5% вердиктов Unknown (12,5% в среднем). Количество ложных вердиктов Unsafe относительно количества проанализированных драйверов от 0,2% до 1,1%, что составляет (в среднем 0,7%). Для примера, по сравнению с версией 3.2 ядра ОС Linux, в ядре 3.4 для правила 32_7 появилось лишь 3 новых вердикта Unsafe.

Делается вывод, что количество ложных вердиктов Unsafe невелико - при анализе очередных новых версий ядра появляются лишь единицы новых ложных Unsafe вердиктов.

В заключении перечисляются основные результаты работы.

Основные результаты работы

Основные научные и практические результаты, полученные в диссертационной работе и выносимые на защиту, состоят в следующем:

1. Разработан метод верификации драйверов устройств операционных систем для проверки выполнения правил корректного взаимодействия драйверов с ядром операционной системы;

2. Разработан метод построения моделей окружения драйверов устройств ОС Linux;

3. Разработан метод построения конфигурируемой системы верификации,

24

обеспечивающий возможность расширения системы за счет пополнения набора правил корректности и набора инструментов верификации;

4. Разработаны методы оптимизации предикатной абстракции в инструменте BLAST;

5. На основе предложенных методов разработана система верификации драйверов ОС Linux.

Система верификации драйверов ОС Linux разработана в рамках проектов отдела Технологий программирования Института системного программирования РАН при непосредственном участии автора в качестве руководителя и участника разработки основных компонентов системы верификации.

Работы автора по теме диссертации

1. Мутилин B.C., Новиков Е.М., Хорошилов A.B. Анализ типовых ошибок в драйверах операционной системы Linux //Сборник трудов ИСП РАН, том 22, 2012 г.

2. М.У. Мандрыкин, B.C. Мутилин, Е.М. Новиков, A.B. Хорошилов. Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux //Сборник трудов ИСП РАН, том 22, 2012 г.

3. B.C. Мутилин, М.У. Мандрыкин. Интерполяция формул с кванторами в CSIsat на основе инстанцирования //Сборник трудов ИСП РАН, том 22, 2012 г.

4. М.У. Мандрыкин, B.C. Мутилин, Е.М. Новиков, A.B. Хорошилов, П.Е. Швед. Использование драйверов устройств операционной системы Linux для сравнения инструментов статической верификации, Программирование №5, 2012.

5. П.Е. Швед, B.C. Мутилин, М.У. Мандрыкин . Опыт развития инструмента статической верификации BLAST. //ПРОГРАММИРОВАНИЕ, №3, с. 2425

35,2012.

6. V. Mutilin, M. Mandrykin. Instantiation-Based Interpolation for Quantified Formulae in CSIsat. //SYRCOSE 2012

7. P. Shved, M. Mandrykin, V. Mutilin. Predicate Analysis with Blast 2.7. In Flanagan, C., König, В. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 525-527. Springer, Heidelberg, 2012.

8. Shved P., Mutilin V., Mandrykin M. Static verfication "under the hood": Implementation details and improvements of BLAST // Proceedings of SYRCoSE. —Vol. 1, —2011, —Pp. 54-60.

9. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an open framework for С verification tools benchmarking //Proceedings of PSI. — 2011, —Pp. 82-91.

10.A.V.Khoroshilov, V.V.Mutilin, A.K.Petrenko, V.A.Zakharov. Establishing Linux Driver Verification Process PSI 2009 Perspectives of System informatics 2009 LNCS, Vol. 5947 165-176.

11 .В.Мутили», А.Хорошилов. База правил для верификации драйверов Linux // Протва 2009 Тезисы докладов VI Конференции разработчиков свободных программ на Протве, Обнинск, 2009.

12.В.С. Мутилин, A.B. Хорошилов, В.А. Захаров. Верификация безопасности драйверов ОС Linux. Материалы XVII Общероссийской научно-технической конференции «Методы и технические средства обеспечения безопасности информации» 106-112 2008 .

13.А. Khoroshilov, V. Mutilin, V. Shcherbina, О. Strikov, S. Vinogradov, and V. Zakharov. How to Cook an Automated System for Linux Driver Verification. SYRCoSE'2008 2nd Spring Young Researchers' Colloquium on Software Engineering, Volume 2 11-14.

14.A. Khoroshilov, V. Mutilin. Formal Methods for Open Source Components Certification OpenCert 2008 2nd International Workshop on Foundations and Techniques for Open Source Software Certification 52-63 Milan 2008.

Подписано в печать:

28.09.2012

Заказ № 7703 Тираж - 100 экз. Печать трафаретная. Типография «11-й ФОРМАТ» ИНН 7726330900 115230, Москва, Варшавское ш., 36 (499) 788-78-56 www.autoreferat.ru

Введение

Глава 1. Обзор работ в области верификации драйверов операционных систем.

1.1. Ядро ОС Linux.

1.2. Правила

1.3. Инструменты тестирования (динамической верификации)

1.4. Общецелевые инструменты статического анализа

1.5. Системы верификации драйверов операционных систем

1.6. Выводы.

Глава 2. Метод верификации драйверов ОС Linux

2.1. Поток команд

2.2. Шаг 1.

2.3. Шаг 2.

2.4. Шаг 3.

2.5. Построение моделей правил

2.6. Отделение привязки к интерфейсу ядра

Глава 3. Метод генерации окружения целевого драйвера

3.1. Сценарии взаимодействия

3.2. Основные определения

3.3. Формальная модель драйвера и его окружения в 7г-исчислении

3.4. Примеры задания окружения в виде процессов с учетом правил взаимодействия

3.5. Трансляция процессов в Си программу.

Глава 4. Методы оптимизации анализа при помощи предикатных абстракций.

4.1. Общая информация.

4.2. Метод CEGAR.

4.3. Известные ограничения.

4.4. Выводы.

Глава 5. Система верификации драйверов ОС Linux.

5.1. Пользовательский интерфейс системы

5.2. Разработка адаптера инструмента верификации.

Глава 6. Методика выявления и классификации правил корректности

6.1. Выбор источника

6.2. Методика анализа журнала изменений

6.3. Классификация ошибок взаимодействия драйверов с ядром

ОС Linux

6.4. Аналогичные работы

Глава 7. Практические результаты

Актуальность темы

В работе ставится задача верификации драйверов операционной системы (ОС) Linux. Обеспечение надежности и, в частности, информационной безопасности программных и программно-аппаратных систем является одной из главных задач современных информационных технологий. Особый вклад в решение этой задачи вносят работы по верификации системного программного обеспечения, в первую очередь операционных систем. Верификация драйверов ОС Linux является критически важной задачей, так как:

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

• Драйверы ОС Linux, входящие в ядро, это большой, стремительно растущий класс программных систем. На данный момент суммарный объем драйверов составляет более 9 миллионов строк исходного кода. За последний год он увеличился на полмиллиона строк.

Для драйверов, которые входят в состав ядра, обеспечение качества проводится силами разработчиков ядра. По данным Linux Foundation, на сегодняшний день в разработке каждой версии ядра, выходящей раз в 2-3 месяца, участвуют более 1000 человек, представляющих более 200 различных организаций. Несмотря на такое большое количество разработчиков, значительное число изменений в уже выпущенных и новых версиях ядра связано с исправлением ошибок в драйверах. Так, например, анализ изменений в драйверах стабильных версий ядра за год разработки с 26.10.10 по 26.10.11 показал, что порядка 80% изменений являются исправлениями ошибок. Происходит это в силу того, что обеспечивать надежность драйверов ОС Linux затруднительно ввиду огромного количества достаточно сложного исходного кода, который должен удовлетворять большому числу разнообразных правил корректности, начиная от общих правил, которым должны подчиняться все программы на Си, и заканчивая специфичными правилами, которые говорят о том, как драйверы должны использовать интерфейс ядра.

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

Перспективным направлением является разработка высокоточных инструментов статической верификации при помощи предикатных абстракций. Примерами являются инструменты BLAST, CPAchecker, SLAM. За счет построения предикатных абстракций они позволяют показать не только наличие ошибок, но и их отсутствие для заданного правила.

Ключевым свойством высокоточных инструментов для проверки специфических правил является возможность итеративного уточнения абстракции по методу CEGAR (Counter Example Guided Abstraction-Refinement), что позволяет подстраивать абстракцию как под произвольное правило корректности, так и для конкретного драйвера. Это выгодно отличает такие инструменты от общецелевых, в которых настройка под правило корректности требует реализации соответствующей функциональности в инструменте статического анализа.

Применение инструментов высокоточного статического анализа к драйверам ОС Linux имеет хорошие предпосылки. Высокоточные методы в настоящее время имеют ограничения по размеру анализируемого кода (до 50-100 тыс. строк). В случае драйверов это ограничение приемлемо. Размер драйверов, входящих в состав ядра ОС Linux, не превышает 50 тысяч строк, а в среднем составляет порядка 2-3 тыс. строк кода. Кроме того, важно, что большинство драйверов публикуется вместе с исходным кодом, который является необходимым для большинства инструментов статического анализа.

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

Таким образом, задача верификации драйверов ОС Linux является актуальной, для ее решения требуется разработка нового метода верификации.

Цель и задачи работы

Цель работы - разработка метода верификации драйверов устройств операционных систем для проверки выполнения правил корректного взаимодействия драйверов с ядром операционной системы.

Для достижения цели работы были поставлены следующие задачи:

1. Провести анализ существующих методов верификации драйверов;

2. Провести анализ ошибок в драйверах ОС Linux, приводящих к некорректному взаимодействую с ядром ОС;

3. Разработать метод верификации и архитектуру системы верификации драйверов ОС Linux при помощи предикатных абстракций, обеспечивающий:

• верификацию драйверов в условиях непрерывного развития ядра;

• возможности расширения (конфигурируемости) системы верификации драйверов за счет пополнения набора правил корректности и набора инструментов верификации.

4. Разработать систему верификации, реализующую метод;

5. Оценить реализацию метода на практике, дать оценку области применимости метода.

Научная новизна работы

Научной новизной обладают следующие результаты работы:

1. Метод построения моделей окружения драйверов устройств ОС Linux;

2. Метод построения конфигурируемой системы верификации;

3. Математическое доказательство адекватности предложенного метода формализации правил корректности в рамках заданного класса правил работы со структурами обработчиков событий;

4. Методы оптимизации предикатной абстракции в BLAST.

Практическая значимость

На основе разработанного метода была создана система верификации драйверов ОС Linux LDV (Linux Driver Verification). Система LDV позволяет находить нарушения правил корректности взаимодействия с ядром ОС для драйверов, входящих в поставку ядер ОС Linux с версии 2.6.31 по 3.4. По состоянию на 25.09.2012 было найдено более 60 ошибок, которые признаны разработчиками ядра и уже исправлены или будут исправлены в последующих версиях.

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

Доклады и публикации

По теме диссертации автором опубликовано 15 работ [1-15] (из них 5 в изданиях из перечня ВАК [1-5]).

Основные положения работы докладывались на следующих конференциях и семинарах:

• Весенний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE: Spring Young Researchers Colloquium on Software Engineering, г. Санкт-Петербург, 2008 г.);

• Общероссийская научно-техническая конференция "Методы и технические средства обеспечения безопасности информации" (г. Санкт-Петербург, 2008 г.);

• Международный семинар "Принципы и технические средства сертификации свободного программного обеспечения" (OpenCert: International Workshop on Foundations and Techniques for Open Source Software Certification, г. Милан, 2008 г.);

• Конференция разработчиков свободных программ на Протве (г. Обнинск, 2009 г.);

• Международная конференция памяти академика А.П.Ершова "Перспективы систем информатики" (PSI: Perspectives of System informatics, г. Новосибирск, 2011 г.);

• Международная конференция по инструментам и алгоритмам создания и анализа систем (TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, г. Таллин, 2012 г.);

• Семинар "День свободного программного и аппаратного обеспечения" (г. Москва, 2012 г.);

• Семинар Института системного программирования РАН (г. Москва, 2012 г.).

Структура и объем диссертации

Работа состоит из введения, семи глав, заключения и списка литературы (55 наименований). Основной текст диссертации (без приложений и списка литературы) занимает 115 страниц.

4.4. Выводы

В данной главе были рассмотрены следующие методы оптимизации, реализованные в инструменте BLAST 2.7:

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

• В синтаксическом анализаторе CIL, используемым инструментом BLAST, были внесены исправления, которые позволили успешно анализировать до 98% драйверов ядра (измерено на версии 2.6.37), и лишь около 2% приводят к ошибкам разбора. До этого BLAST 2.5 не мог разобрать ни одного драйвера в ядре 2.6.31.

• Была улучшена работа с решателями, получающими на вход формулы в формате SMTLIB, за счет снижения накладных расходов при конвертации формул из внутреннего представления.

• Оптимизирован алгоритм фильтрации формулы пути, который осуществляет удаление частей формулы, не влияющих на получение ин-терполянта. Время работы алгоритма стало 0(log N), вместо O(N).

• Был реализован новый алгоритм анализа алиасов, который позволяет анализировать программы, использующие указатели на базовые типы и структуры.

Данные улучшения позволили инструменту BLAST 2.7 занять первое место в категории DeviceDrivers64 и третье в категории DeviceDrivers32 на международных соревнованиях по верификации программ SV-COMP 2012 [68].

Глава 5

Система верификации драйверов ОС Linux

Система верификации LDV (Linux Driver Verification) является реализацией метода верификации, описанного в главе 2.

Разработанная система верификации обладает следующими важными особенностями:

• Система интегрирована с процессом сборки ядра, поэтому вся необходимая информация о составе и настройках сборки драйверов извлекается автоматически.

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

• Система позволяет добавлять новые правила корректности с помощью аспектно-ориентированного расширения языка программирования Си.

• Система поддерживает встраивание внешних инструментов статической верификации с помощью написания адаптеров.

• Для анализа трасс ошибок и сравнительного анализа результатов система предоставляет специальные компоненты с Веб-интерфейсом.

5.1. Пользовательский интерфейс системы

Пользователь взаимодействует с системой верификации LDV посредством высокоуровневого интерфейса командной строки LDV manager. Данный компонент позволяет проверить некоторый набор драйверов (внутренних или внешних) для некоторого набора ядер по одному или нескольким правилам корректности. В том случае, когда в ходе работы не происходит критическая исключительная ситуация, на выходе LDV manager создает архив, содержащий результаты анализа, информацию о работе компонентов архитектуры LDV, трассы ошибок и необходимые для их визуализации файлы с исходным кодом драйверов и ядра ОС Linux. Далее данный архив может быть загружен в базу данных и использован для анализа, например, с помощью Statistics Server.

Statistics Server - это компонент, который предоставляет веб-интерфейс для статистического анализа и сравнения результатов верификации.

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

Система верификации LD V изначально проектировалась для использования различной целевой аудиторией такой, как разработчики компонентов, разработчики ядра, разработчики инструментов верификации достижимости и т.д. Как правило, запросы к представлению статистики у этих групп отличаются, поэтому Statistics Server предлагает различные заранее подготовленные профили представления данных. Так, например, разработчикам инструментов верификации достижимости помимо статистики по вердиктам предоставляется статистика по времени, затраченном на верификацию; разработчикам компонентов показывается статистика по внутренним проблемам соответствующих компонентов.

Еще одна важная возможность компонента - это возможность сравнения результатов различных заданий верификации. В частности, это оказывается очень полезным и удобным инструментом для сравнения различных инструментов статической верификации, в том числе, различных версий и конфигураций.

Statistics Server интегрирован с Error Trace Visualizer, компонентом, который нацелен на упрощение анализа трасс ошибок, которые выдают инструменты верификации достижимости в случае вынесения вердикта Unsafe. Данный компонент позволяет ускорить анализ трасс ошибок, благодаря чему существенно повышается степень автоматизации процесса верификации в целом. Error Trace Visualizer подробно описан в статье [69].

Как правило, трасса ошибки представляется в текстовом виде, который имеет весьма специфичный, вообще говоря, сильно зависящий от инструмента верификации, формат. Для некоторых инструментов статической верификации существуют инструменты, позволяющие представить трассы ошибок в более наглядном и удобном для анализа формате. Например, трассу ошибки инструмента статической верификации CPAchecker можно преобразовать в HTML, после чего ее можно открывать в любом браузере. Трассы ошибок SATABS визуализируются посредством специального Eclipse плагина. А, например, инструмент статической верификации BLAST до Error Trace Visualizer не имел инструментов, позволяющих упростить анализ трасс ошибок. Подобное многообразие форматов представления трасс ошибок, в конечном итоге, затрудняет их анализ для различных инструментов верификации.

В рамках проекта LDV был разработан общий формат представления трасс ошибок. Разработанный формат является в достаточной степени гибким и расширяемым, что позволяет преобразовывать к нему трассы ошибок различных инструментах верификации без больших трудозатрат. Преобразование исходных трасс ошибок к общему формату реализуется на уровне адаптеров инструментов верификации. Для инструментов BLAST и CPAchecker подобное преобразование было реализовано разработчиками LDV. Error Trace Visualizer визуализирует трассы, представленные в общем формате, единообразным образом и показывает результаты с помощью веб-интерфейса.

Важно отметить, что при визуализации наряду с трассой ошибок Error Trace Visualizer показывает соответствующий ей исходный код программы, причем, между ними устанавливаются определенные взаимосвязи (например, соответствие строк трассы ошибки строкам исходного кода программы). Также компонент выделяет каждый класс элементов трассы ошибки определенным стилем и цветом. Для показываемого исходного кода программы выполняется синтаксическая подсветка. Имеется возможность скрывать и раскрывать как отдельные элементы, так и целые классы элементов трассы ошибки. Все это существенно облегчает анализ трасс ошибок различных инструментов верификации.

5.2. Разработка адаптера инструмента верификации

Для использования инструмента статической верификации необходим адаптер, в котором можно выделить следующие четыре части:

• подготовка входных файлов;

• подготовка обработчика вывода инструмента верификации;

• запуск инструмента;

• обработка результатов.

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

В рамках одной задачи инструменту верификации необходимо проверить достижимость ошибочной метки из некоторой точки входа, причем анализируемая программа может быть расположена в одном или нескольких файлах. Инструменты верификации могут накладывать ограничения на то, в каком виде должны быть представлены эти файлы. Разработчику адаптера предоставляется возможность применить к каждому из входных файлов стандартный препроцессор языка Си, обработать файлы с помощью инструмента трансформации кода CIL, или соединить все файлы в один с помощью того же CIL [70]. В результате возвращается список файлов, в которых содержится весь необходимый для проверки исходный код.

Обработчику вывода инструмента верификации на вход подаются строчки, выдаваемые инструментом верификации на стандартный вывод и/или на стандартный поток ошибок. Обработчик опционально возвращает набор значений с некоторой информацией, которую он извлек из трассы (например, последние 20 строк или вердикт о наличии/отсутствии в программе ошибок). Каждая функция-обработчик хранит свое внутреннее состояние. Непосредственно перед запуском инструмента верификации адаптер регистрирует такие функции, a Reachibihty С Verifier применяет их, когда инструмент верификации будет запущен, параллельно с его работой.

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

• автоматически применяет функции обработчики вывода, зарегистрированные адаптером ранее;

• вывод инструмента, который может быть большим по объему, архивируется и сохраняется на диск;

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

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

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

Адаптер также может передать произвольную текстовую строку (например, содержащую исключение и трассу стека, выброшенные инструментом при неудачном завершении) и один или несколько файлов для сохранения их в финальном отчете с результатами верификации. Затем эта информация может быть использована для последующей обработки и построения статистики с помощью компонента LDV Statistics Server.

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

Глава 6

Методика выявления и классификации правил корректности

6.1. Выбор источника

Для выявления правил корректности достаточно много информации можно найти в документации, в том числе, входящей в состав ядра и в исходный код ядра и драйверов, а также в литературе по разработке драйверов и ядра ОС Linux.

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

В качестве еще одного источника для выявления правил можно рассмотреть список рассылки ядра Linux (от англ. Linux Kernel Mailing List, LKML). В данном списке рассылки обсуждаются различные актуальные вопросы разработки ядра, в том числе вопросы, связанные с исправлением ошибок. На основании этих обсуждений можно выявить множество общих и специфичных правил, но анализ сообщений в LKML достаточно трудоемок, поскольку сообщений много и они содержат большое количество информации, причем не только технической. Кроме того, много ошибок обсуждается в других списках рассылок, на форумах, системах отслеживания ошибок и т.д.

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

Каждое изменение содержит в себе достаточно подробную информацию, включающую сведения об авторе, краткое название изменения, подробное описание (возможно, со ссылками на соответствующие обсуждения), изменение исходного кода драйверов и/или ядра ОС Linux и различную вспомогательную информацию.

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

6.2. Методика анализа журнала изменений

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

Далее из рассмотрения исключаются ошибки, исправления которых связано с требованиями к функциональности конкретного драйвера или ошибки взаимодействия драйвера с конкретным оборудованием. Это так называемые "нетиповые" ошибки. В том случае, если ошибка связана с неправильным использованием специализированных для конкретного драйвера или группы драйверов констант, условий и вычислений, ее следует исключить из дальнейшего рассмотрения, так как для нее нельзя сформулировать правило корректности.

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

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

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

Важно отметить, что список классов неизвестен заранее и может быть определен только непосредственно по ходу самого анализа. Предполагается, что, в первую очередь, классы позволят различить общие и специфичные ошибки в драйверах. commit 5fc8fe8e2ea30805bee5al3420817d6ad34ea9ce Author Anders Larsen <al@alarsen net> Date Wed Oct 6 23 46 25 2010 +0200

USB cp210x Add WAGO 750-923 Service Cable device ID commit 93ad03d60b5bl8897030038234aa2ebae8234748 upstream

The WAGO 750-923 USB Service Cable is used for configuration and firmware updates of several industrial automation products from WAGO Kontakttechnik GmbH skipped)

Signed-off-by Anders Larsen <al@alarsen net> Signed-off-by Greg Kroah-Hartman <gregkh@suse de> diff -git a/drivers/usb/serial/cp210x с b/drivers/usb/serial/cp210x с index 3ad53bd 9927bca 100644 a/drivers/usb/serial/cp210x с + + + b/drivers/usb/serial/cp210x с -132 6 +132 7 @@ static const struct usbdeviceid idtable[] = { USBDEVICE(0xl7F4, OxAAAA) >, /* WavesenseJazz blood glucose meter*/ { USBDEVICE(0x1843, 0x0200) > /* Vaisala USB Instrument Cable */ { USBDEVICE(0xl8EF, OxEOOF) >, /* ELV USB-l2C-lnterface */ + { USBDEVICE(0xlBE3, 0x07A6) }, /* WAGO 750 923 USB Service Cable */ { USBDEVICE(0x413C, 0x9500) }, /* DW700 GPS USB interface */ { } I* Terminating Entry */

Рис 6 1 Описание изменения 5fc8fe8, добавляющего поддержку нового устройства

6.2.1. Примеры применения предложенной методики

Рассмотрим применение предложенной методики на примерах На основании описания и изменения в исходном коде для изменения в драйвере, представленного на Рис 6.1 можно сделать вывод, что данное изменение в драйвере не является исправлением ошибки, а добавляет поддержку нового USB устройства

Изменение в драйвере на Рис 6.2 демонстрирует исправление нетиповой ошибки, вызванной нарушением контракта драйвера трекпада Изменение исходного кода задействует специфичные для данного драйвера константы и ограничения

На Рис 6 3 представлено изменение в драйвере, которое является исправлением типовой специфичной ошибки. Данная ошибка вызвана неправильным использованием интерфейса сердцевины ядра, а именно, в контексте блокировки вызывается функция выделения памяти, которая может перевеcommit 8e6b41c76c5b8a27b2abd7b9f6ed0877987fdllb Author Chase Douglas <chase douglas@canonical com> Date Tuejan 11 19 37 50 2011 +0100

HID magicmouse Don't report REL{X, Y} for Magic Trackpad Linus' tree commit 6a66bbd693cl2f71697c61207aal8bc5al2da0ab ]

With the recent switch to having the hid layer handle standard axis initialization, the Magic Trackpad now reports relative axes This would be fine in the normal mode, but the driver puts the device in multitouch mode where no relative events are generated Also, userspace software depends on accurate axis information for device type detection Thus, ignoring the relative axes from the Magic Trackpad is best

Signed-off-by Chase Douglas cchase douglas@canonical com> Signed-off-by Jiri Kosina <jkosina@suse cz> Signed-off-by Greg Kroah-Hartman <gregkh@suse de> diff --git a/drivers/hid/hid-magicmouse с b/drivers/hid/hid-magicmouse с index e6dcl51 ed732b7 100644 — a/drivers/hid/hid-magicmouse с + + + b/drivers/hid/hid-magicmouse с -433,6 +433,11 @@ static int magicmouseinputmapping(struct hiddevice *hdev, if ('msc->input) msc->input = hi->input, Л Magic Trackpad does not give relative data after switching to MT */ + if (hi->input >id product == USBDEVICEIDAPPLEMAGICTRACKPAD && + field->flags & HIDMAINITEMRELATIVE) return -1 return 0,

Рис 6 2 Описание изменения 8е6Ь41с, исправляющего петиповую ошибку commit 83a9a8034ee98ac21804c376ec90af8e4997790e Author John Johansen <john.johansen@canomcal com> Date Wed Jun 8 15 07 47 2011 -0700

AppArmor Fix sleep in invalid context from tasksetrlimit commit 1780f2d3839a0d3eb85ee014a708f9e2c8f8ba0e upstream Affected kernels 2 б 36 - 3 0

AppArmor may do a GFPKERNEL memory allocation with tasklock(tsk->groupleader), held when called from securitytasksetrlimit This will only occur when the task's current policy has been replaced, and the task's creds have not been updated before entering the LSM securitytasksetrlimit() hook

BUG sleeping function called from invalid context at mm/slub с 847 inatomic() 1, irqsdisabled() 0, pid 1583, name cupsd skipped)

Signed-off-by John Johansen <john johansen@canonical com> Reported-by Miles Lane <miles lane@gmail com> Signed-off-by James Morris <jmorris@namei org> Signed-off-by Greg Kroah-Hartman <gregkh@suse de> diff --git a/security/apparmor/lsm с b/security/apparmor/lsm с index eclbcec 3d2fdl4 100644 - a/security/apparmor/lsm с + + + b/secunty/apparmor/lsm с -612,7 +612,7 @@ static int apparmorsetprocattr(struct taskstruct *task char 'name static int apparmortasksetrlimit(struct taskstruct *task, unsigned int resource, struct rlimit *newrlim) struct aaprofile +profile = aacurrentprofile() struct aaprofile ^profile =aacurrentprofile() int error = 0, if ('unconfined(profile))

Рис 6 3 Оппсаиие изменения 83a9a80, исправляющего типовую специфичную ошибку (вызов функции, которая может заснуть, в контексте блокировки) сти процесс в режим ожидания.

6.3. Классификация ошибок взаимодействия драйверов с ядром ОС Linux

Подробное описание анализа можно найти в статье [1].

В рамках основного анализа рассматривались изменения, которые были сделаны в стабильных ядрах с 2.6.35 по 3.0 в репозитории [71] за время, начиная с 26 октября 2010 года по 26 октября 2011 года. Всего таких изменений насчитывается 3101. Среди данных изменений некоторые являются дубликатами, поскольку одни и те же изменения попадают в различные стабильные ветки. Уникальных изменений за указанный период времени насчитывается 2623 (около 84.6% от общего числа изменений). Для того чтобы отделить изменения в драйверах от остальных изменений в ядре, рассматривались только такие изменения, которые затрагивали файлы из папок: crypto, drivers, sound, security, include/acpi, include/crypto, include/drm, include/media, include/mtd, include/pcmcia, include/rdma, include/rxrpc, include/scsi, include/sound и include/video. Из всех уникальных изменений, сделанных в стабильных ядрах с 26.10.10 по 26.10.11, в драйверах оказалось 1503, т.е. около 57.3% от общего числа уникальных изменений. Сводные результаты основного анализа изменений в драйверах представлены в Табл. 6.1. Подробное описание анализа можно найти в статье [1].

В соответствии с методикой, предложенной в данной работе, была произведена классификация выявленных типовых ошибок. При классификации не рассматривались изменения, которые являются исправлением типовых специфичных ошибок, связанных с некорректным использованием интерфейса группы драйверов (47 изменений). Изменениям, которые включали исправления сразу нескольких ошибок, приписывалось соответствующее количество

Изменения в драйверах (1503)

Расширение функциональности (321 - 21%) Исправление ошибок (1182 - 79%)

Нетиповые ошибки (786 - 67%) Типовые ошибки (396 - 33%)

Заключение

Основные научные и практические результаты, полученные в диссертационной работе и выносимые на защиту, состоят в следующем:

1. Разработан метод верификации драйверов устройств операционных систем для проверки выполнения правил корректного взаимодействия драйверов с ядром операционной системы;

2. Разработан метод построения моделей окружения драйверов устройств ОС Linux;

3. Разработан метод построения конфигурируемой системы верификации, обеспечивающий возможность расширения системы за счет пополнения набора правил корректности и набора инструментов верификации;

4. Разработаны методы оптимизации предикатной абстракции в инструменте BLAST;

5. На основе предложенных методов разработана система верификации драйверов ОС Linux.

Система верификации драйверов ОС Linux разработана в рамках проектов отдела Технологий программирования Института системного программирования РАН при непосредственном участии автора в качестве руководителя и участника разработки основных компонентов системы верификации. Автор выражает свою признательность всем участникам данных проектов. Особый вклад в работу внесли А.В.Хорошилов, Е.М.Новиков, П.Е.Швед.

1. Мутилин В. С., Новиков Е. М., Хорошилов А. В. Анализ типовых ошибок в драйверах операционной системы Linux // Труды Института системного программирования РАН. 2012. Т. 22. С. 349-374.

2. Мутилин В. С., Мандрыкин М. У. Интерполяция формул с кванторами в CSIsat на основе инстанцирования // Труды Института системного программирования РАН. 2012. Т. 22. С. 327-348.

3. Мандрыкин М. У., Мутилин В. С., Новиков Е. М. и др. Использование драйверов устройств операционной системы Linux для сравнения инструментов статической верификации // Программирование. 2012. Т. 5. С. 54-71.

4. Швед П. Е., Мутилин В. С., Мандрыкин М. У. Опыт развития инструмента статической верификации BLAST // Программирование. 2012. Т. 3. С. 24-35.

5. Mutilin V., Mandrykin М. Instantiation-Based Interpolation for Quantified Formulae in CSIsat // Proceedings of SYRCoSE. 2012. Vol. 1. P. 85-93.

6. Shved P., Mandrykin M., Mutilin V. Predicate Analysis with Blast 2.7 // Proceedings of TACAS. 2012. Vol. 7214. P. 525-527.

7. Мутилин В. С., Новиков Е. М., Страх А. В. и др. Архитектура Linux

8. Driver Verification // Труды Института системного программирования РАН. 2011. Т. 20. С. 163-187.

9. Shved P., Mutilin V., Mandrykin М. Static Verfication "Under The Hood": Implementation Details and Improvements of BLAST // Proceedings of SYR-CoSE. Vol. 1. 2011. P. 54-60.

10. Khoroshilov A., Mutilin V., Novikov E. et al. Towards An Open Framework for С Verification Tools Benchmarking // Proceedings of PSI. 2011. P. 82-91.

11. Мутилин В., Хорошилов А. База правил для верификации драйверов Linux // Тезисы докладов VI Конференции разработчиков свободных программ на Протве. 2009.

12. Мутилин В. С., Хорошилов А. В., Захаров В. А. Верификация безопасности драйверов ОС Linux // Материалы XVII Общероссийской научно-технической конференции "Методы и технические средства обеспечения безопасности информации". 2008. С. 106-112.

13. Khoroshilov A., Mutilin V., Shcherbina V. et al. How to Cook an Automated System for Linux Driver Verification // 2nd Spring Young Researchers' Colloquium on Software Engineering. Vol. 2 of SYRCoSE 2008. 2008. P. 11-14.

14. Khoroshilov A., Mutilin V. Formal Methods for Open Source Components Certification // 2nd International Workshop on Foundations and Techniques for Open Source Software Certification. OpenCert 2008. 2008. P. 52-63.

15. Ядро дистрибутива Debian Электронный ресурс] // Режим доступа: http: //wiki . debian. org/DebianKernel, свободный.

16. ОС Linux реального времени Электронный ресурс] // Режим доступа: https://www.osadl.org/Realtime-Linux.projects-realtime-linux. O.html, свободный.

17. Corbet J. How to Participate in the Linux Community. A Guide To The Kernel Development Process Электронный ресурс] // Режим доступа: http://www.linuxfoundation.org/sites/main/files/ How-Participate-Linux-Community0.pdf, свободный. 2008.

18. Leemhuis T. What's new in Linux 3.3 Электронный ресурс] // Режим доступа: http://www.h-online.com/open/features/ What-s-new-in-Linux-3-3-1466872.html, свободный. 2012.

19. Chou A., Yang J., Chelf В. et al. An empirical study of operating systems errors // SOSP '01: Proceedings of the eighteenth ACM symposium on Operating systems principles. New York, NY, USA: ACM, 2001. P. 73-88.

20. Swift M. M., Bershad B. N., Levy H. M. Improving the reliability of commodity operating systems // SOSP '03: Proceedings of the nineteenth ACM symposium on Operating systems principles. New York, NY, USA: ACM, 2003. P. 207-222.

21. Ganapathi A., Ganapathi V., Patterson D. Windows XP kernel crash analysis // Proceedings of the 20th conference on Large Installation System Administration. LISA '06. Berkeley, CA, USA: USENIX Association, 2006. P. 12-12.

22. Palix N., Thomas G., Saha S. et al. Faults in linux: ten years later // SIG-PLAN Not. 2011. Vol. 47, no. 4. P. 305-318.

23. ISO/IEC TR 24772 // Information Technology Programming Languages - Guidance to Avoiding Vulnerabilities in Programming Languages through Language Selection and Use. 2010.

24. Kroah-Hartman G. The Linux Kernel Driver Interface Электронный ресурс] // Режим доступа: http://www.kernel.org/doc/ Documentâtion/stableapinonsense.txt, свободный.

25. Ахо А. В., Лам M. С., Сети Р., Ульман Д. Д. Компиляторы: принципы, технологии и инструментарий. 2-е изд. Москва: Вильяме, 2008.

26. Johnson S. С. Lint, а С program verifier // Bell Laboratories. Murray Hill, New Jersey, 1987.

27. Страница инструмента Sparse A Semantic Parser for С Электронный ресурс] // Режим доступа: http://www.kernel.org/pub/software/ devel/sparse/, свободный.

28. Engler D., Chelf В., Chou A. Checking system rules using system-specific, programmer-written compiler extensions // Proceedings of the 4th conferenceon Symposium on Operating System Design & Implementation Volume 4. 2000. P. 1-16.

29. Guo P. J., Engler D. Linux kernel developer responses to static analysis bug reports // Proceedings of the 2009 conference on USENIX Annual technical conference. USENIX'09. Berkeley, CA, USA: USENIX Association, 2009. P. 22-22.

30. Stuart H. Hunting bugs with Coccinelle: Ph. D. thesis / University of Copenhagen. 2008.

31. Lawall J. L., Brunei J., Palix N. et al. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code // DSN'09 The 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks. 2009. P. 43-52.

32. Xie Y., Aiken A. Saturn: a SAT-based tool for bug detection // Proceedings of the 17th international conference on Computer Aided Verification. CAV'05. Berlin, Heidelberg: Springer-Verlag, 2005. P. 139-143.

33. Xie Y., Aiken A. Saturn: A scalable framework for error detection using Boolean satisfiability // ACM Trans. Program. Lang. Syst. 2007. Vol. 29, no. 3.

34. Dillig I., Dillig T., Aiken A. Sound, complete and scalable path-sensitive analysis // SIGPLAN Not. 2008.-June. Vol. 43. P. 270-280.

35. Pratikakis P., Foster J. S., Hicks M. LOCKSMITH: Practical static race detection for С // ACM Trans. Program. Lang. Syst. 2011. Vol. 33, no. 1. P. 3:1-3:55.

36. Сыромятников С. Декларативный интерфейс поиска дефектов по синтаксическим деревьям: язык К AST / / Труды Института системного программирования РАН. 2011. Т. 20. С. 51-68.

37. Ayewah N., Iiovemeyer D., Morgenthaler J. D. et al. Using Static Analysis to Find Bugs // IEEE Softw. 2008. Vol. 25, no. 5. P. 22-29.

38. Evans D., Larochelle D. Improving Security Using Extensible Lightweight Static Analysis // IEEE Softw. 2002. January. Vol. 19. P. 42-51.

39. Аветисян А., Белеванцев А., Бородин А., Несов В. Использование статического анализа для поиска уязвимостей и критических ошибок в исходном коде программ // Труды Института системного программирования РАН. 2011. Т. 21. С. 23-38.

40. Ball Т., Bounimova Е., Levin V. et al. The Static Driver Verifier Research Platform // Computer Aided Verification. CAV'10. 2010. P. 119-122.

41. Ball Т., Rajamani S. K. SLIC: A specification language for interface checking Электронный ресурс] // Режим доступа: http://research.microsoft, com/apps/pubs/default.aspx?id=69906, свободный. 2001.

42. Ball Т., Bounimova E., Kumar R., Levin V. SLAM2: Static driver verification with under 4% false alarms // Formal Methods in Computer-Aided Design (FMCAD), 2010. 2010.-oct. P. 35 -42.

43. Ball Т., Levin V., Rajamani S. K. A decade of software model checking with SLAM // Commun. ACM. 2011. Vol. 54, no. 7. P. 68-76.

44. Post H., Kiichlin W. Integrated static analysis for Linux device driver verification // Proceedings of the 6th international conference on Integrated formal methods. IFM'07. Berlin, Heidelberg: Springer-Verlag, 2007. P. 518-537.

45. Post H., Kiichlin W. Automatic data environment construction for static device drivers analysis // Proceedings of the 2006 conference on Specification and verification of component-based systems. SAVCBS '06. New York, NY, USA: ACM, 2006. P. 89-92.

46. Beyer D., Henzinger T. A., Jhala R., Majumdar R. The software model checker Blast: Applications to software engineering // Int. J. Softw. Tools Technol. Transf. 2007. Vol. 9, no. 5. P. 505-525.

47. Novikov E. One Approach to Aspect-Oriented Programming Implementation for the C programming language // Proceedings of SYRCoSE. 2011. Vol. 1. P. 74-81.

48. Milner R. The Polyadic 7r-Calculus: a Tutorial. LFCS, Department of Computer Science, University of Edinburgh, 1991. P. 49.

49. Henzinger T. A., Jhala R., Majumdar R. Lazy abstraction // Symposium on Principles of Programming Languages. ACM Press, 2002. P. 58-70.

50. Clarke E., Grumberg O., Jha S. et al. Counterexample-Guided Abstraction Refinement // Computer Aided Verification / Ed. by E. Emerson, A. Sistla. Springer Berlin / Heidelberg, 2000. Vol. 1855 of Lecture Notes in Computer Science. P. 154-169.

51. Detlefs D., Nelson G., Saxe J. B. Simplify: a theorem prover for program checking // J. ACM. 2005. Vol. 52, no. 3. P. 365-473.

52. Barrett C., Tinelli C. CVC3 // Proceedings of the 19£/l International Conference on Computer Aided Verification (CAV '07) / Ed. by W. Damm, H. Hermanns. Vol. 4590 of Lecture Notes in Computer Science. Springer-Verlag, 2007. P. 298-302. Berlin, Germany.

53. Craig W. Linear reasoning // J. Symbolic Logic. 1957. Vol. 22. P. 250-268.

54. Henzinger T. A., Jhala R., Majumdar R., McMillan K. L. Abstractions from proofs // SIGPLAN Not. 2004. Vol. 39, no. 1. P. 232-244.

55. Jhala R., Majumdar R. Path slicing // SIGPLAN Not. 2005. Vol. 40, no. 6. P. 38-47.

56. Beyer D., Zufferey D., Majumdar R. CSIsat: Interpolation for LA+EUF // CAV. 2008. P. 304-308.

57. McMillan K. L. An interpolating theorem prover // Theor. Comput. Sci. 2005. Vol. 345, no. 1. P. 101-121.

58. Andersen L. O. Program Analysis and Specialization for the С Programming Language. K0benhavns Universitet. Datalogisk Institut. DIKU, 1994.

59. Новиков Е. Упрощение анализа трасс ошибок инструментов статического анализа кода // Труды второй научно-практической конференции «Актуальные проблемы системной и программной инженерии» (АПСПИ-2011). 2011.-25 Мая. С. 215-221.

60. Репозиторий стабильных версий ядра ОС Linux Электронный ресурс] // Режим доступа: http://git.kernel.org/?p=linux/kernel/ git/stable/linux-stable.git;a=summary, свободный.

61. Engler D., Chen D. Y., Hallem S. et al. Bugs as deviant behavior: a general approach to inferring errors in systems code // SIGOPS Oper. Syst. Rev. 2001. Vol. 35, no. 5. P. 57-72.

62. Li Z., Zhou Y. PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code // SIGSOFT Softw. Eng. Notes. 2005. Vol. 30, no. 5. P. 306-315.