В последние десятилетия происходит значительный рост объема и сложности программного обеспечения (ПО). Сегодня речь идет о миллионах строк кода. При этом вопросы качества становятся одним из основных критериев успеха ПО на рынке, и в целом - важнейшим условием существования как самого ПО, так и индустрии в целом. К настоящему моменту создано большое количество методов верификации и остро стоит вопрос об их практическом применении.
Помимо создания более эффективных методов, важной задачей является интеграция существующих методов в реально работающие на практике цепочки (methods chains) и решения. Это можно делать с помощью композиции готовых методов по принципу черного ящика, создавая многоуровневые системы верификации. Важна также и структурная композиция методов, подразумевающая доработку и тонкую настройку каждого метода-участника результирующего ансамбля.
За последние десять лет одной из центральных тем в области языков программирования и анализа программ стало символьное исполнение - способ автоматического исследования зависимости исполняемых ветвей программы от входных данных. Анализаторы кода на основе символьного исполнения разрабатываются и используются ведущими компаниями - Microsoft, Facebook, IBM, Ericsson, Linux Foundation. Тем не менее, символьное исполнение имеет фундаментальную проблему - комбинаторный взрыв путей исполнения, связанный с экспоненциальной зависимостью количества ветвлений в программах от количества исполненных инструкций. Это существенно затрудняет использование символьных верификаторов для больших программ. Выходом здесь являются новые, более эффективные методы исследования ветвей программы.
Наш проект посвящен решению проблемы повышения эффективности методов верификации путём сочетания и интеграции различных имеющихся методов и получению качественно новых результатов, позволяющих существенно увеличить объем программного кода, на котором способны работать средства верификации. В качестве базового метода мы рассматриваем символьное исполнение. На основе эффективного символьного исполнения мы предполагаем реализовать эффективную генерацию направленных модульных тестов, позволяющих проверять сценарии выполнения программы, проходящие через заданную пользователем фрагмент программы. Данный подход будет нацелен на поиск ошибок управления памятью в системном ПО - в драйверах аппаратуры, ядрах операционных систем и СУБД, компиляторах, высокопроизводительных информационных системах и т.д.
Мы предлагаем разработать двунаправленный композициональный подход к символьному исполнению программ, который позволит выполнять поиск по ветвям программы в двух направлениях: прямом - обычное символьное исполнение от входной точки программы, - и обратном, от целевого фрагмента в программе. Для обратного символьного исполнения мы будем использовать известный подход по анализу обратной символьной достижимости (Backward Symbolic Reachability Analysis) и перспективный подход к верификации аппаратных систем на основе достижимости, направляемой свойством (Property-Directed Reachability). Двунаправленный поиск позволит отсекать экспоненциальное число путей, заведомо не достигающих целевых инструкций. Композициональность позволяет анализировать составные части большого приложения по отдельности и соединять результаты анализа, что ведёт к существенному уменьшению времени работы на больших приложениях. Для автоматической проверки выполнимости символьных ограничений будут использоваться SMT-решатели.
На основе предложенного подхода мы планируем создать эффективный генератор модульных тестов в рамках символьной виртуальной машины Klee для широко известного открытого компиляторного проекта LLVM, позволяющий подавать на вход тестам сложные структуры данных. Мы также планируем провести масштабные эксперименты для созданного подхода и программных средств на реальных индустриальных приложениях.
