Разработка и применение метода верификации драйверов операционной системы Linux на основе процессной семантики тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Павлов, Евгений Геннадьевич

• Павлов, Евгений Геннадьевич
• кандидат технических наук
• 2013

Оглавление диссертации кандидат технических наук Павлов, Евгений Геннадьевич

Оглавление.

Введение.

Глава 1 Обзор исследований в области разработки драйверов.

1.1 Анализ методов повышения надежности операционных систем.

1.1.1 Автоматизация разработки драйверов.

1.1.2 Использование языка более высокого уровня.

1.1.3 Тестирование и верификация драйверов.

1.1.4 Запуск драйверов в специальной безопасной среде.

1.1.5 Ограниченный доступ к привилегированному режиму.

1.1.6 Построение операционных систем, устойчивых к сбоям.

1.1.7 Анализ рассмотренных методов.

1.2 Инструменты для верификации драйверов операционных систем.

1.2.1 Static Driver Verifier.

1.2.2 SLICx.

1.2.3 DDVerify.

1.2.4 Linux Driver Verification.

1.3 Вывод по главе 1.

Глава 2 Анализ драйверной модели операционной системы Linux.

2.1 Типы драйверов Linux.

2.1.1 Символьные драйверы устройств.

2.1.2 Блочные драйверы устройств.

2.2 Ошибки в драйверах Linux.

2.2.1 Взаимное исключение.

2.2.2 Очередь ожидания.

2.2.3 Тасклеты и очереди отложенных действий.

2.2.4 Прерывания.

2.2.5 Порты и память ввода/вывода.

2.2.6 Использование памяти.

2.2.7 Типичные ошибки в драйверах Linux.

2.3 Объекты синхронизации в ядре.

2.3.1 Атомарные операции.

2.3.2 Спин-блокировки.

2.3.3 Семафоры.

2.3.4 Условные переменные.

2.3.5 Секвентные блокировки.

2.4 Выводы по главе 2.

Глава 3 Применение процессной семантики для верификации драйверов.

3.1 Язык асинхронных функциональных схем.

3.2 Формальная семантика АФС-программ.

3.3 Аксиоматизация свойств семантической области.

3.4 Эквациональная характеризация априорных семантических значений.

3.5 Априорная семантика функциональных процессов.

3.6 Процессная семантика каналов связи и семантика АФС-программ.

3.7 Семантика основных элементов языка программирования Си.

3.7.1. Операционная семантика линейных операторов и выражений.

3.7.2 Операционная семантика условий и операторов выбора.

3.7.3 Операционная семантика циклов.

3.7.4 Операционная семантика break, continue и return.

3.7.5 Операционная семантика goto.

3.7.6 Операционная семантика функций.

3.8 Семантика объектов синхронизации драйверов Linux.

3.8.1 Операционная семантика условных переменных.

3.8.2 Операционная семантика спин-блокировок.

3.8.3 Операционная семантика спин-блокировок чтения-записи.

3.8.4 Операционная семантика семафоров.

3.8.5 Операционная семантика семафоров чтения-записи.

3.8.6 Операционная семантика мьютексов.

3.8.7 Атомарные переменные.

3.9 Пример верификации драйвера на основе семантических моделей.

ЗЛО Разделяемые ресурсы.

3.10.1 Разделяемые переменные.

3.10.2 Методы устранения состояния гонок.

3.11 Сравнительный анализ с методом проверки моделей.

3.12 Выводы по главе 3.

Глава 4 Разработка инструментальной системы верификации драйверов Linux.

4.1 Препроцессор.

4.2 Транслятор кода драйвера в язык АФС.

4.3 Преобразование АФС-программы в систему рекурсивных уравнений.

4.4 Анализатор системы рекурсивных уравнений.

4.5 Особенности структуры верификатора.

4.6 Экспериментальная оценка эффективности метода.

4.7 Оценка эффективности метода процессной семантики.

4.8 Выводы по главе 4.

Введение диссертации (часть автореферата) на тему «Разработка и применение метода верификации драйверов операционной системы Linux на основе процессной семантики»

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

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

На заре рождения операционных систем драйверы были написаны небольшой группой программистов, прекрасно знающих оборудование и систему. Конечно, операционные системы того времени были гораздо менее объемные по коду и, как правило, эти системы работали на стандартизированном оборудовании. Для сравнения, в современное ядро Linux включено свыше 3200 драйверов, в создании которых участвовало более 300 программистов различной квалификации [142], а Microsoft Windows Vista поставляется в комплекте со свыше 30000 драйверами.

