Введение 7
Глава 1. Обзор литературы 14
1.1 Анализаторы кода 14
1.2 Представление структуры программного кода 17
1.3 Языки спецификации поведения 20
1.4 Методы верификации 21
1.5 Методы интеграции 24
Глава 2. Архитектура программного решения 26
Глава 3. Особенности чтения исходных текстов 27
3.1 Формальная модель программы 27
3.2 Семантики языков программирования 29
3.3 Организация языково-независимого чтения 30
3.4 Метод чтения нескольких файлов и объединения их семантики 34
3.5 Система типов данных 37
3.5.1 Принципы хранения данных 38
3.5.2 Структура типов 41
3.6 Организация чтения и записи сериализированных данных . . 42
Глава 4. Виртуальная машина и промежуточное представление Midair 44
4.1 Язык Midair 44
4.2 Гипервизор и виртуальные машины 45
4.3 Трансляция подпрограмм из обобщенных деревьев в
промежуточное представление 46
4.3.1 Метод обобщения 50
4.3.2 Метод инстанцирования 52
4.4 Модифицирование и упрощение команд в результате анализа . 53
4.5 Поддержка различных языков программирования в одном
контексте 54
Глава 5. Структура и функции гибридного решателя 56
5.1 Аналитическое представление программы 56
5.2 Моделирование памяти 57
5.2.1 Версионирование переменных 58
5.2.2 Разбиение на регионы 60
5.2.3 Анализ псевдонимов 62
5.2.4 Инкрементальные и кумулятивные модели 65
5.2.5 Свойства и их перенос 66
5.3 Метод трансформации программ в SMT-представление .... 68
5.4 Обнаружение ошибок при помощи SMT-решателя 72
5.5 Обнаружение ошибок с помощью вычислителя 73
5.6 Ошибки типов 75
Глава 6. Интеграции с языковыми инструментами 77
6.1 Контракты в языке РуСи 77
6.2 Проверка комментариев Doxygen 78
6.3 Анализ групп связности 79
6.4 Анализ зависимостей 80
6.5 Анализ языка 81
6.6 Композиционный анализ 82
6.7 Интерфейс клиент-серверного взаимодействия 83
6.8 Интерактивное управление 83
6.9 Интеграция различных архитектур и компиляторов 84
6.10 Моделирование поддержки различных операционных систем . 88
6.11 Сканирующий запуск компиляции 89
6.12 Эмуляция окружения на основе аргументов компиляторов . . 90
Глава 7. Обеспечение качества решения 92
7.1 Тестирование в различных режимах и средах 93
Глава 8. Апробация решения 95
8.1 Апробация в синтетических тестах 95
8.2 Апробация на промышленных проектах 96
8.3 Тестирование межъязыкового анализа 97
8.4 Тестирование технологического решения по интеграции ... 99
8.5 Апробация в научном сообществе 101
Заключение 103
Словарь терминов 105
Список литературы 109
Приложение А. Схема работы анализатора 128
Приложение Б. Поддерживаемые дополнения 129
Приложение В. Обнаруживаемые классы ошибок 130
Приложение Г. Схема работы модуля чтения 131
Приложение Д. Универсальный языковой базис 132
Приложение Е. Принцип работы подсистемы виртуальных машин 134
Приложение Ж. Команды языка Midair 135
Приложение З. Типы и их размеры 138
Приложение И. Отображение конструкций C++ в языковой базис . 139
Приложение К. Отображение конструкций РуСи в языковой базис 143
Приложение Л. Отображение конструкций ACSL в языковой базис 145
Приложение М. Перенос тегов между регионами памяти 147
Приложение Н. Уникальные конструкции языков 148
Приложение О. Основные группы юнит-тестов 149
Приложение П. Организация системного тестирования 150
Стр.
Приложение Р. Организация тестирования в различных средах . . 151
Приложение С. Результат тестирования на бенчмарке Toyota ITC . 152
Купить

