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

005534151

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

Новиков Евгении Михайлович

РАЗВИТИЕ МЕТОДА КОНТРАКТНЫХ СПЕЦИФИКАЦИЙ ДЛЯ ВЕРИФИКАЦИИ МОДУЛЕЙ ЯДРА ОПЕРАЦИОННОЙ СИСТЕМЫ LINUX

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

Автореферат

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

3 ОКТ 2013

Москва 2013

005534151

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

Научный руководитель: доктор физико-математических наук, профессор

Петренко Александр Константинович

Официальные оппоненты: Горбунов-Посадов Михаил Михайлович, доктор

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

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

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

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

учреждение науки Научно-исследовательский институт системных исследований Российской академии наук

Защита диссертации состоится 31 октября 2013 г. в 16:00 на заседании диссертационного совета Д 002.087.01 при Федеральном государственном бюджетном учреждении науки Институте системного программирования Российской академии наук по адресу: 109004, Москва, ул. Александра Солженицына, д. 25, конференц-зал (комната 110).

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

Автореферат разослан 26 сентября 2013 г.

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

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

Общая характеристика работы

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

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

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

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

Исследования показали, что более 85% ошибок в ядре ОС Linux сосредоточены в модулях. Это обусловлено тем, что, во-первых, модули составляют большую часть всего ядра. Во-вторых, сердцевина ядра активно используется разными модулями, а потому ошибки в ней выявляются достаточно быстро. Кроме того, разработчики модулей ядра ОС Linux, как правило, не являются экспертами в устройстве ядра.

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

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

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

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

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

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

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

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

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

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

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

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

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

1) описание в виде спецификаций всех правил из составленного каталога;

2) применение различных инструментов верификации для автоматизированной проверки модулей ядра ОС Linux на предмет выполнения требований спецификаций;

3) автоматизацию контроля корректности и согласованности спецификаций в условиях изменения программного интерфейса.

г) Разработать инструментарий, реализующий предлагаемый метод.

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

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

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

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

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

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

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

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

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

Разработанные контрактные спецификации и инструментарий были использованы в процессе подготовки эталонного набора задач достижимости для измерения сравнительных характеристик инструментов верификации. Данный набор используется в рамках ежегодных мероприятий ETAPS/Competition on Software Verification. В будущем планируется обновлять данный набор на основе результатов верификации модулей новых версий ядра ОС Linux.

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

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

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

- Научно-практическая конференция «Актуальные проблемы программной инженерии» (г. Москва, 2009 г.);

- 52-я научная конференция МФТИ «Современные проблемы фундаментальных и прикладных наук» (г. Долгопрудный, 2009 г.);

- 5-й весенний/летний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE, г. Екатеринбург, 2011 г.);

- 6-я летняя школа Microsoft Research (г. Кембридж, Великобритания, 2011 г.);

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

- 2-й международный семинар Linux Driver Verification в рамках 5-го международного симпозиума по внедрению формальных методов, верификации и валидации (LDV Workshop, ISoLA, г. Ираклион, о. Крит, Греция, 2012 г.);

- семинар ИСП РАН (г. Москва, 2012 г.);

- Европейская конференция по программной инженерии, совмещенная с Симпозиумом по основам программной инженерии ACM SIGSOFT (ESEC/FSE, г. Санкт-Петербург, 2013 г.).

По теме диссертации автором опубликовано 15 работ и получено 2 свидетельства о государственной регистрации программы для ЭВМ. Полный список работ приведен в конце автореферата. Первые 7 из них опубликованы в изданиях из перечня ВАК.

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

Диссертация состоит из введения, 4 глав, заключения, списка литературы (132 наименования) и 2 приложений. Основной текст диссертации (без приложений и списка литературы) занимает 123 страницы.

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

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

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

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

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

- список выявленных нарушений;

- описание релевантных элементов программного интерфейса сердцевины ядра ОС Linux;

- неформальные формулировки правил.

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

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

-аспектная компоновка — процесс связывания аспектов с целевой программой;

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

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

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

