Сборники трудов ИСП РАН


Статическая верификация конфигураций ядра Linux

С.В. Козин (ВШЭ, Москва, Россия)
В.С. Мутилин (ИСП РАН, Москва, Россия)

Аннотация

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

Ключевые слова

линейка программных продуктов, Linux, Kconfig, препроцессор

Издание

Труды Института системного программирования РАН, том 29, вып. 4, 2017, стр. 217-230.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(4)-14

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома