Введение к работе
Актуальность темы. Драйверы устройств являются одной из самых
главных составляющих операционной системы. По этой причине, предъявляются повышенные требования к надежности и эффективности драйверов, так как одна неверная операция может привести к сбою операционной системы или снижению скорости работы устройства. Помимо этого, разработчику драйверов необходимо знать внутренние особенности строения операционных систем. Поэтому разработка драйверов относится к одной из самых сложных и ответственных отраслей программирования.
Как правило, новые устройства поставляются с драйверами, которые были написаны фирмой-производителем самого устройства. Разработчики драйверов этих организаций отлично знают спецификацию нового устройства, но не всегда хорошо понимают внутреннюю структуру той операционной системы, для которой разрабатывается драйвер. Помимо этого, иногда драйверы одного устройства вызывают сбой в драйвере другого устройства, так как довольно сложно протестировать взаимодействие между специфичными устройствами. В силу этих причин драйвер стороннего производителя имеет меньшую надежность по сравнению со стандартными драйверами операционной системы.
Исследования ошибок в подсистемах ядра операционных систем Linux и Open BSD показывают, что количество проблем в драйверах в среднем от 3 до 7 раз больше, чем в остальном коде ядра. Такое количество ошибок в драйверах отрицательно сказывается на надежности операционной системы в целом.
Наиболее трудно в драйверах обнаружить ошибки синхронизации. Так как к драйверу зачастую может обращаться сразу несколько программ, то он должен правильно обрабатывать асинхронные запросы. Для этого в драйверах применяются примитивы синхронизации: спин-блокировки, мьютексы, семафоры и другие. Наибольшее количество ошибок в драйверах случается именно из-за ошибок синхронизации, которые приводят к блокировкам и состояниям гонки за ресурсы.
Приведенные аргументы свидетельствуют о необходимости разработки формального метода анализа исходного кода драйверов с целью обнаружения в них ситуаций, приводящих к блокировкам и состояниям гонки за ресурсы.
Объектом исследования являются драйверы операционной системы Linux.
Предметом исследования являются примитивы взаимодействия и синхронизации в драйверах Linux, а также методы их верификации.
Цели диссертационной работы. Целью работы является разработка метода верификации драйверов операционной системы Linux на основе процессной семантики.
Задачи исследования. Для достижения указанной цели в диссертации поставлены и последовательно решены следующие задачи:
исследованы наиболее типичные проблемы в драйверах операционных систем и выявлена актуальность проблемы повышения надежности драйверов;
проведен анализ уже существующих систем верификации драйверов и сформулированы их основные недостатки;
разработан формальный метод обнаружения блокировок и состояний гонки в драйверах Linux;
на основе процессной семантики разработан инструментарий для верификации драйверов операционной системы Linux.
Методы исследований. В диссертации используются методы семантической теории языков распределенного программирования, методы построения трансляторов и статического анализа кода.
Научная новизна. В работе присутствуют следующие аспекты научной новизны:
предложен новый, основанный на семантической теории языков программирования, метод анализа драйверов с целью обнаружения в них ситуаций, приводящих к блокировкам и состояниям гонки;
расширена семантическая модель Ю.П. Кораблина для анализа драйверов и доказано, что семантическое значение модели драйверов может быть представлено конечной системой рекурсивных уравнений;
показана применимость предложенного подхода для анализа драйверов операционных систем семейства Linux.
Теоретическая значимость. Теоретические результаты работы:
на основе проведенного анализа современных инструментов верификации объектов синхронизации разработан семантический метод, позволяющий автоматизировать процесс анализа исходного кода драйверов с целью обнаружения в них блокировок и состояний гонки;
доказана корректность представления семантических значений схем программ с помощью конечной системы рекурсивных уравнений.
Практическая значимость. В работе:
разработан семантический метод, позволяющий автоматизировать процесс анализа исходного кода драйверов с целью обнаружения в них ситуаций, приводящих к блокировкам и состояниям гонки;
разработан инструмент верификации драйверов Linux, основанный на построении для исходного текста драйверов модели на языке асинхронных функциональных схем и последующим семантическим анализом полученной модели.
Внедрение. Предложенный метод и разработанный инструментарий были успешно внедрены в производственный процесс ООО «Исследовательский центр Самсунг», ООО «Инсайт» и в учебный процесс Российского государственного социального университета.
Апробация. Основные результаты работы докладывались: на Всероссийском конкурсе научно-исследовательских работ студентов и аспирантов в области информатики и информационных технологий (г. Белгород, 2012), семинарах кафедр информационной безопасности и программной инженерии и моделирования информационных систем и сетей РГСУ, семинаре Института системного программирования РАН.
Публикации. По теме диссертационной работы опубликованы 8 печатных работ, из них 4 в изданиях по перечню ВАК.
Объем и структура работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы и двух приложений. Общий объем основ- ного текста составляет 140 страниц, в том числе 15 рисунков. Список литературы состоит из 143 наименований.