- они не учитывают особенности языка программирования Си и процесса сборки Си-программ;

- предоставляемые средства являются недостаточно выразительными для

задания спецификаций многих правил корректного использования программного интерфейса сердцевины ядра ОС Linux;

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

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

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

Далее рассматриваются шаги предлагаемого метода.

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

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

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

Шаг 4. Задание предусловий использования элементов программного интерфейса на основании тех требований, которые накладывают правила

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

Шаг 5. Объединение частей контрактной спецификации, полученных на шагах с первого по четвертый, и модели обработчиков событий в итоговую контрактную спецификацию, которая представляется в виде аспекта.

Контрактные спецификации для правил корректного использования программного интерфейса сердцевины ядра ОС Linux приведены в приложении А для каждого вида правил из представленного там каталога.

Для демонстрации места контрактных спецификаций в ядре ОС Linux представлены схема обработки событий в ядре ОС Linux (рисунок 1) и схема контрактных спецификаций (рисунок 2).

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

События

1» __■-.,,..■ _-_ г _

Пользовательские приложения Аппаратное обеспечение \ Ядро ОС Linux Е '['

\ \1 / \ / \ / \ Сердцевина л о I >s 5 ш 1 -а Модули !..........-..........я.....................

! 1 а. ш н о X О. S С

Рисунок 1. Схема обработки событий в ядре ОС Linux.

Модель обработчиков событий

Модули

ГС

Модель ш

элементов «л 5

программного < £

интерфейса ш О.

1=

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

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

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

Аспектный компоновщик

ГП=-----

Инструментированный >- код модулей (задача достижимости)

Unsafe 4

Инструменты /^Safe

верификации

\

ч

Unknown

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

По результатам решения данной задачи инструменты верификации могут вынести один из трех вердиктов:

- Safe - в анализируемом модуле нет ошибок искомого вида;

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

- Unknown - инструмент не смог решить поставленную задачу достижимости (например, из-за нехватки отведенного на решение времени).

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

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

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

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

Стабилизация

Ядро ОС Linux

Запросы для извлечения функций-обработчиков

Доработка

Контрактные спецификации

Модель обработчиков событий

к

Модель m

элементов ц

программного =t

интерфейса ф о.

С

Запросы для извлечения элементов программного интерфейса

7

Контроль корректности и согласованности

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

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

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

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

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

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

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

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

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

- уникальный идентификатор;

- набор файлов, в том числе с аспектом;

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

В четвертой части показано место разработанного инструментария в системе верификации Linux Driver Verification. Показывается, каким образом в

системе верификации используется аспектный компоновщик и какие данные ему подаются на вход. Затем рассматриваются инструменты, которые используют новую реализацию АОП. Данные инструменты реализуют:

- подход к автоматизированному анализу структуры программ на основе высокоуровневых запросов по исходному коду;

- метод автоматизированной поддержки корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса (рисунок 4);

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

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

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

Приводятся результаты, которые были получены в рамках практического применения разработанного инструментария в составе системы верификации, разработанной в рамках проекта Linux Driver Verification. В среднем для ядра версий от 2.6.31.6 и до 3.11-rcl был успешно инструментирован исходный код более 95% модулей (всего их порядка 2 — 4 Тыс. в зависимости от версии ядра). Инструментированный код был успешно проверен с помощью нескольких инструментов верификации: BLAST, CPAchecker, UFO и CBMC.

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

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

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

В последней части показывается, как разработанные контрактные спецификации и инструментарий были использованы в процессе подготовки эталонного набора задач достижимости для измерения сравнительных характеристик инструментов верификации. Показывается, что поскольку данный набор используется в рамках ежегодных мероприятий ETAPS/Competition on Software Verification, то все инструменты верификации, которые участвуют в этих мероприятиях, потенциально могут быть использованы для проверки модулей ядра ОС Linux на предмет выполнения требований контрактных спецификаций автоматизированным образом.

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

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

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

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

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

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

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

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

1 Новиков Е.М. Подход к реализации аспекТно-ориентированного программирования для языка Си // Программирование. 2013. №4. С. 47-65.

