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

На правах рукописи

^Г /

^ г

ПАВЛОВ ЕВГЕНИЙ ГЕННАДЬЕВИЧ

РАЗРАБОТКА И ПРИМЕНЕНИЕ МЕТОДА ВЕРИФИКАЦИИ ДРАЙВЕРОВ ОПЕРАЦИОННОЙ СИСТЕМЫ LINUX НА ОСНОВЕ ПРОЦЕССНОЙ СЕМАНТИКИ

Специальность 05.13.11 —

«Математическое и программное обеспечение вычислительных машин, комплексов и

компьютерных сетей»

АВТОРЕФЕРАТ

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

Москва-2013

3 О МАП 2013

005060670

Работа выполнена на кафедре «Моделирование информационных систем и сетей» Федерального государственного бюджетного образовательного учреждения высшего профессионального образования «Российский государственный социальный университет».

Научный руководитель: Кораблнп Юрий Прокофьевич

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

Официальные оппоненты: Назаров Александр Викторович

доктор технических наук, профессор, заведующий кафедрой 44-4 федерального государственного бюджетного образовательного учреждения высшего профессионального образования «Московский авиационный институт (национальный исследовательский университет)»

Басок Борис Моисеевич

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

Ведущая организация: Федеральное государственное бюджетное учреждение науки

«Институт системного анализа Российской академии наук»

Защита состоится «19» июня 2013 г. в 16 часов 30 минут на заседании диссертационного совета Д212.131.05 при МГТУ МИРЭА по адресу: г. Москва, пр-т Вернадского, д. 78, ауд. Д-412.

С диссертацией можно ознакомиться в библиотеке МГТУ МИРЭА

Автореферат разослан «17» мая 2013 г.

Ученый секретарь диссертационного совета к.т.н., доцент

сУ Е.Г. Андрианова

Общая характеристика работы Актуальность темы. Драйверы устройств являются одной из самых

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

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

Исследования ошибок в подсистемах ядра операционных систем Linux и Open BSD показывают, что количество проблем в драйверах в среднем от 3 до 7 раз больше, чем в остальном коде ядра. Такое количество ошибок в драйверах отрицательно сказывается на надежности операционной системы в целом.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4

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

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

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

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

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

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

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

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

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

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

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

5

ного текста составляет 140 страниц, в том числе 15 рисунков. Список литературы состоит из 143 наименований.

Содержание работы

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

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

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

Для верификации драйверов операционных систем семейства Windows компания Microsoft разработала программный пакет под названием Static Driver Verifier (далее SDV), поставляемый с 2006 года как часть Microsoft Windows Driver Development Kit. Данный верификатор основан на технологии SLAM, разработанный в Microsoft Research. Подобные инструменты были разработаны и для драйверов Linux. За основу был взят язык спецификаций SLIC и вместо SLAM используется верификатор на основе проверки моделей СВМС. На базе документации ядра были сформулированы некоторые правила для драйверов Linux, которые реализованы на языке SLICx. Таким образом, этот инструментарий позволил использовать стиль SDV для верификации драйверов Linux. Это средство выполнено в виде расширения для среды разработки Eclipse.

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

6

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

Исследования в области верификации драйверов активно ведутся и в России. В 2009 году на базе Института системного программирования Российской академии наук создан Центр верификации операционной системы Linux. Основным средством для верификации является инструментальный комплекс Linux Driver Verification (далее LDV).

Процесс верификации драйвера в LDV начинается с инициализации системы LDV-Core. Перед началом работы на основе архива с исходным кодом ядра Linux создается копия этого ядра со специально модифицированной подсистемой сборки. Далее LDV-Core запускает процесс компиляции драйверов, и одновременно с этим читается поток команд компиляции и линковки, выделяя из них те, которые относятся к верифицируемым драйверам. Затем создается для каждого типа драйвера одна или несколько моделей окружения, добавляя код моделей и проверок указанных правил корректности к соответствующим файлам драйвера. Далее код отправляется на вход верификатору (BLAST, CPAchecker и другие), который уже не имеет представления о том, что поданный ему на вход код является драйвером ядра операционной системы Linux. На настоящее время в LDV используются только верификаторы достижимости. Этот факт означает, что инструментарий предназначен лишь для выявления нарушений правил корректности.

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

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

