• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
ФИО студента
Название работы
Руководитель
Факультет
Программа
Оценка
Год защиты
Козин Святослав Владимирович
Программа статической верификации конфигураций ядра операционной системы Linux
2017
Данная работа посвящена процессу верификации ядра Linux с учетом вариабельности системы.

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

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

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

Наша основная цель - разработать продукт для поиска возможных дефектов(ошибок и не предусмотренных разработчиком поведений) в вариабельном ПО и предложить быстрое и безопасное решение для повышения безопасности систем на основе Linux.

Итоговая программа использует такие инструменты как: Undertaker, Z3, CPAchecker и имеет консольный интерфейс

Этот документ содержит 39 страниц, 3 главы, 10 иллюстраций, 31 источников, 4 приложения.

Ключевые слова: Линейки программных продуктов, Linux, Kconfig, Препроцессор

Выпускные квалификационные работы (ВКР) в НИУ ВШЭ выполняют все студенты в соответствии с университетским Положением и Правилами, определенными каждой образовательной программой.

Аннотации всех ВКР в обязательном порядке публикуются в свободном доступе на корпоративном портале НИУ ВШЭ.

Полный текст ВКР размещается в свободном доступе на портале НИУ ВШЭ только при наличии согласия студента – автора (правообладателя) работы либо, в случае выполнения работы коллективом студентов, при наличии согласия всех соавторов (правообладателей) работы. ВКР после размещения на портале НИУ ВШЭ приобретает статус электронной публикации.

ВКР являются объектами авторских прав, на их использование распространяются ограничения, предусмотренные законодательством Российской Федерации об интеллектуальной собственности.

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

Расширенный поиск ВКР