28.06.2018: Центр верификации Linux на семинаре Sound Static Analysis for Security

Опубликовано admin в ЧТ, 28/06/2018 - 22:26

27-28 июня 2018 года на площадке Национального института по стандартизации и технологиям (National Institute of Standards and Technology, NIST) в г.Гейтерсберг (шт. Мэриленд), США, состоялся международный семинар, посвященный применению консервативного статического анализа для обеспечения безопасности программных систем (Sound Static Analysis for Security). В рамках семинара обсуждалась задача снижения количества уязвимостей в программных системах и как современные достижения в области консервативного статического анализа могут способствовать её решению. Поясним, что консервативным называют статический анализ, который не допускает пропуска ошибок искомого вида, при условии выполнения четко сформулированного набора допущений.

Работа семинара была разбита на три секции:

  • Анализ ранее разработанного кода.
  • Применение формальных методов при разработке новых систем.
  • Контроль за качеством программного обеспечения.

Работы Центра верификации ОС Linux были представлены в первой секции в докладе Алексея Хорошилова Proving sequential properties of unmodified Linux kernel code. В ходе выступления были представлены результаты по применению методов дедуктивной верификации к компонентам ядра ОС Linux, а также описаны проблемы верификации ранее разработанного низкоуровнего кода, которые привели к необходимости разработки новых инструментов верификации. В качестве целевых компонентов для верификации выступали реализация специализированного модуля управления доступом, разработанного для операционной системы специального назначения Astra Linux Special Edition, а также множество библиотечных функций ядра Linux, реализующих базовые операции с памятью и строками.

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