Институт системного программирования Роcсийской академии наук


LDV. Технология статической верификации драйверов ядра ОС Linux

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

Конфигурируемая система статической верификации драйверов ядра ОС Linux LDV KLEVER позволяет автоматизированным образом подготовить исходный код драйверов к верификации на основе спецификаций модели ядра и проверить его на соответствие спецификациям правил корректности с помощью инструментов статической верификации.

LDV KLEVER включает спецификации моделей 20 наиболее широко используемых интерфейсов драйверов, таких как обработчики прерываний и таймеры, интерфейсы USB и PCI устройств, интерфейсы сетевых и символьных устройств.

LDV KLEVER включает 34 спецификации правил корректного использования программного интерфейса ядра ОС Linux, которые в том числе позволяют обнаружить следующие ошибки:

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

Помимо этого конфигурируемая система статической верификации драйверов ядра ОС Linux позволяет выявлять и другие ошибки, например:

  • выход за границу буфера,
  • разыменование нулевого указателя,
  • использование неинициализированной памяти,
  • утечка памяти,
  • повторное или некорректное освобождение памяти.

В настоящее время LDV KLEVER использует такие инструменты статической верификации, как CPAchecker, BLAST и CBMC.

По результатам верификации LDV KLEVER выносит вердикт для каждой пары драйвер-правило:

  • Safe – доказано выполнение правила корректности,
  • Unsafe – обнаружено нарушение правила корректности,
  • Unknown – правило корректности проверить не удалось.

В случае вердикта Unsafe LDV KLEVER предоставляет пользователю интерактивную трассу ошибки, описывающую полный аннотированный путь выполнения в исходном коде драйвера, который приводит к ошибке, с конкретными значениями всех переменных.

Процесс верификации

LDV. Технология статической верификации драйверов ядра ОС Linux

Для запуска и анализа результатов верификации LDV KLEVER предоставляет веб-интерфейс.

С помощью LDV KLEVER в драйверах ядра ОС Linux было выявлено более 250 ошибок, которые были признаны разработчиками (http://linuxtesting.org/results/ldv).

Например, для драйвера ядра ОС Linux 3.14 drivers/usb/serial/kobil_sct.ko в конфигурации allmodcon на архитектуре x86_64 было обнаружено нарушение правила linux:alloc:irq. Данное правило требует, чтобы в контексте прерывания драйверы выделяли ресурсы неблокирующим образом. В противном случае возможно снижение производительности или зависание системы.

В процессе инициализации драйвера — ldv_insmod — были зарегистрированы обработчики USB Serial. После этого было начато выполнение основного сценария ldv_usb_serial_scenario. Модель окружения имитировала подключение устройства USB Serial. Данное устройство было успешно инициализировано драйвером при выполнении обработчиков probe и attach. Затем был имитирован вызов обработчиков уровня терминала: открытие порта open (kobil_open) и запись данных write (kobil_write). В kobil_open драйвер выделяет память блокирующим образом. Эта операция является корректной, поскольку данный обработчик вызывается в контексте процесса. В kobil_write память также выделяется блокирующим образом, что является ошибкой, поскольку данный обработчик вызывается в контексте прерывания.

Визуализация трассы ошибки

LDV. Технология статической верификации драйверов ядра ОС Linux

Страница LDV

Разработчик/участник

Компиляторные технологии

Перейти к списку всех технологий