Одной из ее обязанностей является информировать ядро о том, какие функции могут быть использованы пользовательским приложением. Когда драйвер выгружается из системы, вызывается функция выхода, которая производит операции освобождения ресурсов. Макросы module init и module_exit используется для сообщения точек входа и выхода из драйвера.

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

Анализ ядра Linux показывает, что около 40 % ошибок являются ошибками блокировки. Эти ошибки приводят к блокировке всей системы. Приведем пример возникновения блокировки, обнаруженный в коде драйвера soimdisa'sb/sb 16 csp.c ядра Linux 2.6.3:

spin_lock_irqsave(&p->chip-> reg lock, flags);

unsigned char *kbuf, *_kbuf;

kbuf= kmalloc(size, GFP KERN EL);

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

Второй по частоте появления ошибкой является обращение к нулевому указателю. Примером может служить код драйвера drivers/isdn/avmbl/capidrv.c, взятого из ядра Linux 2.4.1:

if {card == NULL) { printk(KERN_ERR "capidrv-%d'\ card->contrnr, id);

}

Функция printk вызывается только в том случае, если указатель на card равен NULL. Но этот указатель используется в функции printk для получения счетчика card->contrnr.

Еще одной частой ошибкой является обращение к уже освобожденной памяти. Примером может служить следующий код драйвера /driver/message/i2o/pci.c из ядра Linux 2.6.13:

struct i2o controller *c\

с = i2o_iop_alloc{)\

ilojopJreei);

put_device(c-> device.parent)',

Здесь функция ilojop allocQ выделяет память для структуры i2o controller при помощи kmalloc. После некоторых операций происходит освобождение памяти функцией i2o_iopfree. Но в следующей строке кода происходит обращение к только что освобожденной структуре с->device.parent.

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

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

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

Пусть заданными являются следующие синтаксические области (с учетом введенных расширений языка АФС для разделяемых переменных): Сот — множество элементарных команд с типичным элементом а; Ехр — множество булевских выражений с типичным элементом Ь; BConst - множество булевских констант, содержащее константы tt (тождественно истинное значение) и ff (тождественно ложное значение); RCom - множество команд ввода с типичным элементом read; WC от - множество команд вывода с типичным элементом write; GCom - множество значений команд асинхронного ввода с типичным элементом get;

SCom — множество значений команд асинхронного вывода с типичным элементом set;

CPLab — множество меток каналов и процессов с типичным элементами і и /; SVIJ— множество идентификаторов разделяемых переменных с типичным элементом лт;

CNom — множество номеров входов/выходов каналов с типичными элементами кчі;

Cmd— множество команд с типичным элементом с; CWait- множество команд ожидания с типичным элементом wait; ТЕхр — множество временных выражений типичным элементом time. Множество АФС-программ Prog с типичным элементом рг задается следующим образом:

рг ::= NET chart; shared var BEGINfproc END chart ::= CHANj::type(k):type(l) \ chant; chart2 type v.= ALL I ANY

shared var ::= SHARED VAR sv {, .vv} fproc ::= FUN i::c \ fproct ;fproc2

с ::= a | skip \ exit \ break \ wait(time) | read(i, Г) | \vrite(i, к) | get(i, Г) | set(i, к) | SEO(c {,c})

PAR(c {, с}) I ALT(gc) I LOOP(ALT(gc)) gc ::= g с I gc {; gc}

g ::= It I ff\ b I li ait(time) \ read(i, I) \ write(i, к) | get(i, I) \ set(i, k)

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

Определим семантические области, на которые отображаются значения АФС-программы. Предполагается, что заданными являются следующие семантические области:

