Верификация кода большого объема

Верификация модулей ядра ОС Linux предполагает работу с большим объемом кода. Для преодоления ограничений набора инструментов AstraVer в рамках проекта «Разработка методов и инструментов для дедуктивной верификации модулей ядра операционной системы Linux» (2014-2016) был разработан набор вспомогательных утилит.

Страница утилит: https://forge.ispras.ru/projects/astraver-utils

Установка внешних зависимостей утилит осуществляется следующим образом:

cpan cpanm
cpanm --installdeps .

Для удобства работы с программами рекомендуется задать переменные окружения:

Краткое описание функциональности утилит

Каждая из утилит имеет собственную документацию, которая доступна по ключу --help. Ниже представлено краткое описание функциональности и предназначения программ. Программы разбиты на две группы: первая группа используется для трансформации, вторая - для анализа исходного кода.

Трансформация исходного кода

Анализ исходного кода

Данные утилиты предназначены для изучения исходного кода и интерфейсов его взаимодействия с ядром.