В [50] авторы исследовали общее количество ошибок в подсистеме ядра в операционных системах Linux и OpenBSD и пришли к выводу, что количество ошибок в драйверах в среднем от 3 до 7 раз больше, чем в оставшемся коде ядра.

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

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

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

Объектом исследования являются драйверы операционной системы Linux.

Предметом исследования являются примитивы взаимодействия и синхронизации в драйверах Linux, а также методы их верификации.

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

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

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

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

• разработан формальный метод обнаружения блокировок и состояний гонки в драйверах Linux;

• на основе процессной семантики разработан инструментарий для верификации драйверов операционной системы Linux.

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

Научная новизна. В работе присутствуют следующие аспекты научной новизны:

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

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

• показана применимость предложенного подхода для анализа драйверов операционных систем семейства Linux.

Теоретическая значимость. Теоретические результаты работы:

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

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

Практическая значимость. В работе:

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

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

Положения, выносимые на защиту.

1. Семантическая модель драйверов операционной системы Linux.

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

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

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

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

Предложенный метод и разработанный инструментарий были успешно внедрены в производственный процесс ООО «Исследовательский центр Самсунг», ООО «Инсайт» и в учебный процесс Российского государственного социального университета.

Основные результаты работы докладывались: на Всероссийском конкурсе научно-исследовательских работ студентов и аспирантов в области информатики и информационных технологий (город Белгород, 2012), семинарах кафедры Информационной безопасности и программной инженерии РГСУ.

Публикации. По теме диссертации опубликовано 8 работ, из них 4 в изданиях по перечню ВАК.

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

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Павлов, Евгений Геннадьевич

4.8 Выводы по главе 4

1. Разработано инструментальное средство для верификации драйверов Linux, реализованное на основе теории, разработанной в третьей главе.

2. Проведена апробация разработанной верификационной системы для драйверов операционной системы Linux.

3. Разработанным инструментальным комплексом было проверено более 1200 драйверов ядра Linux 2.6.32-5, для каждого драйвера была построена модель на языке АФС и получена соответствующая ей система рекурсивных уравнений. Корректность построенных моделей обосновывается выборочной ручной проверкой 300 построенных моделей драйверов. Данный анализ занял около 50 минут на персональном компьютере. Экспериментальные результаты доказывают масштабируемость данного метода и применимость к драйверам ядра Linux.

124

Заключение

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

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

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

3. На основе предложенного метода реализован инструментальный комплекс для верификации драйверов операционной системы Linux. Данный инструментальный комплекс доказывает применимость предложенного автором метода для драйверов Linux.

4. Разработанным инструментальным комплексом было проверено более 1200 драйверов ядра Linux 2.6.32-5, для каждого драйвера была построена модель на языке АФС и получена соответствующая ей система рекурсивных уравнений. Корректность построенных моделей обосновывается выборочной ручной проверкой 300 построенных моделей драйверов. Данный анализ занял около 50 минут на персональном компьютере. Экспериментальные результаты доказывают масштабируемость данного метода и применимость к драйверам ядра Linux.

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

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

7. Предложенный метод и разработанный инструментарий были успешно внедрены в производственный процесс ООО «Исследовательский центр Самсунг», ООО «Инсайт» и в учебный процесс Российского государственного социального университета.

126

Список литературы диссертационного исследования кандидат технических наук Павлов, Евгений Геннадьевич, 2013 год

1. Аветисян А.И. Современные методы статического и динамического анализа программ для автоматизации процессов повышения качества программного обеспечения // Автореферат дис. . д-ра техн. наук. М., 2012. 37 с.

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

3. Ахо A.B., Лам М.С., Сети Р., Ульман Д.Д. Компиляторы: принципы, технологии и инструментарий, 2-е изд.: Пер. с англ. М.: ООО «И.Д. Вильяме», 2008. 1184 с.

4. Гук М.Ю. Аппаратные средства IBM PC. Энциклопедия, 3-е изд. СПб.: Питер, 2006. 1072 с.

5. Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.

6. Комиссарова В. Программирование драйверов для Windows СПб.: БХВ-Петербург, 2007. 247 с.

7. Кораблин Ю.П. Семантика языков программирования. М.: Изд-во МЭИ, 1992. 100 с.

