24.06.2014: Команда LDV представила доклад на международной конференции PSI'2014

Член команды LDV, Илья Захаров, представил доклад “Modeling Environment for Static Verification of Linux Kernel Modules” на 9-ой международной Ершовской конференции по информатике. В докладе представлены результаты совместных иссследований с Алексеем Хорошиловым, Вадимом Мутилиным и Евгением Новиковым, посвященных моделированию окружения модулей ядра ОС Linux с целью статической верификации, используя современные инструменты верификации программного обеспечения на основе проверки моделей.

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

Детальное описание метода можно найти в статье [Khoroshilov A., Mutilin V., Novikov., Zakharov I. Modeling Environment for Static Verification of Linux Kernel Modules. Proceedings of PSI, pp. 116-125, 2014.]