29.04.2014: Linux Driver Verification был представлен на Дагштульском семинаре

21-25 апереля 2014 года члены команды Linux Driver Verification Алексей Хорошилов и Вадим Мутилин приняли участие в семинаре Evaluating Software Verification Systems: Benchmarks and Competitions в городе Дагштуль. Семинар был организован Дирком Бейером (Dirk Beyer, Universität Passau), Мариикой Хайсман (Marieke Huisman, University of Twente), Владимиром Клебановым (Vladimir Klebanov, Karlsruher Institut für Technologie) и Розмари Монахан (Rosemary Monahan, NUI Maynooth).

В докладе "The Experience of Linux Driver Verification" мы представили наш опыт по верификации драйверов операционной системы Linux при помощи инструментов статической верификации, основанных на методах проверки моделей. Эти инструменты решают задачу достижимости, т.е. доказывают, что помеченные метками ошибок точки программы не могут быть достигнуты при любом ходе выполнения программы. Но драйвера устройств Linux значительно отличаются от обычных программ. В них нет традиционной точки входа в программу, кроме того в них нет точек, помеченных метками ошибок. Именно поэтому драйверы необходимо предварительно готовить к верификации.

При загрузке драйвера, ядро Linux​​ вызывает функцию инициализации драйвера, которая регистрирует функции обработчики. Затем эти обработчики вызываются ядром для обработки запросов, поступающих со стороны пользователя и аппаратного оборудования. Таким образом, для верификации необходимо подготовить модель окружения с явными вызовами обработчиков драйвера. Модель окружения должна воспроизводить все сценарии взаимодействия с драйверами какие присутствуют в реальном ядре и в то же время быть достаточно простой, чтобы существующие инструменты статической верификации могли с ней эффективно работать. Для этих целей мы предлагаем метод моделирования окружения, основанный на пи-исчислении, где окружение представляется как набор пи-процессов, взаимодействующих с драйверами посредством передачи сообщений. По пи-модели мы генерируем программу на языке Си, которая в сочетании с драйвером становится программой с традиционной точкой входа, из которой достижимы все допустимые пути выполнения в коде драйвера.

Но этот код до сих пор не имеет меток ошибок. Поэтому, второй задачей является внедрение меток, достижимость которых бы означала наличие ошибки в драйвере. Для этой цели используются возможности C Instrumentation Framework (CIF). В докладе мы представили архитектуру системы Linux Driver Verification Tools (LDV Tools), показали возможности инструментов визуализации и анализа трасс ошибок, представили примеры нескольких из 150 ошибок, которые были подтверждены и исправлены в различных версиях ядра Linux.

В завершении доклада мы обсудили извлеченные уроки. Во-первых, важным фактором полезности инструмента верификации является поддержка полного набора возможностей языка программирования. Но если инструмент всё же не поддерживает некоторые конструкции, он не должен аварийно завершать работу. Даже если инструмент уже знает, что не сможет доказать корректность программы, он может продолжить работу и найти ошибку. Второй вывод заключается в том, что для инструментов верификации эффективное игнорирование тысяч нерелевантных переходов даже более важно, чем эффективная обработка релевантных. Вполне ожидаемым заключением является вывод о том, что инженерные усилия по доводке инструментов верификации важны для его успеха. В качестве подтверждения мы привели наш опыт по оптимизации инструмента BLAST, который позволил ускорить верификацию от 8 раз на драйверах небольшого размера и до 30 раз на средних.

Основываясь на этих результатах, мы сделали несколько предложений по улучшению международных соревнований по верификации программ International Competition on Software Verification (SV-COMP). Прежде всего, существует два различных способа использования инструментов верификации программ. Первый – это доказать корректность анализируемого кода относительно некоторых свойств. Второй – найти как можно больше ошибок. В настоящее время правила и подсчет очков в соревнованиях SV-COMP оценивают инструменты только по первому направлению, в то время как было бы полезно также оценивать инструменты и по второму направлению тоже.

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

Эффективный анализ трасс ошибок, выдаваемых инструментами верификации в случае обнаружения нарушения спецификации, имеет решающее значение для промышленного использования. По крайней мере, должна быть возможность проанализировать трассу ошибок без знания деталей реализации инструмента верификации. Единый формат выдачи трассы, требуемый правилами соревнований, облегчил бы использование инструментов для верификации драйверов, так как трассы ошибок, генерируемые различными инструментами, могли бы быть преобразованы одинаковым образом для единообразной визуализации и анализа с помощью инструментов LDV Tools.

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