8. Кораблин Ю.П. Семантические методы анализа распределённых систем // Автореферат дис. . д-ра техн. наук. М., 1994. 40 с.

9. Кораблин Ю.П., Налитов С.Д. Язык асинхронных функциональных схем -концепция распределенного программирования // Программирование. АН СССР. 1989. № 6. С. 35-45.

10. Кораблин Ю. П., Павлов Е. Г. Разработка верификатора объектов синхронизации драйверов для операционной системы Linux на основе процессной семантики // Программная инженерия. 2012. № 8. С. 2-10.

11. Кораблин Ю.П., Павлов Е.Г. Вопросы верификации драйверов Linux на основе процессной семантики // Ученые записки РГСУ. 2012. №7. С. 165

12. Кораблин Ю.П., Павлов Е.Г. Разработка инструментов верификации драйверов на основе семантических моделей // Программные продукты и системы. 2012. № 1. С. 128-134.

13. Кораблин Ю.П., Павлов Е.Г. Разработка инструментальных средств анализа драйверов операционной системы Linux // Программные продукты и системы. 2012. № 3. С. 160-165.

14. Костарев А.Н. Разработка инструментального комплекса для создания и семантического анализа распределенных информационных систем // Автореферат дис. . канд. техн. наук. М., 2004. 20 с.

15. Кулаков В. Программирование на аппаратном уровне. Специальный справочник. 2-е изд. СПб.: Питер, 2003. 847 с.

16. Курочкин В.М. Семантика языков программирования: Сб. статей под ред. Курочкина В.М. М.: изд-во «Мир», 1980. 400 с.

17. Кутепов В.П., Кораблин Ю.П. Язык граф-схем параллельных алгоритмов. // Программирование. АН СССР. 1978. № 1. С. 3-11.

18. Лав Р. Разработка ядра Linux, 2-е изд.: Пер. с англ. М. : ООО «И.Д. Вильяме», 2006.448 с.

19. Мутилин B.C., Новиков Е.М., Страх A.B., Хорошилов A.B., Швед П.Е. Архитектура Linux Driver Verification. // Труды Института системного программирования РАН. 2011. Т. 20. С. 163-187.

20. Несвижский В. Программирование аппаратных средств в Windows, 2-е изд., перераб. и доп. СПб.: БХВ-Петербург, 2008. 528 с.

21. Они У. Использование Microsoft Windows Driver Model, 2-е изд: Пер с англ. СПб.: Питер, 2007. 764 с.

22. Орвик П., Смит Г. Windows Driver Foundation. Разработка драйверов: Пер. с англ. М.: Изд-во «Русская Редакция»; СПб.: БХВ- Петербург, 2008. 880 с.

23. Родригес, К.З., Фишер Г., Смолски С. Linux: азбука ядра: Пер. с англ. М.: КУДИЦ-ПРЕСС, 2007. 584 с.

24. Руссинович М., Соломон Д. Внутреннее устройство Microsoft Windows: Windows Server 2003, Windows XP и Windows 2000, 4-е изд.: Пер. с англ. М.: Издательство «Русская редакция»; СПб.: Питер, 2006. 992 с.

25. Солдатов, В. П. Программирование драйверов Windows, 3-е изд., перераб. и доп. М: ООО «Бином-Пресс», 2006. 576 с.

26. Таненбаум Э. Современные операционные системы, 2-е изд.: Пер. с англ. СПб.: Питер, 2007. 1038 с.

27. Шрайбер С. Недокументированные возможности Windows 2000: Пер. с англ. СПб.: Питер, 2002. 544 с.

28. Artho C. Finding faults in multi-threaded programs // Master's thesis. Institute of Computer Systems, Federal Institute of Technology. 2001. Zurich, Switzerland. 128 p.

29. Baier C., Katoen J.P. Principles of Model Checking. MIT Press, 2008. 984 p.

30. Ball Т., Majumdar R., Millstein Т., Rajamani S.K. Automatic predicate abstraction of С programs // In Proceedings of the Conference on Programming language design and implementation. June 20-22, 2001. Snowbird, Utah, USA, pp. 203-213.

31. Ball Т., Rajamani S.K. Bebop: A symbolic model checker for Boolean programs // In SPIN Model Checking and Software Verification. Springer-Verland Limited, London, 2000, pp. 113-130.

32. Ball Т., Rajamani S.K. The SLAM project: Debugging system software via static analysis // In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 16-18, 2002. Portland, OR, USA, pp. 1-3.

