Алексей Хорошилов

Кандидат физико-математических наук (2006 г.), тема диссертации - «Спецификация и тестирование компонентов с асинхронным интерфейсом», руководитель А. К. Петренко. С 1999 года работает в Институте системного программирования РАН, на 2011 год — в должности старшего научного сотрудника. С 2009 года работает на кафедре Системного программирования факультета Вычислительной математики и кибернетики МГУ. Основные научные результаты: участие в создании технологии разработки тестов на основе формальных моделей UniTESK и поддерживающих ее инструментов, разработка унифицированной архитектуры тестового набора и правил построения расширений языков программирования для разработки тестов на основе контрактных спецификаций, разработка методов построения тестов для математических библиотек, разработка специализированной технологии быстрого создания тестов работоспособности.

Верификация операционных систем

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

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

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

Наиболее распространённым подходом к верификации программ является тестирование, то есть динамическая проверка корректности поведения целевой системы в ходе проведения тестового эксперимента. В случае функционального тестирования публичного интерфейса  ОС  целью эксперимента является проверка того, что наблюдаемое поведение компонентов, доступных через публичные интерфейсы ОС, соответствует декларируемому. Важным моментом для понимания этой задачи является количественная оценка состава интерфейсов ОС. На одной стороне спектра находятся специализированные ОС, предназначенные для работы на встраиваемых устройствах. Например, одна из таких ОС, с которой нам приходилось работать, включает поддержку порядка 700 функций и 80 команд. На другой стороне спектра находятся ОС общего назначения, которые как, например, Debian 7.0 для архитектуры x86, включают в себя более 10 тысяч утилит и более полутора тысяч библиотек, предоставляющих более 700 тысяч функций. Таким образом, задача тщательного функционального тестирования может ставиться только для специализированных ОС или для ключевых интерфейсов ОС общего назначения. Для широкомасштабного функционального тестирования ОС общего назначения приходится использовать методы, в большей степени ориентированные не на достижение высокого качества тестирования, а на обеспечение приемлемых временных и экономических показателей проектов.

Для решения задачи тщательного тестирования отдельных компонентов наш опыт показывает [1], что наиболее эффективным подходом является разработка тестов на основе моделей, в частности, при помощи технологии UniTESK [2], разработанной в ИСП РАН. Также часто для конкретного целевого компонента оказывается наиболее эффективной  разработка специализированной тестовой системы. Примером таких систем является набор для тестирования библиотек математических функций [3] и специализированная система тестирования драйверов файловых систем ОС Linux [4].

Примером подхода к решению задачи широкомасштабного тестирования является API Sanity Autotest [5], который позволяет полностью автоматически генерировать тесты работоспособности на основе заголовочных файлов библиотеки и дополнительной семантической информации об особенностях библиотеки, представленных в ней типах данных и специфики их использования в определённых функциях. Типичными примерами такой информации являются описания того:

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

В промежутке между тестированием работоспособности и тщательным тестированием находятся более-менее традиционные подходы к построению тестов. Поскольку часто оказывается, что целая группа тестов выполняет приблизительно одни и те же действия, отличающихся лишь в небольшом числе деталей, то естественным развитием традиционного подхода является та или иная форма шаблонов тестов, позволяющая минимизировать дублирование кода. Примером такого развития является технология автоматизированной разработки тестов T2C [6], с помощью которой был разработан набор тестов, проверяющий более 4000 требований стандарта Linux Standard Base (LSB).

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

Гонки по данным также являются важной проблемой для ядра ОС [7], поскольку ошибки этого вида очень сложно локализовать и тестировать. В ИСП РАН проводятся исследования сразу над несколькими подходами к обнаружению гонок как при помощи динамических методов KernelStrider [8] и RaceHound [9], так и при помощи статических [10].

