Программа LDV (Linux Driver Verification)
Программа Linux Driver Verification (LDV) объявлена Центром верификации ОС Linux в июне 2009 года. Основными целями данной Программы являются:
- повышение качества драйверов устройств ОС Linux;
- создание платформы для плодотворного сотрудничества исследователей в области верификации ПО и сообщества разработчиков ядра ОС Linux;
- внедрение передовых инструментов верификации в процесс разработки и сопровождения драйверов устройств.
Для достижения поставленных целей предполагается решение следующих задач:
- создание репозитория потенциальных проблем в коде драйверов устройств ОС Linux;
- разработка специализированных инструментов верификации, выявляющих наличие потенциальных проблем в исходном коде драйверов и нацеленных на особенности анализа драйверов устройств ОС Linux;
- построение системы верификации по принципу сборки "батареи" различных инструментов верификации и статического анализа.
Программа собирается привлечь специалистов различного профиля. Разработчикам драйверов Программа позволит получить в распоряжение инструменты для верификации драйверов, анализа их совместимости с различными версиями ядра, информацию об уже известных проблемах в драйверах и рекомендации по их устранению или нейтрализации. Для специалистов по методам верификации Программа предоставит широкий полигон для экспериментальной апробации новых инструментов на реальном ПО. Кроме того, и тем, и другим будет полезен свод правил корректного взаимодействия драйверов с ядром ОС.
В настоящее время Программа находится на начальной стадии. В скором времени планируется публикация более детальной информации о ней.
Ряд публикаций по теме верификации драйверов ОС Linux собран здесь. Список проблем, обнаруженных в драйверах ОС Linux, в рамках данной Программы представлен здесь.
Приглашаем заинтересованные стороны из числа исследователей методов верификации программ на языке Си и разработчиков драйверов в партнёры Программы.