2 Новиков Е.М. Построение спецификаций программных интерфейсов в

открытой системе покомпонентной верификации ядра Linux // Труды Института системного программирования РАН. 2013. Т. 24. С. 293-316.

3 Новиков Б.М., Хорошилов A.B. Использование аспектно-ориентированного программирования для выполнения запросов по исходному коду программ // Труды Института системного программирования РАН. 2012. Т. 23. С. 371-386.

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

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

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

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

8 Новиков Е.М. Использование аспектно-ориентированного подхода программирования в процессе верификации ядра операционной системы Linux // Сборник научных трудов Научно-практической конференции «Актуальные проблемы программной инженерии». Москва, 2009. С. 148-154.

9 Мутилин B.C., Новиков Е.М., Хорошилов A.B. Классификация концепций для аспектно-ориентированного расширения языка программирования С // Труды 52-й научной конференции МФТИ «Современные проблемы фундаментальных и прикладных наук», часть 7 «Управление и прикладная математика». Долгопрудный, 2009. Т. 2. С. 31-33.

10 Новиков Е.М., Хорошилов A.B. Реализация аспектно-

ориентированного программирования для языка Си // Тезисы докладов восьмой конференции разработчиков свободных программ. Обнинск, 2011. С. 23-26.

11 Щепетков И.В., Новиков Е.М. Диагностика синтаксической совместимости правил корректности с ядром ОС Linux при статической верификации драйверов // Сборник научных трудов Научно-практической конференции «Актуальные проблемы системной и программной инженерии». Москва, 2013. С. 192-201.

12 Novikov Е. One Approach to Aspect-Oriented Programming Implementation for the С programming language // Proceedings of the 5th Spring/Summer Young Researchers' Colloquium on Software Engineering. Yekaterinburg. 2011. Pp. 74-81.

13 Khoroshilov A., Mutilin V, Novikov E., Shved P, Strakh A. Towards an open framework for С verification tools benchmarking // Perspectives of Systems Informatics, Lecture Notes in Computer Science. 2012. V. 7162. Pp. 179-192.

14 Zakharov I., Mutilin V., Novikov E., Khoroshilov A. Generating Environment Model for Linux Device Drivers // Proceedings of the 7th Spring/Summer Young Researchers' Colloquium on Software Engineering. Kazan. 2013. Pp. 77-83.

15 Beyer D., L6we S., Novikov E., Stahlbauer A., Wendler P. Precision Reuse for Efficient Regression Verification // Proceedings of the 9th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering. 2013. Pp. 389-399.

16 Новиков Е.М. Свидетельство о государственной регистрации программы для ЭВМ №2012615598 от 20.06.2012 «Система аспектно-ориентированного программирования для языка Си».

17 Мандрыкин М.У, Мутилин B.C., Новиков Е.М., Хорошилов А.В., Швед П.Е. Свидетельство о государственной регистрации программы для ЭВМ №2012615596 от 20.06.2012 «Система проверки выполнения проблемно-ориентированных правил для Си программ».

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

17.09.2013

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

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

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

04201363554

Новиков Евгений Михайлович

РАЗВИТИЕ МЕТОДА КОНТРАКТНЫХ СПЕЦИФИКАЦИЙ ДЛЯ ВЕРИФИКАЦИИ МОДУЛЕЙ ЯДРА ОПЕРАЦИОННОЙ СИСТЕМЫ LINUX

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

Диссертация

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

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

профессор, д. ф.-м. н.

Петренко Александр Константинович

Москва 2013

СОДЕРЖАНИЕ

Введение..............................................................................................................................................4

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

1.1 Неформальные методы контрактных спецификаций.........................................................18

1.2 Формальные методы контрактных спецификаций.............................................................19

1.2.1 Контрактные спецификации для компиляторов и интерпретаторов.........................20

1.2.2 Контрактные спецификации при динамическом анализе..........................................21

1.2.3 Контрактные спецификации при статическом анализе..............................................23