33. Baker A., Lozano J. The Windows 2000 Device Driver Book, A Guide for Programmers, 2-nd edition. Prentice Hall PTR, 2002. 480 p.

34. Banerjee U., Bliss В., Ma Z., Petersen P. A Theory of Data Race Detection // Proceedings of the workshop on Parallel and distributed systems: testing anddebugging. July 17-20,2006. Portland, ME, USA. pp. 69-78.

35. Basili V., Perricone B. Software Errors and Complexity: An Empirical Investigation // Communications of the ACM, 1984. Vol. 27. № 1, pp. 42-52.

36. Basler G., Kroening D., Weissenbacher G. SAT-based summarisation for Boolean programs // In SPIN Workshop on Model Checking of Software. SpringerVerlag Berlin, Heidelberg, 2007, pp. 131-148.

37. Ben-Ari M. Principles of the Spin Model Checker, 1st edition. Springer, 2008. 236 p.

38. Bevier W.R. Kit: A Study in Operating System Verification // IEEE Transactions on Software Engineering, 1989. Vol. 15. № 11, pp. 1382-1396.

39. Blazy S., Dargaye Z., Leroy X. Formal verification of a C compiler front-end // FM 2006: Formal Methods. Springer-Verlag Berlin Heidelberg, 2006, pp. 460475.

40. Bornât R. Proving pointer programs in Hoare Logic // Mathematics of Program Construction. Springer-Verlag Berlin Heidelberg, 2000, pp. 102-126.

41. Brookes S. Retracing the semantic of CSP // Communicating Sequential Processes: the First 25 Years. Springer-Verlag Berlin Heidelberg, 2005, pp. 1-14.

42. Brookes S., Roscoe A.W. An improved failures model for CSP // Proc. Seminar on concurrency, LNCS, 1984. № 197, pp. 281-305.

43. Chaki S., Clarke E., Groce A., Jha S., and Veith H. Modular verification of software components in C // IEEE Transactions on Software Engineering, 2004. Vol. 30. № 6, pp. 388-402.

44. Chou A., Yang J., Chelf B., Hallem S., and Engler D. An Empirical Study of Operating System Errors // Proceedings of the 18th ACM Symposium on Operating Systems Principles. October 21-24, 2001. Chateau Lake Louise, Banff, Canada, pp. 73-88.

45. Chubb P. Get More Device Drivers out of the Kernel! // Proceedings of the

46. Linux Symposium. July 21-24, 2004. Ottawa, Ontario, Canada, pp. 149-162.

47. Clarke E.M., Grumberg O., Long D.E. Model checking and abstraction // ACM

48. Transactions on Programming Languages and Systems, 1994. Vol. 16. № 5, pp. 1512-1542.

49. Clarke E., Kroening D., and Lerda F. A tool for checking ANSI-C programs // Tools and Algorithms for the Construction and Analysis of Systems. SpringerVerlag Berlin Heidelberg, 2004, pp. 168-176.

50. E. Clarke E., Kroening D., Sharygina N., and Yorav K. SATABS: SAT-based predicate abstraction for ANSI-C // Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag Berlin Heidelberg, 2005, pp. 570574.

51. Clarke E.M., Grumberg O., Jha S., Lu Y., and Veith H. Counterexample-guided abstraction refinement // Computer Aided Verification. Springer-Verlag Berlin Heidelberg, 2000, pp. 154-169.

52. Cleaveland R., Parrow J., and Steffen B. The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems // ACM Transactions on Programming Languages and Systems, 1993. Vol. 15. № 1, pp. 3672.

53. Cobleigh J. M., Clarke L.A., Osterweil L.J. FLA VERS: a Finite State Verification Technique for Software Systems // IBM Systems Journal, 2002. Vol. 41. № l,pp. 140-165.

54. Conway C.L., Edwards S.A. NDL: A Domain Specific Language for Device Drivers // Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems. June 11-13, 2004. Washington, DC, USA.

55. Cook B., Kroening D., and Sharygina N. Symbolic model checking for asynchronous Boolean programs // Model Checking Software. Springer-Verlag Berlin, 2005, pp. 75-90.

56. Corbet J., Rubini A., Kroah-Hartman G. Linux Device Drivers, 3-rd edition. O'Relly, 2006. 616 p.

57. Cousot P. Verification by abstract interpretation // Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, January 9-11, 2003. New York, NY, USA. Springer-Verlag London, pp. 20-24.