1. Множество значений элементарных команд АСот с типичным элементом А.

2. Множество значений булевских выражений ВЕхр с типичным элементом В.

3. Множество значений команд ввода PICom с типичным элементом IN.

4. Множество значений команд вывода РОСот с типичным элементом OUT.

5. Множество взаимодействий РСот с типичным элементом у.

6. Множество Const, содержащее константы г (тождественное преобразование), 0 (останов), Т (тождественно-истинное значение) и F (тождественно ложное значение).

7. Элементы BREAK, EXIT и TIME, являющиеся значениями команд завершения цикла, завершения процесса и ожидания соответственно.

8. Множество значений команд асинхронного ввода PAICom с типичным элементом GET.

9. Множество значений команд асинхронного вывода PAOCom с типичным элементом SET.

10. Множество асинхронных взаимодействий РАСот с типичным элементом со.

Множество тестов и множество действий задается следующим образом: ß ::= Т I F I В I TIME I IN I OUT I GET \ SET \у\ш a::= r I 0 I A I IN I OUT \ GET \ SET \ у | со \ TIME \ BREAK \ EXIT Зададим семантическую функцию для функциональных процессов F: FProc —> SP, где FProc — множество функциональных процессов с типичным элементом fproc.

Hfproc^, fproc2l = FIfvroc^l II Hfproc2f, FIFUN i :: c] = CM,

где С: Cmd. -> SP есть функция, сопоставляющая командам языка АФС множества ВП. СМ = А С [skip] = г Cffexit] = EXIT Clbreaki = BREAK Clwait(time)l = TIME Cfread(i, Z)] = INul Clwrite(i,l)] = OUTik €lSEQ(Cl; c2)] = CJcJ о C|[c2] (С[[РЛй(сг;с2)1 = CIcJJiCIcz] ClALTdgc^gcJl = C^cJ + C^cJ CItt-»cl = Е[й]л£И

да -» c] = EI/Я л <cw C[b -» c] = ЕВДл CM

Clwait(time) -> c] = Clwciit(time)J л CM

C[read(i, 0 -> c] = C[read(U)]]A СИ

