Архитектура Linux Driver Verification

В статье "Архитектура Линукс Driver Verification ⁰" (PDF, 700 Кб) представлено описание применимости способа статического анализа кода для проверки корректности драйверов устройств для платформы Линукс. Представленный способ дает возможность выявить ошибки на основании анализа исходных текстов, без непосредственного исполнения кода. В отличие от традиционных методов тестирования статический разбор кода дает возможность проследить немедленно все пути исполнения утилиты, в частности, нечасто встречающиеся и трудно воспроизводимые при динамическом тестировании.

Проект Линукс Driver Verification является открытым и развивается при участии организации Линукс Foundation, Института системного программирования Отечественной Академии Наук (ИСП РАН) и Федерального агентства РФ по науке и инновациям. Наработки проекта распространяются в рамках лицензии Apache. Дополнительно подготовлен online-сервис для проверки драйверов. Перечень выявленных с помощью LDV проблем возможно поглядеть на данной странице ⁰.