Моделирование окружения драйверов операционной системы Linux для их статической верификации

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

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

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

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

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

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