Статический анализ драйверов ОС Linux

Программа Linux Driver Verification (LDV) объявлена Центром верификации ОС Linux в июне 2009 года. Основными целями данной Программы являются:

  • повышение качества драйверов устройств ОС Linux;
  • создание платформы для плодотворного сотрудничества исследователей в области верификации ПО и сообщества разработчиков ядра ОС Linux;
  • внедрение передовых инструментов верификации в процесс разработки и сопровождения драйверов устройств.

Для повышения качества драйверов собираются и систематизируются проблемы, возникающие в драйверах устройств, и находятся реальные ошибки в исходном коде.  На основе анализа отчетов об ошибках из списка рассылки ядра Linux LKLM выделяются часто встречающиеся проблемы. Описание проблем с примерами и ссылками сохраняется в базе правил. Постепенно правила формализуются в виде, который позволяет осуществлять их автоматическую верификацию.

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

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

Результаты

Скачать и развернуть систему верификации Linux Driver Verification Вы можете следуя следующим инструкциям. Также Вы можете проверить драйвер ONLINE!

Хотя в рамках проекта наши основные усилия были направлены на разработку и улучшение инструментов верификации, мы уже обнаружили более 50 ошибок в драйверах Linux, которые были признаны и исправлены в основной ветке ядра.

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

Наша команда

  • Илья Захаров
  • Михаил Мандрыкин
  • Вадим Мутилин
  • Евгений Новиков
  • Алексей Хорошилов

Наша искренняя благодарность бывшим участникам проекта:

  • Олег Стриков
  • Александр Страх
  • Павел Швед
»