58. Dijkstra E. W. Cooperating sequential processes. // In: Programming Languages, Genuys F. (editor). Academic Press, 1968, pp. 43-112.

59. Ehrich H.D., Caleiro C. Specifying Communication in Distributed Information Systems //Acta Informática, 2000. Vol. 36. № 8, pp. 591-616.

60. Elphinstone K., Klein G., Derrin P., Roscoe T. Towards a practical, verified kernel // Proceedings of the 11th Workshop on Hot Topics in Operating Systems, May 7-9,2007. San Diego, CA, USA. Article No. 20.

61. Erosa A., Hendren L.J. Taming control flow: a structured approach to eliminating goto statements // In Proceedings of 1994 IEEE International Conference on Computer Languages, May 16-19, 1994. Toulouse, France, pp. 229-240.

62. Engler D., Ashcraft K. RacerX: Effective, Static Detection of Race Conditions and Deadlocks // Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003. Bolton Landing, NY, USA. pp. 237252.

63. Ernst M.D., Perkins J.H., Guo P. J., McCamant S., Pacheco C., Tschantz M. S., and Xiao C. The Daikon system for dynamic detection of likely invariants // Science of Computer Programming, 2007. Vol. 69, № 1-3, pp. 35^5.

64. Fujimoto R.M., Feng H.C. A Shared Memory Algorithm and Proof for the Generalized Alternative Construct in CSP // International Journal of Parallel Programming, 1987. Vol. 16. № 3, pp. 215-241.

65. Ganapathy V., Balakrishnan A., Swift M.M., and Jha S. Microdrivers: A New Architecture for Device Drivers // The 11th Workshop on Hot Topics in Operating Systems (HotOS XI). May 7-9, 2007. San Diego, California, USA. Article No. 15.

66. Godefroid P. Software model checking: The VeriSoft approach // Formal Methods in System Design (FMSD), 2005. Vol. 26. № 2, pp. 77-101.

67. Graf S., Saidi H. Construction of abstract state graphs with PVS // Proceedings of the 9th International Conference on Computer Aided Verification. June 2225,1997. Haifa, Israel. Springer-Verlag London, pp. 72-83.

68. Gurevich Y., Huggins J.K. The Semantics of the C Programming Language // Selected Papers from the Workshop on Computer Science Logic. September 1317,1993. Swansea, United Kingdom, Springer-Verlag London, pp. 274-308.

69. Gurfinkel A., Wei O., and Chechik M. Yasm: A software model-checker for verification and refutation // In Computer Aided Verification. Springer-Verlag Berlin Heidelberg, 2006. Vol. 4144 of LNCS, pp. 170-174.

70. Hennessy M. Algebraic Theory of Processes. The MIT Press, 1988. 284 p.

71. Henzinger T.A., Jhala R., Majumdar R., and Qadeer S. Thread-modular abstraction refinement // In Computer Aided Verification. Springer-Verlag Berlin Heidelberg, 2003. Vol. 2725 of LNCS, pp. 262-274.

72. Henzinger T.A., Jhala R., Majumdar R., and Sutre G. Lazy abstraction // Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming language. January 16-18, 2002. Portland, OR, USA. ACM Press, pp. 58-70.

73. Herder J.N., Bos H., Gras B., Homburg P. and Tanenbaum A.S. Fault Isolation for Device Drivers // 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks. June 29-July 22, 2009. Estoril, Lisbon, Portugal, pp. 33-42.

74. Herder J.N., Bos H., Gras B., Homburg P., Tanenbaum A.S. Failure Resilience for Device Drivers // The 37th International Conference on Dependable Systems and Networks. June 25-28,2007. Edinburgh, UK, pp. 41-50.

75. Herder J.N., Bos H., Gras B., Homburg P., Tanenbaum A.S. Construction of a

76. Highly Dependable Operating System // Proceedings of the Sixth European Dependable Computing Conference, October 18-20, 2006. Coimbra, Portugal. IEEE Computer Society 2006, pp. 3-12.

77. Herder J.N., Bos H., Gras B., Homburg P., Tanenbaum A.S. Reorganizing UNIX for Reliability // Advances in Computer Systems Architecture. Springer Berlin Heidelberg, 2006, pp. 81-94.

78. Herder J.N., Bos H., Gras B., Homburg P. and Tanenbaum A.S. The Architecture of a Reliable Operating System // Proc. ASCI 2006, pp. 74-81.

