Статический анализ драйверов ОС Linux
Программа Linux Driver Verification (LDV) объявлена Центром верификации ОС Linux в июне 2009 года. Основными целями данной Программы являются:
- повышение качества драйверов устройств ОС Linux;
- создание платформы для плодотворного сотрудничества исследователей в области верификации ПО и сообщества разработчиков ядра ОС Linux;
- внедрение передовых инструментов верификации в процесс разработки и сопровождения драйверов устройств.
Для повышения качества драйверов собираются и систематизируются проблемы, возникающие в драйверах устройств, и находятся реальные ошибки в исходном коде. На основе анализа отчетов об ошибках из списка рассылки ядра Linux LKLM выделяются часто встречающиеся проблемы. Описание проблем с примерами и ссылками сохраняется в базе правил. Постепенно правила формализуются в виде, который позволяет осуществлять их автоматическую верификацию.
Интегрированная платформа служит связующим звеном между исходным кодом драйверов, ядрами ОС Linux с kernel.org, базой правил и инструментами верификации общего назначения. Платформа предоставляет анализ драйверов на основе автоматически создаваемого окружения.
Верификация осуществляется открытыми инструментами статического анализа кода для языка Си. Модульная архитектура интегрированной платформы и огромные объемы исходного кода драйверов Linux предоставляют площадку для различных инструментов верификации. Инструменты постоянно улучшаются, в частности благодаря исследованиям, проводимым в рамках данного проекта, что позволяет проводить более качественную верификацию.
Результаты
Скачать и развернуть систему верификации Linux Driver Verification Вы можете следуя следующим инструкциям.
Хотя в рамках проекта наши основные усилия были направлены на разработку и улучшение инструментов верификации, мы уже обнаружили более 350 ошибок в драйверах Linux, которые были признаны и исправлены в основной ветке ядра.
Большая часть драйверов, в которых были найдены ошибки в рамках данного проекта, используется интернациональной исследовательской группой, поддерживающей статический верификатор CPAchecker, в качестве регрессионных тестов.
Для обсуждения различных вопросов, связанных с программой Linux Driver Verification, предназначен список рассылки (на английском языке).
Подробнее
Для знакомства с проектом рекомендуем следующие статьи:
- И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов
Конфигурируемая система статической верификации модулей ядра операционных систем
Труды ИСП РАН, том 26-2, 2014. С. 5-42. - М.У. Мандрыкин, В.С. Мутилин, А.В. Хорошилов
Введение в метод CEGAR — уточнение абстракции по контрпримерам
Труды ИСП РАН, том 24, 2013. С. 219-292. - В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов
Анализ типовых ошибок в драйверах операционной системы Linux
Труды ИСП РАН, том 22, 2012. С. 349-372.
Другие работы представлены в разделе Публикации.
Наша команда
- Павел Андрианов
- Антон Васильев
- Владимир Гратинский
- Илья Захаров
- Михаил Мандрыкин
- Виталий Мордань
- Вадим Мутилин
- Евгений Новиков
- Алексей Хорошилов
- Илья Щепетков
Наша искренняя благодарность бывшим участникам проекта:
- Олег Стриков
- Александр Страх
- Павел Швед
- Марина Макиенко