Верификация драйверов операционной системы Linux при помощи предикатных абстракций


Верификация драйверов операционной системы Linux при помощи предикатных абстракций

В.С. Мутилин. Начало семинара - 09 октября 2012 г.

В работе ставится задача верификации драйверов операционной системы (ОС) Linux. Верификация драйверов ОС Linux является критически важной задачей, так как драйверы - это большой, стремительно растущий класс программных систем, а поскольку драйверы работают с тем же уровнем привилегий, что и остальное ядро, то корректность драйверов является необходимым условием обеспечения надежности и безопасности систем.

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

Целью работы является разработка метода верификации драйверов устройств операционных систем для проверки выполнения правил корректного взаимодействия драйверов с ядром операционной системы.

Разработанный в работе метод верификации основан на использовании высокоточных инструментов статической верификации при помощи предикатных абстракций, примерами которых являются инструменты BLAST, CPAchecker. Ключевым свойством высокоточных инструментов для проверки специфических правил является возможность итеративного уточнения абстракции по методу CEGAR (Counter Example Guided Abstraction-Refinement), что позволяет подстраивать абстракцию под произвольное правило корректности. Для того, чтобы высокоточные инструменты было возможно применять для драйверов ядра ОС Linux разработаны следующие методы:

  1. Метод генерации окружения драйвера, который позволяет описывать возможные воздействия на драйвер с учетом ограничений, накладываемых на взаимодействия сердцевины ядра ОС с драйверами данного типа.
  2. Метод построения конфигурируемой системы верификации, обеспечивающий возможность расширения системы за счет пополнения набора правил корректности и набора инструментов верификации;
  3. Методы оптимизации предикатной абстракции в инструменте BLAST.

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

С презентацией доклада можно ознакомиться здесь.

Семинар группы

Технологии программирования

Перейти к списку семинаров ИСП РАН