79. Hoare C.A.R., Brookes S., and Roscoe A.W. A Theory of Communicating Sequential Processes // Journal of the ACM (JACM), 1984. Vol. 31. № 3, pp. 560599.

80. Hoare, C.A.R. Communicating sequential processes. Prentice-Hall, 1984. 256 p.

81. Erickson J., Musuvathi M., Olynyk K. Effective Data-Race Detection for the Kernel // Proceedings of 9th USENIX Symposium on Operating Systems Design and Implementation. October 4-6, 2010. Vancouver, BC, Canada, pp. 151-162.

82. Isaev I., Sidorov D. The Use of Dynamic Analysis for Generation of Input Data that Demonstrates Critical Bugs and Vulnerabilities in Programs // Programming and Computing Software, 2010. Vol. 36. № 4, pp. 225-236.

83. Klein G. Operating System Verification An Overview // Sadhana, 2009. Vol. 34. № 1, pp. 26-69.

84. Korablin Y.P. Deciding equivalence of functional schemes for parallel programs // Mathematical Centre, Department of Computer Science, Research Report IW 200/82, Amsterdam. 1982. 33 p.

85. Lattner C., Adve V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation // Proceedings of the 2004 International Symposiumon Code Generation and Optimization (CGO'04). March 20-24, 2004. San Jose, CA, USA, pp. 75-86.

86. Leroy X., Blazy S. Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations // Journal of Automated Reasoning, 2008. Vol. 41. №1, pp. 1-31.

87. Levine J. R. Flex & Bison. O'Relly, 2009. 304 p.

88. McMillan K.L. The SMV system // Technical Report CMU-CS-92-131. Carnegie Mellon University, 1992. 27 p.

89. Milner R. Communication and concurrency. Prentice Hall, 1989. 300 p.

90. Mühlberg J., Lüttgen G. BLASTING Linux Code. // In the proceedings of 11th International Workshop on Formal Methods for Industrial Critical Systems. August 26-27,2006. Bonn, Germany, pp. 211-226.

91. Naik M. Chord: A Versatile Platform for Program Analysis // In the proceedings of the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI). June 4-8, 2011. San Jose, California.

92. Nesov V. Automatically Finding Bugs in Open Source Programs // Electronic

93. Communications of the EASST, 2009. Vol. 20.

94. Ostrand T., Weyuker E., and R. Bell. Where the Bugs Are // Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis. July 11-14, 2004. Boston, MA, USA, pp. 86-96.

95. Ostrand T.J., Weyuker E.J. The Distribution of Faults in a Large Industrial Software System // Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis. July 22-24, 2002. Rome, Italy, pp. 5564.

96. Papaspyrou N. S. A Formal Semantics for the C Programming Language // Doctoral Dissertation. National Technical University of Athens, 1998. Athens, Greece. 253 p.

97. Park J.C., Choi Y.H., Kim T. Domain Specific Code Generation For Linux Device Driver // Proceedings of the 10th International Conference ICACT 2008. February 17-20, 2008. Phoenix Park, Korea. Vol. 1, pp. 101-104.

98. Plotkin G.D.A Structural Approach to Operational Semantics // Technical Report DAIMI FN-19, Computer Science Department, Aarhus University. Aarhus, Denmark. September 1981. 132 p.

99. Post H., Kuchlin W. Integrated Static Analysis for Linux Device Driver Verification // Proceedings of the 6th international conference on Integrated formal methods (IFM'07). July 2-5, 2007. Oxford, UK, pp. 518-537.

100. Qadeer S., Wu D. KISS: Keep it simple and sequential // Proceedings of the conference on Programming language design and implementation (PLDI). June 9-11,2004. Washington, DC, USA, pp. 14-24.

101. Renzelmann M.J., Swift M.M. Decaf: Moving Device Drivers to a Modem Language // In Proceedings of the USENIX Annual Technical Conference. June 1419,2009. San Diego, CA, USA.

102. Reynolds J. Separation Logic: A Logic for Shared Mutable Data Structures // Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS). July 22-25 , 2002. Copenhagen, Denmark, pp. 55-74.

103. Roscoe A.W. The theory and practice of concurrency. Prentice Hall, 1997. 512 P

104. Roscoe A.W. Denotational semantics for occam // Proceeding Seminar on Concurrency Carnegie-Mellon University. July 9-11, 1984. Pittsburgh, PA, USA, pp. 306-329.

