Отчёт "Методология построения статического анализа программ для поиска ошибок и уязвимостей в исходном коде программ" по теме: "Исследование и разработка методов выявления дефектов производительности и архитектуры приложений для современных мобильных и параллельных вычислительных систем" (заключительный).

Цель: разработка методов и инструментов статического и динамического анализа, позволяющих находить дефекты проектирования и реализации приложений, критические дефекты и уязвимости, дефекты производительности программ, проявляющиеся на современных параллельных архитектурах.Для поиска дефектов производительности существенным является учет особенностей как параметров процессорной архитектуры, так и всей вычислительной системы. Разработан метод масштабирования по памяти для систем межмодульного статического анализа, необходимый для осуществления анализа больших программных систем, и реализован в компиляторной инфраструктуре LLVM. Проведена классификация методов статического анализа по уровню используемых анализаторами абстракций, и реализована инфраструктура для многоуровневого статического анализа программ на языке Java.Разработана инфраструктура динамического анализа программ для выявления дефектов с помощью механизма статической инструментации исполняемого кода в формате ELF (реализована для архитектуры ARM). Предложены метод формализации ошибочных ситуаций при статическом анализе программ в ходе символьного выполнения, предлагающий ряд способов описать искомую ошибочную ситуацию с разной степенью точности; метод поиска дефектов переполнения буфера, основанный на предложенных формализациях ошибочных ситуаций, и реализован в инструменте статического анализа Svace, разрабатываемом в ИСП РАН. Разработана методология выполнения многоуровневого анализа исходного кода для поиска ошибок в программах с использованием общей модели памяти, состоящая из внутрипроцедурного анализа с использованием модели абстрактного синтаксического дерева и его обхода, межпроцедурного анализа с чувствительностью к путям выполнения с использованием модели потока данных программы с выделением классов эквивалентности вычисленных значений. Представлен метод поиска уязвимостей в исходном коде программ на языке C# на базе отслеживания помеченных данных путем сведения к задаче достижимости на расширенном графе потока управления (IFDS-подход), и осуществлена его реализация в анализаторе SharpChecker, разработанном в ИСП РАН.