Статическая верификация нацелена на выявление типовых ошибок в анализируемом коде посредством умозрительного рассмотрения всех возможных путей выполнения программы без её реального выполнения. В рамках проекта Linux Driver Verification (LDV) [11] в ИСП РАН разрабатывается набор инструментов, реализующих тяжеловесные методы статической верификации, основанные на подходе CEGAR (Counter-Example Guided Abstraction Refinement) [12]. Отличие этого подхода от распространённых инструментов статического анализа (Coverity, Klockwork, SVACE, Smatch, Sparse, Coccinelle) заключается в том, что они позволяют не только найти типовые ошибки, но и доказать их отсутствие. Расплатой за это является то, что тяжеловесные методы требуют на один-два порядка больше времени и памяти. В рамках проекта LDV основной целью является выявление некорректного использования интерфейсов ядра в модулях ядра ОС Linux. Несмотря на наличие большого количества направлений для дальнейшего развития, инструменты LDV уже готовы к применению на практике, что подтверждается тем фактом, что они позволили найти и исправить уже более 180 ошибок в ядре ОС Linux [13].

Если тестирование демонстрирует корректность целевой системы только на определённых тестовых данных и при определённых обстоятельствах, а статическая верификация нацелена только на доказательство отсутствия ошибок определённого вида, то методы дедуктивной верификации позволяют доказать полную корректность целевой системы её функциональным спецификациям, хотя и при определённых предположениях, например, о корректности работы компилятора или о корректности модели внешних сервисов или аппаратуры. Неудивительно, что дедуктивная верификация крайне трудоёмка и применяется только для очень важных компонентов ОС. Интересным опытом ИСП РАН в этом направлении является проект по дедуктивной верификации модуля, реализующего механизм управления доступом в ОС Astra Linux Special Edition.

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

Литература

• Н.В.Пакулин, А.В.Хорошилов. Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов. Программирование, №6, 2007, C.26-55.
• А.В. Баранцев, И.Б. Бурдонов, А.В. Демаков, С.В. Зеленов, А.С. Косачев, В.В. Кулямин, В.А. Омельченко, Н.В. Пакулин, А.К. Петренко, А.В. Хорошилов. “Подход UniTesK к разработке тестов: достижения и перспективы”. Труды Института системного программирования РАН, №5, 2004. C.121-156.
• Kuliamin. Standardization and Testing of Mathematical Functions. // Proc. of PSI’2009, Novosibirsk, Russia, June 2009, LNCS 5947. pp. 257-268, Springer, 2009.
• Проект по верификации модулей драйверов файловых систем.  http://linuxtesting.org/spruce.
• А.В. Пономаренко, В.В. Рубанов, А.В. Хорошилов. Автоматическая генерация тестов для C/C++ библиотек. Сборник докладов Седьмой конференции разработчиков свободных программ, Переславль, 26-27 июля 2010 г.
• Alexey Khoroshilov, Vladimir Rubanov, Eugene Shatokhin. «Automated Formal Testing of C API Using T2C Framework». In Proceedings of the Third International Symposium «Leveraging Applications of Formal Methods, Verification and Validation» (ISoLA 2008), Porto Sani, Greece, October 13-15, 2008. pp.56-70. ISBN 978-3-540-88478-1.
• В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов. “Анализ типовых ошибок в драйверах операционной системы Linux”. Труды Института Системного Программирования, Том 22, 2012, с. 349-374.
• Сайт проекта Kernel Strider. https://code.google.com/p/kernel-strider/.
• Сайт проекта Race Hound. http://forge.ispras.ru/projects/race-hound.
• Павел Андрианов, Алексей Хорошилов, Вадим Мутилин "Lightweight Static Analysis for Data Race Detection in Operating System Kernel". Материалы международной научно-практической конференции Инструменты и Методы Анализа Программ(TMPA-2014), с.128-135, 14-15 ноября 2014, Кострома, Россия.
• И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. “Конфигурируемая система статической верификации модулей ядра операционных систем”. Труды Института Системного Программирования, Том 26-2, 2014, с. 5-42.
• М.У. Мандрыкин, В.С. Мутилин, А.В. Хорошилов. “Введение в метод CEGAR — уточнение абстракции по контрпримерам”. Труды Института Системного Программирования, Том 24, 2013, с. 219-292.
• Список ошибок, обнаруженный при помощи LDV. http://linuxtesting.org/results/ldv.