105. Roscoe A.W., Wu Z. Verifying Statemate Statecharts Using CSP and FDR // Formal Methods and Software Engineering. Springer-Verlag Berlin Heidelberg, 2006, pp. 324-341.

106. Savage S., Burrows M., Nelson G., Sobalvarro P., and Anderson T. Eraser: a dynamic data race detector for multi-threaded programs // ACM Transactions on Computer Systems, 1997. Vol. 15. № 4, pp. 391^111.

107. Schwoon S. Model-Checking Pushdown Systems // PhD thesis. Technical University of Munich. 2002. Munich, Germany. 202 p.

108. Serebryany K., Iskhodzhanov T. ThreadSanitizer data race detection in practice // Proceedings of the Workshop on Binary Instrumentation and Applications (WBIA). December 12-12, 2009. New York, NY, USA, pp. 62-71.

109. Swift M.M, Bershad B.N., Levy H.M. Improving the Reliability of Commodity Operating Systems // Operating Systems Review, 2003. Vol. 37. № 5, pp. 207222.

110. Tanenbaum A.S., Herder J.N., and Bos H. Can We Make Operating Systems Reliable and Secure? // Computer, 2006. Vol. 39. № 5, pp. 44-51.

111. Thibault S., Marlet R., and Consel C. Domain-specific languages: from design to implementation, application to video device drivers generation // EEE Transactions on Software Engineering, 1999. Vol. 25. № 3, pp. 363-377.

112. Witkowski T. Formal verification of Linux device drivers // Master's thesis.

113. Dresden University of Technology. 2007. Dresden, Germany. 90 p.

114. Xie Y., Aiken A. Saturn: A SAT-based tool for bug detection // Computer Aided Verification (CAV). Vol. 3576 of LNCS. Springer-Verlag Berlin Heidelberg,2005, pp. 139-143.

115. Yang J., Twohey P., Engler D., and Musuvathi M. Using model checking to find serious file system errors // ACM Transactions on Computer Systems (TOCS),2006. Vol. 24. № 4, pp. 393^123.

116. AFS2REQS Электронный ресурс. URL: https://github.com/lucenticus/ AFS2REQS (дата обращения 10.02.2013)

117. Beckman N.E. A Survey of Methods for Preventing Race Conditions Электронный ресурс. // May 10, 2006 URL: http://www.cs.cmu.edu/~nbeckman/papers/racedetectionsurvey.pdf (дата обращения 14.10.2010).

118. Bison GNU parser generator Электронный ресурс. URL: http://www.gnu.org/software/bison/ (дата обращения 29.08.2011).

119. Driver Synchronization Verifier Электронный ресурс. URL: https://github.com/lucenticus/DSV (дата обращения 10.02.2013)

120. FDR «Formal Systems (Europe) Ltd» Электронный ресурс. URL: http://www.fsel.com/ (дата обращения 06.07.2012).

121. Flex: The Fast Lexical Analyzer Электронный ресурс. URL: http://flex.sourceforge.net/ (дата обращения 28.08.2011).

122. GNU General Public License Электронный ресурс. URL: http://www.gnu.org/licenses/gpl.html (дата обращения 15.03.2012)

123. Jungo Ltd Электронный ресурс. URL: http: //www.jungo.com (дата обращения 13.09.2010).

124. Microsoft Research Электронный ресурс. URL: http://research.microsoft.com/ (дата обращения 15.11.2010).

125. Microsoft Software Developer Library Электронный ресурс. URL: http://msdn.microsoft.com/ (дата обращения: 09.03.2010).

126. Naumann D.A. Theory for Software Verification Электронный ресурс. // Stevens Institute of Technology, 2009. URL: http://www.cs.stevens-tech.edu/~naumann/publications/theoryverif.pdf (дата обращения: 14.03.2010).

127. Official Minix3 site Электронный ресурс. URL: http://www.minix3.org/

128. The LLVM Compiler Infrastructure Электронный ресурс. URL: http://www.llvm.org/ (дата обращения: 01.03.2012).

129. Torvalds L. Linux kernel source tree Электронный ресурс. URL: http://www.kemel.org (дата обращения: 01.11.2009).

130. Windows Driver Kit (WDK) Электронный ресурс. // Washington: Microsoft

131. Corporation, 2007. URL: http://msdn.microsoft.com/en-us/library/windows /hardware/gg487428.aspx (дата обращения 10.02.2012).