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

• Автор: Новиков, Евгений Михайлович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2013
• Место защиты: Москва
• Количество страниц: 284 с. : ил.

СОДЕРЖАНИЕ
Введение

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

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

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

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

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

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

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

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

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

1.3 Выводы
Глава 2. Метод контрактных спецификаций
2.1 Анализ правил корректного использования программного интерфейса сердцевины ядра ОС Linux
2.2 Подход аспектно-ориентированного программирования для языка Си
2.2.1 Основные понятия АОП
2.2.2 Традиционные способы описания аспектов
2.2.3 Влияние особенностей языка программирования Си и процесса сборки Си-программ на реализацию АОП
2.2.4 Особенности практического применения реализации АОП для языка Си
2.2.5 Существующие реализации АОП для языка Си
2.2.5.1 AspeCt-oriented С
2.2.5.2 InterAspect
2.2.5.3 Specification Language for Interface Checking
2.2.5.4 Другие реализации АОП для языка Си
2.2.6 Выводы
2.3 Метод описания в виде контрактных спецификаций правил корректного использования программного интерфейса сердцевины ядра ОС Linux
2.3.1 Шаг 1. Разработка модели подсистем ядра
2.3.2 Шаг 2. Описание множества точек использования элементов программного интерфейса
2.3.3 Шаг 3. Привязка модельных функций к точкам использования элементов программного интерфейса
2.3.4 Шаг 4. Задание предусловий использования элементов программного интерфейса
2.3.6 Дополнения к заданию контрактных спецификаций
2.4 Метод автоматизированного инструментирования исходного кода модулей ядра ОС Linux на основе контрактных спецификаций
2.5 К вопросу о доверии к контрактным спецификациям
2.5.1 Идеальные и избыточные контрактные спецификации
2.5.2 Примеры избыточных контрактных спецификаций
2.5.3 Чрезмерная избыточность контрактных спецификаций
2.5.4 Избыточность контрактных спецификаций на практике
2.5.5 Корреляции контрактных спецификаций
2.6 Подход к автоматизированному анализу структуры программы на основе

высокоуровневых запросов по исходному коду
2.6.1 Существующие решения
2.6.1.1 Запросы по исходному коду на основе регулярных выражений
2.6.1.2 Запросы по исходному коду на основе формального представления программы
2.6.2 Использование реализации АОП для выполнения запросов по исходному коду программ
2.6.2.1 Получение фактических параметров макрофункций
2.6.2.2 Получение списка вызываемых функций, у которых тип одного из параметров является указателем
2.6.2.3 Получение списка функций, в которых изменяется глобальная переменная
2.7 Метод автоматизированной поддержки корректности и соглаеовашюсти контрактных спецификаций в условиях изменения программного интерфейса
2.8 Подход к автоматизированному уточнению контрактных спецификаций в условиях неполноты модели окружения
2.9 Выводы
Глава 3. Реализация метода контрактных спецификаций
3.1 Aspect-Oriented С — аспестно-орииггированное расширение языка программирования Си с поддержкой всех расширений компилятора GCC
3.2 С Instrumentation Framework — аспектный компоновщик
3.2.1 Этап 1. Аспектное препроцессирование
3.2.2 Этап 2. Подготовка исходного кода
3.2.3 Этап 3. Инструментирование макросов
3.2.4 Этап 4. Инструментирование
3.2.5 Этап 5. Компиляция
3.3 База контрактных спецификаций
3.4 Место разработанного инструментария в системе верификации LDV
3.5 Выполнение высокоуровневых запросов по исходному коду
3.6 Контроль корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса
3.6.1 Обеспечение синтаксической корректности контрастных спецификаций
3.6.2 Проверка синтаксической совместимости контрактных спецификаций с программным интерфейсом сердцевины ядра ОС Linux
3.6.3 Обеспечение семантической корректности контрастных спецификаций
3.7 Уточнение контрактных спецификаций в условиях неполноты модели окружения
Глава 4. Практические результаты
Заключение
Список использованных источников
Приложение А Каталог наиболее критичных правил корректного использования
программного интерфейса сердцевины ядра ОС Linux
Приложение Б Аспектно-ориентированное расширите языка программирования Си с поддержкой всех расширений компилятора GCC

Введение
На сегодняшний день ядро операционной системы (ОС) 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]. Сердцевина ядра допускает динамическую
2.2 Подход аспектно-ориентированного программирования для языка

Аспектно-ориентированное программирование (АОП) возникло как ответ на вопрос о том, как «правильно» декомпозировать большую программу на модули. Одной из самых оригинальных и, вместе с тем, мощных идей о критериях декомпозиции была идея Д.Л. Парнаса выделять в отдельный модуль каждое проектное решение, особенно, если речь идет о сложных решениях, которые в будущем будут с высокой вероятностью пересматриваться [84]. Парнас показал, что традиционных средств обеспечения модульности часто достаточно, но иногда их явно не хватает - нужны дополнительные возможности. Среди отечественных специалистов примерло в то же время, в 70-х годах, этой же проблемой занимался A.J1. Фуксман, который говорил о необходимости ввести в практику программирования специальные конструкции для «сосредоточенного описания рассредоточенных действий» [85].
Распространенные в настоящее время языки программирования, как правило, не поддерживают такие конструкции. Например, те виды модулей, которые имеются в процедурных или в объектно-ориентированных языках, помогают декомпозировать программную систему по принципу группировки функционально связанных компонентов и/или данных. Но есть и другие способы декомпозиции, которые могут в большей степени зависеть не от структуры реализации основной функциональности, а от архитектурных решений, направленных, например, па выполнение технологических задач. Соответствующая подобным задачам «дополнительная» функциональность получила название сквозной функциональности (англ. cross-cutting concerns).
Описание сквозной функциональности приходится распределять по тексту программы, что запутывает его и приводит к разрастанию кода. Повышается вероятность появления ошибок в связи с некорректным внесением модификаций во фрагменты программной системы, связанные со сквозной