Введение 3
Постановка задачи 5
1. Обзорный раздел по предметной области 6
1.1. Абстрактная интерпретация 6
1.2. Реляционные и нереляционные домены 9
1.3. Существующие реляционные числовые домены 10
1.3.1 Домен, выражающий равенства 10
1.3.2 Polyhedra 10
1.3.3 Октогональный домен 11
1.4. Вывод инвариантов циклов и свойств элементов массивов . 12
2. Добавление поддержки реляционных доменов в движок 18
2.1. Схема работы движка с реляционными доменами 18
2.2. Чувствительность к путям исполнения 20
2.3. Реляционные домены и интерпроцедурность 22
3. Реализация октогонального домена 23
3.1. Абстрактный октогональный домен 23
3.2. Работа с целыми и нецелыми числами в октогональном домене 24
3.3. Учет целочисленности в строгих неравенствах 25
4. Реализация вывода инвариантов, касающихся элементов мас
сивов 27
4.1. Общее устройство домена для вывода инвариантов 27
4.2. Динамическое разбиение на подпространства 28
4.3. Выбор ограничений, хранимых для подпространств 31
4.4. Оптимизации оператора объединения 31
5. Тестирование движка с реляционными доменами 33
5.1. Проведенные тесты и их результаты 33
5.2. Сравнение с возможностями аналогичных движков 36
Заключение 37
Список литературы 38
В современном мире непрерывно увеличивается количество окружающих нас компьютерных программ. Вместе с ним неизбежно увеличивается и количество всевозможных уязвимостей и дефектов в этих программах. Ошибки в программном обеспечении приводят к плачевным последствиям — некорректной работе программ, утечкам данных разработчиков и/или пользователей, а иногда — к крупным экономическим и даже человеческим потерям. Так, проблемы в ПО стали причиной двух крушений самолетов Boeing 737 MAX в 2018 и 2019 годах.
Высокая доля потенциальных ошибок в программах выявляется компилятором или интерпретатором и выдается ими в качестве ошибок или предупреждений. Однако таким образом могут быть выявлены только наиболее стандартные и примитивные ошибки. Другим способом поиска дефектов является тестирование — ручное и автоматическое, которое позволяет проверить корректность работы ПО в сценариях различной сложности. Существенным недостатком этого метода является человеческий фактор: во- первых, разработка и проведение тестов требуют большого количества человекочасов, во-вторых, ошибки можно допустить и при составлении тестов, наконец, зачастую даже самое тщательное тестирование не способно покрыть все возможные сценарии работы программы.
В силу недостаточности приведенных методов поиска дефектов все большее развитие получают статические анализаторы — специальные программы для автоматического поиска уязвимостей в коде, которые не требуют непосредственно запуска этого кода. Статические анализаторы позволяют без помощи человека находить проблемы в коде, которые не под силу найти компиляторам. Одной из наиболее классических и развитых техник статического анализа является абстрактная интерпретация, предложенная еще в 1977 году.
Суть этой техники состоит в том, чтобы научиться представлять конкретные состояния программы (содержимого ее переменных, стека вызовов и пр.) в каждый момент времени исполнения в виде элементов некоторого абстрактного домена, и свести моделирование исполнения программы к выполнению ее инструкций над этим абстрактным состоянием. Тогда, анализируя достижимые абстрактные состояния, можно определить достижимость конкретных ошибочных состояний программы.
Ключевым фактором, определяющим точность абстрактной интерпретации, является выбранный абстрактный домен, отвечающий за хранение информации о состоянии переменных программы. Данная работа посвящена разработке и внедрению в промышленный движок абстрактной интерпретации доменов, способных выводить и использовать в анализе сложные свойства программ: неравенства, связывающие значения различных числовых переменных, а также свойства элементов массивов, выполненные на всех итерациях циклов — инварианты циклов.
В ходе данной работы в движок для абстрактной интерпретации была добавлена возможность расширения его произвольными реляционными доменами. Был реализован октогональный домен для числовых переменных. Также на основе имеющихся работ в этой области был придуман, разработан и внедрен домен, позволяющий выводить инварианты циклов и свойства элементов массивов.
Оба реализованных расширения были протестированы как на искусственных тестовых примерах, так и на реальных больших проектах. В результате оба домена продемонстрировали свою корректность и повышение точности статического анализа при их использовании. При этом октогональ- ный домен практически не оказывает влияния на скорость работы движка, а вывод инвариантов в подавляющем большинстве случаев приводит к разумному замедлению движка не более чем в несколько раз.
Оба домена оказались способны произвести точный анализ кода во многих примерах, с которыми не справились популярные находящиеся в открытом доступе аналоги.
