Программа статической верификации конфигураций ядра операционной системы Linux

Данная работа посвящена процессу верификации ядра Linux с учетом вариабельности системы. Ядро Linux часто используется в качестве яркого реального примера, чтобы продемонстрировать механизм вариабельности линейки программных продуктов. Чтобы обеспечить наиболее безопасное создание вариантов линейки продуктов Linux, необходимо проанализировать файл конфигураций, а также исходный код. Десятки тысяч конфигурационных переменных, выражений - это огромное число даже по стандартам современной разработки программного обеспечения. Исследователи в области верификации предложили множество решений этой проблемы. Стандартные процедуры проверки кода здесь неприемлемы из-за охвата всех конфигураций, поэтому было предложено проверить операционную систему со специальной программой основанной на инструментах, анализирующих построенный код и файл конфигурации. Такая программа способна быть эффективным инструментом для расчета допустимых конфигураций для предопределенного набора кода и Kconfig файла. Этот инструмент может быть использован для улучшения существующих инструментов анализа, а также выбора правильной конфигурации. Наша основная цель - разработать продукт для поиска возможных дефектов(ошибок и не предусмотренных разработчиком поведений) в вариабельном ПО и предложить быстрое и безопасное решение для повышения безопасности систем на основе Linux. Итоговая программа использует такие инструменты как: Undertaker, Z3, CPAchecker и имеет консольный интерфейс Этот документ содержит 39 страниц, 3 главы, 10 иллюстраций, 31 источников, 4 приложения. Ключевые слова: Линейки программных продуктов, Linux, Kconfig, Препроцессор