C[[ivrite(i,k) cj = С [write (i, fc)]A СИ

С[Ь00Р(Л/.Г(5с))] = (CJALT (gcW+

Clget(i, /)] - GETUI

C[se£(i,k)] = SETik

Clget(i,Q -» c] = C[5et(i,k)] л C[c]

C[set(f,fc) - c] = C[set(i, k)]j л CM

Определим семантическую функцию для выражений

Е: Expl -» ГЯ5Г

E[tt]] = Г

Eff/Л = F

ЕИ = В

Зададим функцию взаимодействия СР\D' х D' -> РСот U РАСот, где D' - множество с типичным элементом d'::= ß | а, определяемое следующим образом:

i Yi,k, если d[ = INlJc (IN1*) и d'2 = OUTlJC (OUT<■*) cp(d, dl = I й)к,„если d[ = СЕГ(Л (5ЯГи) «di= SETu{Gmj) или I если di = SfiTi.k и d2 = SET11, где к i V0 в противном случае.

Для преобразования программы на языке Си в программу на языке АФС в диссертации задана операционная семантика основных элементов языка Си (линейных операторов, условий, циклов, функций, оператора goto), а также элементов синхронизации ядра Linux (условных переменных, разделяемых переменных, спин-блокировок, семафоров, мьютексов, семафоров чтения-записи, спин-блокировок чтения-записи). При преобразовании исходного кода драйвера в программу на языке АФС наибольшее внимание уделяется взаимодействию между функциями драйвера, в частности - использование примитивов синхронизации. Линейные операторы языка Си не представляют для анализа программы особого интереса, поэтому на основе правила абстракции они преобразуются в пустые операторы skip. Булевские выражения языка Си на основе операции абстракции преобразуются на языке АФС в выражения b„ 11 и ff Линейное выполнение программы записывается на языке АФС при помощи оператора SEO. Так как в драйверах не происходит параллельное выполнение на уровне команд, то оператор PAR при моделировании не используется.

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

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

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

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

• препроцессор;

• транслятор кода драйвера в программу на языке АФС;

• модуль представления программы АФС в виде системы рекурсивных уравнений;

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

Схема работы верификатора представлена на рисунке 1.

Рисунок 1 Схема работы верификатора на основе процессной семантики Препроцессор

Препроцессор реализован в виде сценария на языке bash. В его обязанности входит подготовка кода драйвера к трансляции в язык АФС.

Исходный код драйвера поступает па вход препроцессора, который считывает файл Makefile драйвера и анализирует зависимости между файлами исходного кода модуля. Затем для каждого файла на языке Си препроцессор производит вызов компилятора командой gcc с ключом —Е: эта команда запускает препроцессор языка Си, который обрабатывает все операторы препроцессора языка Си (Uinclude, Mefine и другие). При необходимости подключения какого-либо заголовочного файла, препроцессор может искать недостающие файлы в директориях, которые указаны в его параметрах. На выходе препроцессора получается один файл исходного кода драйвера на языке Си. Этот файл передается на вход транслятора в язык АФС.

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

После всех подготовительных процедур препроцессор передает управление транслятору в язык АФС. В данном случае АФС выбран как основной язык для промежуточного представления структуры драйвера. Транслятор из языка Си в язык АФС будем называть front-end-транслятором, этот термин часто используется для трансляторов из исходного языка (в данном случае язык Си) в язык промежуточного представления (язык АФС).

Транслятор написан с использованием генераторов лексических анализаторов GNU Flex и синтаксических анализаторов GNU Bison.

В основе транслятора кода драйвера в язык АФС лежит реализация шаблона для анализатора языка Си, а также ранние версии компилятора GCC, синтаксис которого был задан с использованием Bison. Шаблон синтаксического анализатора был дополнен правилами для генерации абстрактного синтаксического дерева (далее АСД), помимо этого добавлено распознавание GCC-расширений языка Си (атрибуты, ассемблерные вставки, инициализация структур и др.). После лексического и синтаксического анализа кода драйвера на выходе получается абстрактное синтаксическое дерево программы. Далее это дерево используется для анализа структуры программы и для генерации программы на языке АФС.

Вначале транслятор ищет функцию module _in¡t{) и считывает название функции инициализации. Далее анализатор просматривает тело функции ини-

цианизации и находит функцию инициализации устройства, из этого вызова считывается идентификатор структуры файловых операций драйвера. Эта структура содержит указатели на операции open, close, read, write и другие. Именно данные операции и представляют особый интерес, так как они зачастую выполняются параллельно. Каждой операции драйвера соответствует функциональный процесс на языке АФС. Транслятор исследует каждую из этих функций и собирает информацию об использовании в них объектов синхронизации. Далее происходит анализ использования объектов синхронизации функций драйвера. Эти взаимосвязи и используются для генерации программы на языке АФС. На выходе после выполнения всех шагов Front-end записывает программу на языке АФС в файл с расширением .afs. Данный файл используется для дальнейшего анализа программы.

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

Следующий этап после представления драйвера на языке АФС - это преобразование программы на языке АФС в систему рекурсивных уравнений.

Для считывания программы на языке АФС при помощи утилит GNU Flex и GNU Bison реализован синтаксический анализатор, который строит абстрактное синтаксическое дерево (АДС) для каждого функционального процесса и канала.

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

Далее полученные априорные семантики объединяются посредством операции параллельной композиции в алгебре вычислительных последовательностей в единое АСД. Это объединение реализовано на основе определения операции параллельной композиции II.

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

Например, пусть у нас получилось следующее первое уравнение:

Рх = ГМ + ОиТ1Л о

Заменяя правые операнды операций «Л» и «°» на Р2 и Р3, получаем:

Рг = глр2 + оит1Л о Р3

Р2= А Рз = INi,2

Полученная система задает множество вычислительных последовательностей, сопоставляемое структуре драйвера. На выходе система рекурсивных уравнений записывается в файл с расширением .sent.

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

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

Данный анализатор реализован в виде сценария на языке Python. Сначала он проходит по ie/я-файлу и считывает систему рекурсивных уравнений. Затем анализатор проходит по полученной системе и ищет операции взаимодействия а) и останова 0. Для каждого найденной операции ищется последовательность событий, которая привела к данной ошибке. Для этого анализатор запускает рекурсивный поиск всех вхождений уравнения, в котором обнаружено некорректное поведение программы, в другие уравнения системы. После получения последовательности событий, которая привела к ошибке, на основе семантических функций производится преобразование данной последовательности в порядок команд на языке Си.

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

17

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

Модульная система верификатора позволяет адаптировать инструмент к программам самого разного назначения, для применения в новой сфере необходимо лишь переписать front-end. Исходный код верификатора написан на языке программирования Си и утилит Flex и Bison. Так как существуют реализации этих утилит для различных операционных систем, то данный верификатор является полностью переносимым. Однако для анализа определенных типов программ необходимо адаптировать front-end. Это связано с различной семантикой элементов синхронизации, а также особенностью реализации библиотеки для работы с потоками.

Помимо этого, область применения данного инструментария не ограничивается языком Си. При необходимости можно реализовать front-end для языков С++, Java. Поддержка нового языка программирования или новой платформы сводится к реализации транслятора целевого языка в язык АФС. Кроме того, для более точного построения модели программы на языке АФС можно использовать не исходный код программы, а его промежуточное представление. Это промежуточное представление можно получить на основе технологии LLVM для языков Си, С+ + и Objective С. Для языка Java можно строить модель программы на языке АФС на основе байт-кода виртуальной машины Java, что избавляет от необходимости иметь исходный код для программы.

Для проверки эффективности метода верификации на основе процессной семантики разработанный инструментарий был запущен на драйверах ядра Linux 2.6.32-5-686, которое является основой дистрибутива GNU/Linux Debian 6.0.6.

Верификатором было проанализировано 1224 стандартных драйвера ядра, для всех них была построена модель драйвера на языке АФС, а также получена процессная семантика драйвера в виде системы рекурсивных уравнений. Весь анализ занял 49 минут на компьютере с процессором Intel(R) Core(TM) i7-3630QM 2.4 с 8 вычислительными ядрами по 2.4 ГГц каждое, объем оперативной памяти - 6 Гб.

Корректность построенной системы рекурсивных уравнений была выборочно проверена для 300 построенных моделей драйверов.

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

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

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

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

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

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

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

19

ручной проверкой 300 построенных моделей драйверов. Данный анализ занял около 50 минут на персональном компьютере. Экспериментальные результаты доказывают применимость данного метода к драйверам ядра Linux.

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

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

7. Предложенный метод и разработанный инструментарий были успешно внедрены в производственный процесс ООО «Исследовательский центр Сам-сунг», ООО «Инсайт» и в учебный процесс Российского государственного социального университета в курс лекций «Специальные разделы теории языков программирования» для студентов специальностей 230105.65 (программное обеспечение вычислительной техники и автоматизированных систем) и 230100.68 (информатика и вычислительная техника); в курс лекций «Семантика языков программирования» для студентов специальности 230100.62 (информатика и вычислительная техника). С использованием разработанных инструментальных средств верификации драйверов операционной системы Linux поставлены лабораторные работы в курс «Операционные системы» для студентов указанных выше специальностей.

Публикации по теме диссертации

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

2. Кораблин Ю.П., Павлов Е.Г. Вопросы верификации драйверов Linux на осно-

20

ве процессной семантики // Ученые записки РГСУ. 2012. №7. С. 165-172.

3. Кораблин Ю.П., Павлов Е.Г. Разработка инструментов верификации для драйверов операционных систем // Современные проблемы информационной безопасности и программной инженерии: Сборник избранных статей научно-методологического семинара №3 кафедры информационной безопасности и программной инженерии (7 декабря 2011 г.). М.: Изд-во «Спутник+», 2012. С. 61-67.

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

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

6. Павлов Е.Г. Разработка инструментария для верификации драйверов операционной системы Linux на основе процессной семантики // Всероссийский конкурс научно-исследовательских работ студентов и аспирантов в области информатики и информационных технологий: Сб. науч. работ в 3 т. Белгород: ИД «Белгород», 2012. Т. 2. С. 325-329.

7. Павлов Е.Г. Актуальные проблемы в области разработки драйверов операционных систем // Современные проблемы информационной безопасности и программной инженерии: взгляд молодых: Сб. избранных статей научно-методологического семинара кафедры информационной безопасности и программной инженерии (8 октября 2011 года). М.: Изд-во «Спутник+», 2011. С. 81-87.

8. Павлов Е.Г. Разработка инструментов для обнаружения ошибок в драйверах Linux на основе семантического анализа // Проблемы информатизации жизненного пространства человека: Материалы 1 межвузовской научной конференции студентов, аспирантов и молодых преподавателей. М.: Изд-во РГСУ, 2012. С. 82-96.

Типография ШсгаЛ Подписано в печать 16.05.2013 г. Тираж 100 экз. Заказ № 297. г. Москва, ул. Цветной бульвар 32/4, оф. 3 Тел. (495) 785 92 72

РОССИЙСКИЙ ГОСУДАРСТВЕННЫЙ СОЦИАЛЬНЫЙ УНИВЕРСИТЕТ

На правах рукописи

04201357374

ПАВЛОВ ЕВГЕНИЙ ГЕННАДЬЕВИЧ

РАЗРАБОТКА И ПРИМЕНЕНИЕ МЕТОДА ВЕРИФИКАЦИИ ДРАЙВЕРОВ ОПЕРАЦИОННОЙ СИСТЕМЫ LINUX НА ОСНОВЕ ПРОЦЕССНОЙ

СЕМАНТИКИ

Специальность 05.13.11 - Математическое и программное обеспечение вычислительных

машин, комплексов и компьютерных сетей

Диссертация на соискание ученой степени кандидата технических наук

Научный руководитель д.т.н., проф. Кораблин Ю. П.

Москва-2013

Оглавление

Оглавление...................................................................................................................2

Введение.......................................................................................................................6

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

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

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

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

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

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

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

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

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

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

1.2.1 Static Driver Verifier...........................................................................................19

1.2.2 SLICx..................................................................................................................20

1.2.3 DDVerify............................................................................................................21

1.2.4 Linux Driver Verification....................................................................................21

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.3.3 Семафоры..........................................................................................................36

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Заключение...............................................................................................................124

Список литературы..................................................................................................126

Приложение А Исходный код транслятора из кода драйвера в программу на языке

АФС..........................................................................................................................141

Файл dsv.li.................................................................................................................141

Файл с^у.с.................................................................................................................143

Файл afs.li..................................................................................................................156

Файл а&.с..................................................................................................................158

Файл рагеег-с.І..........................................................................................................175

Файл рагеег-с.у..........................................................................................................177

Приложение Б Исходный код модуля преобразования программы на языке АФС в

систему рекурсивных уравнений............................................................................189

Файл parser.ii.............................................................................................................189

Файл рагеег.с.............................................................................................................191

Файл рагеег^БЛ........................................................................................................227

Файл рагеег.у.............................................................................................................229

Введение

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

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

На заре рождения операционных систем драйверы были написаны небольшой группой программистов, прекрасно знающих оборудование и систему. Конечно, операционные системы того времени были гораздо менее объемные по коду и, как правило, эти системы работали на стандартизированном оборудовании. Для сравнения, в современное ядро 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 наименований.

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

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

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

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

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

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

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

Операционная система является важнейшим компонентом современных информационных систем. Именно операционная система задает основные характе