Исследование и разработка методов глубокого статического анализа с учетом отдельных путей выполнения и потока чувствительных данных. Проект РФФИ 20-01-00581.

Современные методы статического анализа для поиска дефектов в программах повсеместно используют чувствительный к путям анализ для обеспечения нужной полноты и качества анализа. Предложены масштабируемые методы такого анализа на основе автоматически вычисляемых резюме функций. Однако вопросы комбинирования анализа на основе резюме с межпроцедурным анализом сверху вниз, а также с анализом распространения пометок чувствительных данных, необходимым для выявления критических с точки зрения безопасности ошибок, удовлетворительно не исследованы. Целью исследования является разработка методов межпроцедурного чувствительного к путям анализа, которые применимы к анализу потока чувствительных данных, а также позволяют проводить несколько проходов по графу вызовов анализируемой системы для улучшения точности и масштабируемости анализа. Кроме того, предстоит выработать методы использования SMT-решателей в ходе выполнения чувствительного к путям анализа, которые балансируют между точностью и масштабируемостью анализа.