1.2.4 Контрактные спецификации при верификации...........................................................24

1.2.4.1 Модель окружения для модулей ядра ОС Linux..................................................26

1.2.4.2 Спецификации правил корректного использования программных интерфейсов ..............................................................................................................................................29

1.3 Выводы....................................................................................................................................32

Глава 2. Метод контрактных спецификаций..................................................................................33

2.1 Анализ правил корректного использования программного интерфейса сердцевины ядра ОС Linux.......................................................................................................................................33

2.2 Подход аспектно-ориентированного программирования для языка Си...........................35

2.2.1 Основные понятия АОП................................................................................................36

2.2.2 Традиционные способы описания аспектов................................................................39

2.2.3 Влияние особенностей языка программирования Си и процесса сборки Си-программ на реализацию АОП..............................................................................................44

2.2.4 Особенности практического применения реализации АОП для языка Си...............46

2.2.5 Существующие реализации АОП для языка Си.........................................................47

2.2.5.1 AspeCt-oriented С....................................................................................................47

2.2.5.2 InterAspect...............................................................................................................49

2.2.5.3 Specification Language for Interface Checking.......................................................50

2.2.5.4 Другие реализации АОП для языка Си................................................................52

2.2.6 Выводы............................................................................................................................52

2.3 Метод описания в виде контрактных спецификаций правил корректного использования программного интерфейса сердцевины ядра ОС Linux...........................................................53

2.3.1 Шаг 1. Разработка модели подсистем ядра..................................................................54

2.3.2 Шаг 2. Описание множества точек использования элементов программного интерфейса...............................................................................................................................56

2.3.3 Шаг 3. Привязка модельных функций к точкам использования элементов программного интерфейса.....................................................................................................57

2.3.4 Шаг 4. Задание предусловий использования элементов программного интерфейса

...................................................................................................................................................59

2.3.6 Дополнения к заданию контрактных спецификаций..................................................63

2.4 Метод автоматизированного инструментирования исходного кода модулей ядра ОС Linux на основе контрактных спецификаций............................................................................63

2.5 К вопросу о доверии к контрактным спецификациям........................................................65

2.5.1 Идеальные и избыточные контрактные спецификации.............................................66

2.5.2 Примеры избыточных контрактных спецификаций...................................................68

2.5.3 Чрезмерная избыточность контрактных спецификаций............................................69

2.5.4 Избыточность контрактных спецификаций на практике...........................................70

2.5.5 Корреляции контрактных спецификаций....................................................................71

2.6 Подход к автоматизированному анализу структуры программы на основе

высокоуровневых запросов по исходному коду........................................................................72

2.6.1 Существующие решения...............................................................................................74

2.6.1.1 Запросы по исходному коду на основе регулярных выражений........................74

2.6.1.2 Запросы по исходному коду на основе формального представления программы...........................................................................................................................74

2.6.2 Использование реализации АОП для выполнения запросов по исходному коду программ..................................................................................................................................77

2.6.2.1 Получение фактических параметров макрофункций..........................................78

2.6.2.2 Получение списка вызываемых функций, у которых тип одного из параметров является указателем............................................................................................................80

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

2.7 Метод автоматизированной поддержки корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса..........................................82

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

2.9 Выводы....................................................................................................................................99

Глава 3. Реализация метода контрактных спецификаций...........................................................101

3.1 Aspect-Oriented С — аспектно-ориенгированное расширение языка программирования Си с поддержкой всех расширений компилятора GCC..........................................................101

3.2 С Instrumentation Framework — аспектный компоновщик..............................................102

3.2.1 Этап 1. Аспектное препроцессирование....................................................................105

3.2.2 Этап 2. Подготовка исходного кода............................................................................105

3.2.3 Этап 3. Инструментирование макросов.....................................................................106

3.2.4 Этап 4. Инструментирование......................................................................................106

3.2.5 Этап 5. Компиляция.....................................................................................................107

3.3 База контрактных спецификаций.....................................................................................108

3.4 Место разработанного инструментария в системе верификации LDV..........................110

