ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ =
УДК 681.3.06
ОПЫТ РАЗВИТИЯ ИНСТРУМЕНТА СТАТИЧЕСКОЙ
ВЕРИФИКАЦИИ BLAST
© 2012 г. П.Е. Швед, В.С. Мутилин, М.У. Мандрыкин Институт Системного Программирования РАН 109004, Москва, ул. А. Солженицына, 25 E-mail: shved@ispras.ru, mutilin@ispras.ru, mandrykin@ispras.ru Поступила в редакцию 18.11.2011 г.
Статический верификатор BLAST является одним лучших открытых верификаторов, работающих с программами на языке Си. В статье описываются принципы реализации BLAST, те ограничения, которые выявились при его практическом использовании для верификации драйвером ОС Linux и опыт развития BLAST, полученый в проекте LDV (Linux Driver verification) [3].
1. ВВЕДЕНИЕ
1
Название инструмента BLAST - это сокращение от "Berkeley Lazy Abstraction Software verification Tool", то есть "Инструмент верификации ПО с применением ленивой абстракции, разработанный в Беркли". Это инструмент статической верификации программ на языке C, который предназначен для решения задачи достижимости. Если дана программа на C, функция main (так называемая "точка входа") и имя метки, инструмент проверяет, существует ли такое выполнение программы, которое начинается в точке входа и заканчивается в месте, отмеченном заданной меткой.
Инструмент анализирует программу с помощью подхода CEGAR (Counter-Example Guided Abstraction Refinement) - уточнения абстракции на основе контрпримеров. Подробнее об этом подходе можно прочитать в [1]. BLAST реализует CEGAR методом "ленивой абстракции", который позволяет ему выполнять меньше работы, не уточняя ту часть абстракции, которая не должна измениться после анализа контрпримеров, вместо того,
1 Работа частично поддержана ФЦП "Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2013 годы" (контракт N 11.519.11.4006)
чтобы перестраивать её всю целиком. За использование этого подхода инструмент и получил своё имя BLAST, и был впервые представлен в секции "Экспериментальные результаты" соответствующей статьи [2]. Более того, эта статья не ссылается на какие-либо другие источники, в которых BLAST был бы также описан, или хотя бы упомянут.
Поставленная перед инструментом задача проверки достижимости является алгоритмически неразрешимой, поскольку к ней может быть сведена проблема останова. Инструмент, таким образом, не гарантирует, что его анализ когда бы то ни было завершится. BLAST также может завершиться аварийно, если обнаружит, что его средств недостаточно для корректного анализа программы. У инструмента есть и другие ограничения на проверяемые программы, подробнее о них написано в секции 2.14. В этих случаях BLAST может выдать некорректный результат: как найти "ложную ошибку" (то есть указать "ошибку" в программе, в которой её нет), так и "доказать" "ложную безошибочность" (утверждение, что в программе с достижимой меткой нет соответствующего выполнения). Однако, если инструмент считает, что в программе есть ошибка, он также печатает и "трассу ошибки": путь от точки входа к ошибочной метке - а его уже может тщательно проверить пользователь на предмет того,
действительно ли такое выполнение возможно.
Чтобы построить открытую автоматизированную систему верификации драйверов Linux, описанную в статье [3], необходим инструмент статического анализа промышленного уровня. Но в этой же статье BLAST описывается, как инструмент, "intended for academic research in software verification" (то есть "предназначенный для академических исследований в области верификации ПО"). Наши эксперименты продемонстрировали, что инструмент может не только служить площадкой для экспериментов, но и на практике использоваться для интенсивной верификации драйверов. Однако много работы было проделано прежде, чем его это стало возможно.
Хорошее описание того, как работает BLAST, можно найти в [4]. Эта статья содержит пошаговое объяснение того, как BLAST верифицирует программу, на конкретном примере, но не фокусируется ни на деталях реализации, ни на объяснении корректности и концепций, на которых основан алгоритм работы этого инструмента.
В этой статье мы опишем, что сейчас собой представляет BLAST, и что мы улучшили в нём с момента релиза версии 2.5 его исходными разработчиками. Оставляя общие описания "чистых" алгоритмов другим статьям (см. [2], [4] и [5]), мы опишем те недокументированные или разбросанные по нескольким различным источникам модификации этих алгоритмов, которые были сделаны авторами инструмента. Мы будем рассматривать те алгоритмы и эвристики, которые в BLAST версии 2.5 включаются по рекомендуемым авторами опциям «-craig 2 -predH 7». Основное внимание, однако, будет уделено нашему вкладу, и, по возможности, мы будем представлять оценки эффекта от каждого отдельного улучшения в дополнение к той суммарной оценке общего эффекта от всех внесённых нами изменений, которая будет приведена в секции 3.
1.1. Как работает BLAST
Подход к статической верификации, который использует BLAST можно кратко описать как "CEGAR с ленивой декартовой предикатной абстракцией и интерполяцией Крейга для линейной арифметики и равенств
с неинтерпретируемыми функциями в качестве процедуры для поиска предикатов".
Уточним, что это означает.
Подход CEGAR, или уточнение абстракции на основе контрпримеров, описывает процесс решения задачи достижимости путём построения грубой абстракции всех возможных состояний программы при выполнении её, начиная с точки входа, и последующим итеративным уточнением этой абстракции посредством анализа возможных - с точки зрения абстракции - путей, ведущих к ошибочной метке. В уточнённой абстракции таких путей становится меньше, и этот процесс продолжается до тех пор, пока их не останется вообще, или пока один из таких путей не окажется выполнимым. См. [1] для более подробной информации.
Ленивая абстракция - модификация CEGAR, характеризующаяся тем, что уточнению подлежат только те части абстракции, которые оказываются непосредственно затронуты предикатами, полученными из проанализированной трассы контрпримера. Пересмотра других частей абстракции пытаются в таком подходе избежать. Смотрите [2] для дополнительной информации.
Декартова предикатная абстракция - представление абстрактного состояния точки программы в виде конъюнкции нуля или более предикатов над пространством переменных программы. В отличие от булевой абстракции, декартова ограничивает логику первого порядка до использования лишь конъюнкции предикатов абстракции; смотрите также [6].
Интерполяция Крейга - процедура построения так называемого интерполянта Крейга [18] по упорядоченной паре логических формул, конъюнкция которых невыполнима. Интерполянтом Крейга для такой пары называется логическая формула, которая следует из первой формулы, невыполнима в конъюнкции со второй и использует только общие для этих двух формул неинтерпретируемые символы. Хотя интерполяция Крейга изначально не являлась процедурой получения предикатов, BLAST версии 2.5 использует для этих целей именно её, руководствуясь идеями, изложенными в статье [19].
формула выполнима
-----формул^
невыполнима
Рис. 1. Схема алгоритма верификации, используемого в BLAST. Цифрами в скобках отмечены секции, где
соответствующая часть алгоритма описана более подробно.
В качестве способа представления программы используется граф потока управления (ГПУ) -конечный граф размеченной системы переходов для исходной программы. Абстракция представляется в виде абстрактного дерева достижимости (ART, Abstract Reachability Tree), префиксного дерева всех достижимых путей по вершинам ГПУ из точки входа, при этом каждая вершина дерева помечена абстрактным состоянием - регионом.
Общая схема работы инструмента изображена на рис. 1.
2. ДЕТАЛИ РЕАЛИЗАЦИИ 2.1. Общая информация
BLAST распространяется под лицензией Apache 2.0 как в виде исходного кода, так и собранным в бинарном виде под ОС Linux. Хотя BLAST включает в себя компоненты, написанные на различных языках программирования, его основная часть, реализующая алгоритмы верификации, написана на OCaml [20] и совместима с версиями OCaml 3.11-3.12. BLAST работает под Linux, но собрать его под Windows также возможно с помощью Cygwin.
OCaml - это язык с автоматическим управлением памятью, поэтому операции выделения
памяти и сборки мусора при его использовании могут занимать значительное время. Эта проблема проявилась и в BLAST. Путём подстройки некоторых документированных опций виртуальной машины OCaml, мы уменьшили время, затрачиваемое на операции с памятью, и добились на некоторых программах 20% прироста в количестве посещённых точек проверяемой программы на затраченную единицу памяти.
2.2. Представление программы
Как было замечено ранее, подход, используемый в BLAST, требует, чтобы вся программа была представлена как конечный ГПУ (граф потока управления). Непосредственное использование такой формы представления означало бы, что все вызовы функций должны быть встроены (inlined), и что рекурсия запрещается. Однако BLAST подходит к этому вопросу с несколько другой стороны. Он использует CIL [7] чтобы построить ГПУ для каждой функции, а во время анализа программы, как только встречает оператор вызова функции, BLAST автоматически переходит на ГПУ, соответствующий вызываемой подпрограмме (если этот вызов был осуществлён напрямую, а не через указатель, косвенные вызовы функций BLAST не поддерживает). Этот
Рис. 2. Представление функции assume в виде графа потока управления.
подход предоставляет большую гибкость, позволяет сократить время на подготовку программы к анализу и даёт возможность реализовать эвристики, связанные с вызовами функций. Например, BLAST может встраивать и рекурсивные вызовы, но на какую-то заранее определённую пользователем глубину.
Мы также реализовали ограничение глубины стека вызова функций для всех вызовов, а не только рекурсивных, заметив, что в анализируемых нами программах (драйверах операционной системы) часто нет необходимости глубоко исследовать все функции, поскольку ошибки, которые находит BLAST, зачастую "лежат на поверхност
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.