Стремительное развитие микроэлектроники в 20 веке привело к рас­пространению кремниевых микросхем в различных сферах человеческой деятельности. Долгое время увеличение производительности процессоров происходило через увеличение числа транзисторов по закону Мура [1], но индустрия постепенно стала подходить к физическим пределам плотности их размещения, что потребовало новых подходов к производству тран­зисторов [2]. Индустрия ответила концепцией параллельных вычислений, появились спекулятивное исполнение, внеочередное исполнение и другие тех­нологии, повышающие производительность. Появились специализирован­ные микросхемы, которые добились большей производительности благодаря специализации вычислений. Первыми такими микросхемами стали видео­ускорители. В дальнейшем стали развиваться программируемые микросхемы (FPGA) [3; 4], сетевые процессоры, нейросетевые процессоры, акселераторы глубокого обучения [5], сопроцессоры.
Такие методы решения проблемы производительности привели к зна­чительному увеличению сложности разработки программного обеспечения. Программное обеспечение теперь одновременно разрабатывается для ком­пьютеров, внешних устройств, сопроцессоров, FPGA, требует обучения сопутствующих нейронных сетей. В начале века на рынке процессоров господствовала архитектура x86, и разработчики предпочитали писать про­граммы только под нее. Остальные архитектуры не были массовыми. В настоящее время самой популярной архитектурой можно считать ARM [6] в связи с выпуском большого количества устройств на базе Android [7] (на базе Linux), для стационарных компьютеров — x86_64 (amd64) [8], для маршрутизаторов — MIPS. Переход компании Apple на архитектуру Apple Silicon [9] — процессоров M1 на базе ARM — существенно изменил отноше­ние рынка к процессорам ARM, и теперь сложно представить современную программу для массового потребителя без поддержки данной архитектуры.
Эта тенденция прямо влияет на анализ программ с целью выявле­ния ошибок и несоответствия спецификации. Ранние программы для ЭВМ можно было формально доказать с первой до последней строки в связи с их небольшим размером, но современные программы состоят из множества модулей, в том числе внешних, написанных на разных языках, для множе­ства операционных систем и для различающегося аппаратного обеспечения. В качестве примера можно привести современные системы быстрого оптиче­ского распознавания: низкоуровневое программное обеспечение для камеры и другой периферии написано на С или ассемблере (архитектура может быть различной), прошивка микроконтроллера, использующего камеру, написана на C/C++ (чаще всего для архитектуры ARM), передача потока осуществ­ляется на сервер на базе архитектуры AMD64, нейронная сеть тренируется на нейросетевом процессоре, используются FPGA для увеличения произво­дительности, вывод осуществляется при помощи графического ускорителя. Проверить алгоритмы таких программ очень сложно.
Разнообразие конфигураций порождает проблемы совместимости и масштабируемости. Возникает вопрос: как производить качественный ста­тический анализ программ на разных языках, для разных процессоров, опе­рационных систем?
После значительного числа инцидентов [10; 11], связанных с ошибка­ми в программах, исследователи разработали методы защиты от ошибок. Их можно разбить на несколько групп:
• Установка требований к программному коду, ограничение исполь­зуемых конструкций. Организации могут запретить использовать арифметику указателей в C [12], являющуюся значительным источ­ником ошибок. Однако данный метод является организационным, т.к. он не предотвращает возможность допустить ошибку, а скорее делает её затруднительной.
• Защитные языки программирования. Их идея сводится к снижению возможности допустить ошибку — в основном, за счет удачного синтаксиса и проверок в компиляторе [13]. Интересным способом достижения корректности является использование сертифицирован­ных компиляторов, таких как CompCert [14].
• Анализ программ — это проверка программного кода. Он может осуществляться как статически, т.е. без запуска программы и с уче­том всех возможных путей исполнения, так и динамически, т.е. с запуском программы и с учетом только действующих путей исполне­ния. Статические проверки кода могут проводиться через проверку модели, т.е. сравнение реальной программы с эталоном, заданным либо полностью формальной моделью, либо через аннотации. Дру­гой вариант — через символьное исполнение программы, которое не исключает возможность последующей проверки модели....
Купить