3.5 Выполнение высокоуровневых запросов по исходному коду..........................................111

3.6 Контроль корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса.....................................................................................112

3.6.1 Обеспечение синтаксической корректности контрактных спецификаций.............112

3.6.2 Проверка синтаксической совместимости контрактных спецификаций с программным интерфейсом сердцевины ядра ОС Linux..................................................112

3.6.3 Обеспечение семантической корректности контрактных спецификаций..............ИЗ

3.7 Уточнение контрактных спецификаций в условиях неполноты модели окружения.....115

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

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

Список использованных источников............................................................................................124

Приложение А Каталог наиболее критичных правил корректного использования

программного интерфейса сердцевины ядра ОС Linux..............................................................138

Приложение Б Аспектно-ориентированное расширение языка программирования Си с поддержкой всех расширений компилятора GCC.......................................................................255

Введение

На сегодняшний день ядро операционной системы (ОС) Linux представляет собой одну из самых востребованных программных систем. Ядро ОС Linux используется повсеместно на большом количестве различных аппаратных платформ, начиная от встроенных систем и персональных компьютеров и заканчивая интернет-серверами и суперкомпьютерами [1-4]. За последние несколько лет популярность ядра ОС Linux значительно возросла за счет использования ядра в ОС для мобильных устройств (Android, Tizen, Firefox OS и др.).

Ядро ОС Linux является одной из самых больших и динамично развивающихся программных систем. Разработку ядра начал Линус Торвальдс в 1991 году [5]. Размер первой версии ядра ОС Linux 0.01 был около 10 тыс. строк кода. 17 декабря 2003 года было выпущено ядро версии 2.6.0, размер которого составил около 6 млн строк кода. Последняя на момент начала написания данной работы, стабильная версия ядра ОС Linux 3.8 была выпущена 18 февраля 2013 года. Ее размер составил более 16 млн строк кода. Менее, чем за десять лет, размер исходного кода ядра ОС Linux вырос более, чем в 2,5 раза. Процесс разработки ядра ОС Linux обладает уникальными особенностями. Начиная с версии ядра 2.6.24, выпущенной 24 января 2008 года, в подготовке всех новых версий ядра принимают участие более 1 000 разработчиков из 200 организаций, рассредоточенных по всему миру [6]. Каждая новая версия ядра ОС Linux включает около 9-12 тыс. изменений, что соответствует в среднем 5,4 изменениям в час.

По своей архитектуре ядро ОС Linux является монолитным. Сердцевина ядра состоит из подсистем управления процессами, памятью, и межпроцессорным взаимодействием, подсистем поддержки различных аппаратных платформ и т.д. [7, 8]. Сердцевина ядра допускает динамическую

загрузку модулей, что позволяет расширить набор ее функций [8, 9]. Схематично устройство ядра приведено на рисунке 1. В настоящее время в состав ядра ОС Linux входит более 3,7 тыс. модулей, из которых большая часть является драйверами устройств (около 75%). Помимо драйверов устройств к числу модулей ядра ОС Linux относятся реализации различных файловых систем, сетевых протоколов, аудиокодеков и т.д.

В рамках данной работы было проведено дополнительное исследование, которое показало, что для первого релиз-кандидата ядра версии 3.9 в конфигурации allmodconfig на аппаратной платформе х86_64 сердцевина состоит из 1 651 файла (написанных на языках программирования Си и ассемблер), которые содержат 1 054 022 строк кода. На модули приходится 8 918 Си-файлов, которые содержат 7 862 862 строк кода. Таким образом, всего из 10 569 файлов около 16% приходится на сердцевину и 84% — на модули, а из 8 916 884 строк кода — 12% на сердцевину и 88% на модули. Остальной код ядра

х

3

с

О О

о а И

в;

Сердцевина

Рисунок 1. Схема устройства ядра ОС Linux.

либо относится к другим архитектурам и/или конфигурациям, либо представляет собой заголовочные файлы. Всего в первый релиз-кандидат ядра версии 3.9 вошло 22 061 заголовочный файл, размер которых составил 2 958 407 строк кода.

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

