Введение к работе
Актуальность темы
В работе ставится задача верификации драйверов операционной системы (ОС) Linux. Обеспечение надежности и, в частности, информационной безопасности программных и программно-аппаратных систем является одной из главных задач современных информационных технологий. Особый вклад в решение этой задачи вносят работы по верификации системного программного обеспечения, в первую очередь операционных систем. Верификация драйверов ОС Linux является критически важной задачей, так как:
Корректность драйверов является необходимым условием обеспечения надежности и безопасности систем, поскольку драйверы работают с тем же уровнем привилегий, что и остальное ядро.
Драйверы ОС Linux, входящие в ядро, это большой, стремительно растущий класс программных систем. На данный момент суммарный объем драйверов составляет более 9 миллионов строк исходного кода. За последний год он увеличился на полмиллиона строк.
При разработке драйверов ОС Linux применяются различные подходы к обеспечению качества, в частности, тестирование (динамический анализ) и статический анализ. Важным преимуществом статического анализа по сравнению с динамическим является то, что его можно проводить даже в условиях, когда в распоряжении нет оборудования, которым должен управлять тот или иной драйвер.
Для драйверов, которые входят в состав ядра, обеспечение качества проводится силами разработчиков ядра. По данным Linux Foundation, на сегодняшний день в разработке каждой версии ядра, выходящей раз в 2-3 месяца, участвуют более 1000 человек, представляющих более 200 различных организаций. Несмотря на такое большое количество разработчиков, значительное число изменений в уже выпущенных и новых версиях ядра связано с исправлением ошибок в драйверах. Так, например, анализ изменений в драйверах стабильных версий ядра за год разработки с 26.10.10 по 26.10.11 показал, что порядка 80% изменений являются исправлениями ошибок. Происходит это в силу того, что обеспечивать надежность драйверов ОС Linux затруднительно ввиду огромного количества достаточно сложного исходного кода, который должен удовлетворять большому числу разнообразных правил корректности, начиная от общих правил, которым должны подчиняться все программы на Си, и заканчивая специфичными правилами, которые говорят о том, как драйверы должны использовать интерфейс ядра.
Методы общецелевого статического анализа позволяют обнаруживать нарушения общих правил, таких как разыменование нулевых указателей, выход за границу массива. Однако, помимо них остается значительная часть специфичных для ОC Linux ошибок взаимодействия драйвера с интерфейсом ядра. По данным анализа изменений в драйверах стабильных версий ядра за год разработки с 26.10.10 по 26.10.11 количество специфичных ошибок составляет более половины от всех ошибок, являющихся нарушениями правил корректности.
Перспективным направлением является разработка высокоточных инструментов статической верификации при помощи предикатных абстракций. Примерами являются инструменты BLAST, CPAchecker, SLAM. За счет построения предикатных абстракций они позволяют показать не только наличие ошибок, но и их отсутствие для заданного правила.
Ключевым свойством высокоточных инструментов для проверки специфических правил является возможность итеративного уточнения абстракции по методу CEGAR (Counter Example Guided Abstraction-Refinement), что позволяет подстраивать абстракцию как под произвольное правило корректности, так и для конкретного драйвера. Это выгодно отличает такие инструменты от общецелевых, в которых настройка под правило корректности требует реализации соответствующей функциональности в инструменте статического анализа.
Применение инструментов высокоточного статического анализа к
драйверам ОС Linux имеет хорошие предпосылки. Высокоточные методы в
настоящее время имеют ограничения по размеру анализируемого кода (до 50100 тыс. строк). В случае драйверов это ограничение приемлемо. Размер драйверов, входящих в состав ядра ОС Linux, не превышает 50 тысяч строк, а в среднем составляет порядка 2-3 тыс. строк кода. Кроме того, важно, что большинство драйверов публикуется вместе с исходным кодом, который является необходимым для большинства инструментов статического анализа.
Для применения высокоточных инструментов требуется подготовка драйвера к верификации. Во-первых, требуется подготовить специальное окружение драйвера, которое должно описывать возможности воздействия на него с учетом ограничений, накладываемых на взаимодействия сердцевины ядра ОС с драйверами данного типа. Во-вторых, требуется формально описать правила корректности в виде, удобном для сведения задачи верификации к доказательству достижимости точки программе. При решении этих задач необходимо учитывать специфику ядра ОС Linux. Одна из главных особенностей состоит в том, что интерфейсы между драйвером и ядром ОС Linux постоянно меняются. Меняются правила взаимодействия, появляются новые, меняется окружение драйвера. Поэтому правила, модели окружения и другие части системы верификации должны быть устроены так, чтобы обеспечивать простоту развития, адаптации к текущему состоянию ядра ОС, правилам взаимодействия между драйверами и ОС. На сегодняшний день не существует методов верификации, учитывающих данные особенности.
Таким образом, задача верификации драйверов ОС Linux является актуальной, для ее решения требуется разработка нового метода верификации.
Цель и задачи работы
Цель работы - разработка метода верификации драйверов устройств операционных систем для проверки выполнения правил корректного взаимодействия драйверов с ядром операционной системы. Для достижения цели работы были поставлены следующие задачи: 1. Провести анализ существующих методов верификации драйверов;
Провести анализ ошибок в драйверах ОС Linux, приводящих к некорректному взаимодействую с ядром ОС;
Разработать метод верификации и архитектуру системы верификации драйверов ОС Linux при помощи предикатных абстракций, обеспечивающий:
верификацию драйверов в условиях непрерывного развития ядра;
возможности расширения (конфигурируемости) системы верификации драйверов за счет пополнения набора правил корректности и набора инструментов верификации.
Разработать систему верификации, реализующую метод;
Оценить реализацию метода на практике, дать оценку области применимости метода.
Научная новизна работы
Научной новизной обладают следующие результаты работы:
Метод построения моделей окружения драйверов устройств ОС Linux;
Метод построения конфигурируемой системы верификации;
Математическое доказательство адекватности предложенного метода формализации правил корректности в рамках заданного класса правил работы со структурами обработчиков событий;
Методы оптимизации предикатной абстракции в BLAST.
Практическая значимость
На основе разработанного метода была создана система верификации драйверов ОС Linux LDV (Linux Driver Verification). Система LDV позволяет находить нарушения правил корректности взаимодействия с ядром ОС для драйверов, входящих в поставку ядер ОС Linux с версии 2.6.31 по 3.4. По состоянию на 25.09.2012 было найдено более 60 ошибок, которые признаны
разработчиками ядра и уже исправлены или будут исправлены в последующих версиях.
Результаты работы будут полезны для автоматизации сертификационных процессов для компьютерного обеспечения, которые существуют у многих поставщиков дистрибутивов ОС Linux и ОС, построенных на основе ядра Linux. Также результаты могут быть использованы для проверки качества драйверов ОС Linux, для создания инструментов верификации других видов программного обеспечения, критичного по безопасности. Результаты работы могут быть использованы для сравнения характеристик различных инструментов статического анализа кода.
Доклады и публикации
По теме диссертации автором опубликовано 14 работ (из них 5 в изданиях из перечня ВАК), список которых приведен в конце автореферата.
Основные положения работы докладывались на следующих конференциях и семинарах:
Весенний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE: Spring Young Researchers Colloquium on Software Engineering, г. Санкт-Петербург, 2008 г.);
Общероссийская научно-техническая конференция «Методы и технические средства обеспечения безопасности информации» (г. Санкт- Петербург, 2008 г.);
Международный семинар «Принципы и технические средства сертификации свободного программного обеспечения» (OpenCert: International Workshop on Foundations and Techniques for Open Source Software Certification, г. Милан, 2008 г.);
Конференция разработчиков свободных программ на Протве (г. Обнинск, 2009 г.);
Международная конференция памяти академика А.П. Ершова «Перспективы систем информатики» (PSI: Perspectives of System informatics, г. Новосибирск, 2011 г.);
Международная конференция по инструментам и алгоритмам создания и анализа систем (TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, г. Таллин, 2012 г.);
Семинар «День свободного программного и аппаратного обеспечения» (г. Москва, 2012 г.);
Семинар Института системного программирования РАН (г. Москва, 2012 г.).
Структура и объем диссертации
