DIVINE - это основанный на LLVM инструмент верификации, ориентированный на анализ реальных программ на языках Си и Си++.
Такие программы часто взаимодействуют со своей средой. Например, через входы от пользователей или сети. Когда эти программы анализируются, желательно, чтобы инструмент верификации мог символически работать с входами и анализировать их работу для всех входов. В DIVINE теперь можно работать с входными данными с помощью символических вычислений, инструментализированных в исходную программу на уровне биткода LLVM. Такая инструментальная программа поддерживает символические значения внутри себя и работает непосредственно на них. Приборы позволяют нам совершенствовать инструмент с поддержкой символических данных без существенных модификаций самого инструмента.
Подход к верификации и архитектура программного обеспечения
DIVINE - это средство проверки моделей явного состояния, предназначенное в первую очередь для обнаружения ошибок в многопоточных программах. Тестирование многопоточных программ является известной проблемой из-за недетерминированности при выполнении, вызванной чередованием потоков. Чтобы справиться с недетерминированностью потока управления, DIVINE всесторонне исследует все релевантные исполнения многопоточной программы. К сожалению, такой явный подход не позволяет справиться с недетерминированностью данных, вызванной общением с окружающей средой.
Для того, чтобы проверить программу с помощью входов, DIVINE должен будет изучить все возможные входы программы.
Традиционным способом справиться с входными значениями при верификации является их символическое представление, т.е. выполнение символического исполнения в программе. В DIVINE было бы достаточно расширить интерпретатор LLVM для работы с входными значениями символически и адаптировать алгоритм исследования к работе с символьными состояниями, как это делают другие инструменты. Однако это усложнило бы суть процедуры верификации и, возможно, замедлило бы ее, привело бы к появлению ошибок или уменьшило бы ремонтопригодность и расширяемость.
На рис.1 Сравнение подходов, основанных на интерпретации, и подходов, основанных на компиляции. Все манипуляции с символическими значениями обозначаются красным цветом. В обоих случаях виртуальная машина генерирует переходы в пространстве состояний и передает их в систему проверки моделей (MC), которая выполняет анализ безопасности. При компиляционном подходе символьные операции включаются в программу, в то время как в интерпретационном подходе они являются обязанностью виртуальной машины.
По сравнению со стандартными программами, программа с символическими значениями может не иметь детерминированного потока управления. Когда программа содержит ветвь, которая зависит от символического значения, оба результата могут быть возможны. Чтобы зафиксировать такое поведение в преобразованной программе, вводим недетерминированный выбор и выполняем обе ветви. Пользуемся тем, что компания DIVINE уже сейчас способна справляться с неопределенностью.
На рис.2 - Преобразование в программу, работающую с символическими значениями (справа).
Далее, в выбранном пути мы ограничиваем значения, расширяя условие пути. Изучая пространство состояний, DIVINE извлекает в алгоритме проверки моделей терминологические деревья из состояний программы и проверяет выполнимость запроса SMT Solver (Z3) на удовлетворительность состояния выделенного пути. Кроме того, компания DIVINE должна распознавать, когда она достигает многократного состояния. Следовательно, для проверки равенства состояний мы также используем SMT-решатель. Чтобы точно моделировать программную арифметику, мы используем теорию битового вектора.
На рис. 3- Преобразованная программа создает деревья терминов, которые представляют символические значения. Поля соответствуют символическим переменным, а кружки - конкретное представление терминов. Вопросительные знаки обозначают неограниченные нулевые символы. Серые прямоугольники представляют ограничения условий пути.
Сильные и слабые стороны
По сравнению с ограничивающими моделями, сильной стороной DIVINE является надежная верификация — он исследует все пространство состояний и использует формулы в теории битов для точного представления символических значений. Однако DIVINE дала несколько неверных результатов в конкурсе, но теоретически это невозможно и, скорее всего, связано с ошибками в реализации инструмента проверки.
Подход, основанный на компиляции, позволил повысить модульность инструмента. Легко изменить представление символических значений, алгоритм верификации и даже весь верификатор при сохранении преобразования. Еще одним плюсом является то, что реализация символических операций подвергается проверке со стороны верификатора.
С другой стороны, нынешняя реализация является лишь доказательством концепции. Подход, основанный на компиляции, может конкурировать с подходами, основанными на интерпретации, даже если он увеличивает размер проверяемой программы и, следовательно, может также усложнять проверку.
В настоящее время преобразование может обрабатывать только скалярные значения, поэтому проверка программ с символьной памятью пока невозможна.
Настройка инструмента
Архив верификатора можно найти на странице SV-COMP 2019 под названием DIVINE-SMT .
Обычно достаточно выполнить божественное представление следующим образом:
божественная проверка --символическая --сопоставление TESTCASE.c.
Эта команда запускает DIVINE с SMT-представлением символических данных, описанных в этой статье, и со специфическими для SV-COMP приборами.
Для эталонов SV-COMP дополнительные настройки выполняются с помощью обёртки divinesvc.3 Для DIVINE-SMT используется только опция --32 для 32-битных категорий. Обмотчик устанавливает опции DIVINE на основе файла свойств и эталона. В частности, он включает символический режим при обнаружении недетерминированности, последовательный режим при отсутствии потоков и задает ошибки, о которых необходимо сообщать на основе файла свойств. Он также генерирует файлы свидетелей. Более подробную информацию можно найти на вышеупомянутой странице распространения.
DIVINE участвует во всех категориях, но может выдавать только неизвестные результаты по категориям достижимости ошибок и безопасности памяти.
Многие люди внесли свой вклад в DIVINE, так как это программное обеспечение с открытым исходным кодом, распространяемое по лицензии ISC.
