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

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

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

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

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

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

Результаты

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

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

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

Для обсуждения различных вопросов, связанных с программой Linux Driver Verification, предназначен список рассылки (на английском языке).

Подробнее

Для знакомства с проектом рекомендуем следующие статьи:

Другие работы представлены в разделе Публикации.

Наша команда

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

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

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

»