Ядро ОС Linux является свободным программным обеспечением. Одним из достоинств этого является то, что доступ к его коду имеют большое количество разработчиков и огромное количество пользователей основанных на нем ОС. Это создает так называемый эффект многих глаз — большое количество ошибок обнаруживается и исправляется за достаточно короткое время [10]. Таким образом могут быть обнаружены не все ошибки, так как во всем мире достаточным уровнем знания во всех особенностях устройства ядра обладают небольшое количество людей, а ядро имеет достаточно большой размер и развивается высокими темпами [11].

Исследования показали, что более 85% ошибок в исходном коде ядра ОС

Linux сосредоточены в модулях1 [12-14]. Это обусловлено тем, что, во-первых,

модули составляют большую часть всего ядра. Во-вторых, сердцевина ядра

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

достаточно быстро. Кроме того, разработчики модулей ядра ОС Linux, как

правило, не являются экспертами в устройстве ядра. Например, большинство

драйверов устройств разрабатывается производителями соответствующего

аппаратного обеспечения. Подобное исследование для ядра ОС Microsoft

Windows ХР также показало, что наибольшее количество ошибок в ядре данной

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

ОС находятся в драйверах устройств [15].

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

Взаимодействие сердцевины ядра ОС Linux и модулей осуществляется следующим образом (рисунок 2):

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

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

2 Если не оговорено иное, то здесь и далее под программным интерфейсом сердцевины ядра понимается программный интерфейс только подсистем ядра без обработчиков событий.

Ext/

File Sys

MPEG

x с

реализация описание

A____L

API модулей (функции-обработчики)

О

?! а лз I

К s и ш

I

ш О

возврат

значении

ZÖE

_ вызовы

Обработчики событий

возврат значений

API сердцевины (подсистем ядра)

описание реализация

Подсистемы ядра

реализация описание

_А_____1_

API сердцевины (обработчиков событий) м-

«

системные возврат J/0 прерывания, вызовы,... зрачени^ ... порты, ... ...

Аппаратное еспечение

GNOME Пользовательские приложения

HübreOffice

Рисунок 2. Обработка событий в ядре ОС Linux (программный интерфейс для краткости называется API).

Как правило, программный интерфейс сердцевины ядра ОС Linux включает в себя следующие элементы3. Прототипы функций — наиболее часто используемые элементы программного интерфейса. Реализация этих функций находится в подсистемах ядра, static inline функции — функции с реализацией. Обычно такие функции небольшие по объему, и зачастую в телах этих функций вызываются функции, которые определены в подсистемах ядра. Макросы — в основном используются макрофункции. Если не оговорено иное, то в рамках данной работы считается, что макроподстановки аналогичны вызовам static inline функций (у параметров макрофункций и их возвращаемых значений нет типов). Другие возможности по использованию макросов в работе не рассматриваются. Декларации составных типов данных4 — в основном используются структуры, которые задают соглашение об организации данных, в том числе представлении функций-обработчиков, между сердцевиной и модулями.

Анализ изменений в модулях стабильных версий ядра за год разработки с 26.10.10 по 26.10.11 показал, что нарушения правил корректного использования программного интерфейса сердцевины ядра ОС Linux в модулях являются источником 15% от числа всех ошибок, или 50% от числа ошибок, которые не связаны с нарушениями спецификаций аппаратного обеспечения, сетевых протоколов, аудиокодеков и т.п.5 [18].

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

- для обнаружения 170 видов нарушений правил корректного

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

4 Под составными типами данных языка Си в данной работе понимаются структуры, объединения и перечисления.

5 Стоит отметить, что данные спецификации зачастую невозможно получить в полном виде.

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

- всего для модулей ядра требуется проверять порядка 2000 видов правил, из которых 600 позволяют обнаружить примерно 60% всех нарушений.

Программный интерфейс сердцевины ядра ОС Linux не является стабильным, что в частности подтверждается заявлением Грега Кроа-Хартмана, одного из ведущих разработчи