Методы модульной верификации ядра ОС Linux

Илья Захаров. Начало семинара - 7 мая 2014 г.

Система верификации LDV нацелена на проверку правил корректности использования интерфейсов ядра Linux динамически загружаемыми модулями при помощи инструментов статической верификации. Одновременно анализировать исходный код модуля вместе с кодом остального ядра затруднительно для существующих инструментов верификации из-за большого объема и сложности кода такой системы. Поэтому в системе LDV для целевого модуля генерируется модель окружения, вместе с которой исходный код проверяется инструментами верификации. На текущий момент в системе LDV возможно построение модели окружения для каждого отдельного модуля, но такая модель включает только взаимодействие модуля и сердцевины ядра. В данном докладе будет рассмотрена проблема моделирования взаимодействия модулей между собой и будет предложен метод ее решения в рамках системы LDV.

С презентацией доклада можно ознакомиться здесь.

Семинар группы

Технологии программирования

Перейти к списку семинаров ИСП РАН