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

• Автор: Мутилин, Вадим Сергеевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2012
• Место защиты: Москва
• Количество страниц: 141 с. : ил.

Содержание
Введение .

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

1.1. Ядро ОС Ьпих

1.2. Правила .

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

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

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

1.6. Выводы.

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

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. Метод СЕСАЛ
4.3. Известные ограничения
4.4. Выводы.
Глава 5. Система верификации драйверов ОС Ыпих.
5.1. Пользовательский интерфейс системы
5.2. Разработка адаптера инструмен та верификации.
Глава 6. Методика выявления и классификации правил корректности .
6.1. Выбор источника .
6.2. Методика анализа журнала изменений
6.3. Классификация ошибок взаимодействия драйверов с ядром
ОС Ьших.
6.4. Аналогичные работы .
Глава 7. Практические результаты .
Заключение .
Литература


На основе разработанного метода была создана система верификации драйверов ОС Linux LDV (Linux Driver Verification). Система LDV позволяет находить нарушения правил корректности взаимодействия с ядром ОС для драйверов, входящих в поставку ядер ОС Linux с версии 2. По состоянию на было найдено более ошибок, которые признаны разработчиками ядра и уже исправлены или будут исправлены в последующих версиях. Результаты работы будут полезны для автоматизации сертификационных процессов для компьютерного обеспечения, которые существуют у многих поставщиков дистрибутивов ОС Linux и ОС, построенных на основе ядра Linux. Также результаты могут быть использованы для проверки качества драйверов ОС Linux, для создания инструментов верификации других видов программного обеспечения, критичного по безопасности. Результаты работы могут быть использованы для сравнения характеристик различных инструментов статического анализа кода. По теме диссертации автором опубликовано работ [1-] (из них 5 в изданиях из перечня ВАК [1-5]). Весенний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE: Spring Young Researchers Colloquium on Software Engineering, г. Санкт-Петербург, г. Общероссийская научно-техническая конференция “Методы и технические средства обеспечения безопасности информации1’ (г. Санкт-Петербург. OpenCert: International Workshop on Foundations and Techniques for Open Source Software Certification, г. Милан, 0S г. Конференция разработчиков свободных программ на Протве (г. Обнинск, г. Международная конференция памяти академика А. П. Ершова “Перспективы систем информатики” (PSI: Perspectives of System informatics, г. Новосибирск, г. Международная конференция по инструментам и алгоритмам создания и анализа систем (TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, г. Таллин, г. Семинар “День свободного программного и аппаратного обеспечения” (г. Москва, г. Семинар Института системного программирования РАН (г. Москва, г. Работа состоит из введения, семи глав, заключения и списка литературы ( наименований). Основной текст диссертации (без приложений и списка литературы) занимает 5 страниц. На основе предложенных методов разработана система верификации драйверов ОС Linux. Система верификации драйверов ОС Linux разработана в рамках проектов отдела Технологий программирования Института системного программирования РАН при непосредственном участии автора в качестве руководителя и участника разработки основных компонентов системы верификации. Автор выражает свою признательность всем участникам данных проектов. Особый вклад в работу внесли А. В.Хорошилов, Е. М.Новиков, П. Е.Швед. Прежде, чем приступить к обзору различных существующих методов верификации драйверов устройств ОС Linux рассмотрим подробно ядро ОС Linux и организацию его разработки и развития. Ядро ОС Linux является одним из самых динамично развивающихся и востребованных проектов в мире. Разработку ядра начал Линус Торвальдс в году. В настоящее время в подготовке каждого нового релиза ядра ОС Linux участвуют более человек, распределенных по всему миру [|. Релизы выпускаются в среднем раз в 2-3 месяца. Начиная с ядра версии 2. На сегодняшний день размер исходного кода ядра составляет более млн. Следует отметить тот факт, что помимо официальной, так называемой оригинальной (от англ. ОС Linux, которую выпускает Линус Торвальдс, объединяя разработки сообщества разработчиков ядра со своими, существует большое количество других веток разработки ядра. Например, как правило, разработчики различных дистрибутивов Linux поддерживают свои версии ядра. Об этом говорят, например, разработчики дистрибутивов Red Hat Enterprise Linux, openSUSE и Debian. Подсис . Рис 1. Есть ветки ядра, в которых основы операционной системы реализуются принципиально иначе по сравнению с оригинальной версией (, ]. С течением времени изменения, интересные широкому кругу лиц, из различных веток разработки попадают в оригинальное ядро (, ]. Схема устройства ядра ОС Ьших представлена на 1. Ядро состоит из основной части (“сердцевины”) и драйверов устройств.