Статический анализ программ для проверки настраиваемых ограничений языков программирования C и C++ тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Игнатьев, Валерий Николаевич

• Игнатьев, Валерий Николаевич
• кандидат наук
• 2015

Оглавление диссертации кандидат наук Игнатьев, Валерий Николаевич

Содержание

Введение

Глава 1. Способы формализации ограничений и модели программы для их проверки

1.1. Используемая терминология

1.2. Методы формализации и записи ограничений

1.3. Модели и представления программ для проверки ограничений

1.4. Алгоритмы статического анализа для проверки ограничений

1.5. Сравнительный обзор существующих статических анализаторов

Глава 2. Построение модели программы и её памяти

2.1. Модель программы

2.2. Операторы на ААСГ

2.3. Модель памяти

Глава 3. Формализация ограничений

3.1. Предикатная модель ограничений

3.2. Примеры формализации

3.3. Классификация ограничений

Глава 4. Алгоритмы статического анализа и их реализация в инфраструктуре Clang

4.1. Особенности реализованного подмножества правил

4.2. Этапы работы и особенности реализации анализатора

4.3. Разработанные алгоритмы анализа

4.4. Межмодульные алгоритмы

4.5. Результаты тестирования анализатора

Заключение

Список публикаций

Литература

Введение диссертации (часть автореферата) на тему «Статический анализ программ для проверки настраиваемых ограничений языков программирования C и C++»

Введение

Актуальность работы

Языки программирования С и С++, несмотря на свой возраст, остаются незаменимыми и занимают первое и четвертое место в рейтинге распространённости «ТЮВЕ» [6]. Однако бесконтрольное использование их возможностей обычными программистами часто приводит к серьезным ошибкам. Решением проблемы употребления «опасных» конструкций является введение ограничений на язык с помощью уточнения или изменения его семантики. Это достигается внедрением правил программирования, которые могут быть ориентированы на поиск различных проблем: форматирования кода, безопасности, производительности, переносимости. Минимальные наборы правил состоят из конвенций форматирования кода и именования сущностей в программе. В самых ответственных проектах используются отраслевые стандарты кодирования, например, ЛБГ [7] для ПО самолета, МШИА [8-10] для встраиваемых автомобильных систем. Так как обычно используется значительное количество правил на большом объеме исходного кода, требуется автоматизация проверки программ на соответствие им, а формулировка большинства правил в терминах языка программирования требует применения статического анализа исходного текста.

Основной проблемой при этом является отсутствие универсального статического анализатора, сочетающего достаточно качественную проверку ограничений с малым временем работы, сравнимым со временем компиляции. Под проверкой ограничений (правил) здесь и далее будем понимать проверку кода программ на соответствие этим ограничениям (правилам). Так, практически мгновенно работающие анализаторы ограничиваются только лишь проверкой стилистических правил и не способны выявить остальные ошибки. Анализаторы, осуществляющие глубокий, учитывающий контекст и поток управления анализ, требуют огромное количество ресурсов и времени, вплоть до нескольких су-

ток, имеют высокую рыночную стоимость, поэтому используются очень редко и только в больших проектах. Таким образом, оба типа анализаторов непригодны для регулярного поиска распространенных ошибок в типичных проектах. Существующие достаточно быстрые анализаторы осуществляют проверку либо очень ограниченного и специфического набора правил, например, связанных только с переполнением буфера или переносимостью, либо строгую проверку стандартов, что в прикладных программах приводит к огромному количеству предупреждений, формально нарушающих стандарт, но не провоцирующих ошибку, фактически являющихся ложными предупреждениями. Например, реализация полезного правила «не использовать вызовы функций, зависящие от порядка вычисления параметров» фактически запрещает параметры вызовов с побочными эффектами, поскольку большее недостижимо на уровне синтаксического анализа. Поэтому анализаторы такого уровня также неприменимы для прикладных программ. Таким образом, инструмент проверки правил кодирования должен работать именно на этапе написания текста программы, иметь малое время работы и минимальное количество ложных срабатываний, что требует более глубокого анализа, чем синтаксический. В связи с этим возникает необходимость создания легковесного анализатора для решения задачи проверки большинства описанных ограничений языков С и С++.

Исследования, посвященные статическому анализу, ведутся в отечественных и зарубежных научных организациях (ИСП РАН, СПбГУ, МГУ, MIT, Stanford University) [11-14] и исследовательских центрах ведущих промышленных компаний (Samsung, Intel, Microsoft, HP) [15-18]. Несмотря на это на данный момент не существует языка формального определения правил и модели правил, не выработано единой системы их классификации и отсутствует быстрый универсальный анализатор.

Таким образом, разработка формальной модели ограничений и реализация на её основе легковесного статического анализатора для проверки настраивае-

мых ограничений языков С и С++ является важной научной задачей, имеющей большое практическое значение.

Цель диссертационной работы состоит в создании формальных моделей, алгоритмов и структур данных программного средства для автоматической проверки исходного кода программ на соответствие ограничениям языков программирования С и С++ с малым временем работы, сравнимым со временем компиляции и минимальным количеством ложных предупреждений, а также реализации разработанных средств в виде легковесного статического анализатора.

Для достижения поставленной цели было необходимо решить следующие задачи:

1. Предложить формальную модель ограничений, позволяющую задавать большую часть существующих правил, нотацию для их записи, и их классификацию.

2. Разработать модель программы, включающую модель памяти, удобную для проверки программ на соответствие различным классам ограничений, основанную на представлениях программы, используемых при компиляции.

3. Разработать алгоритмы статического анализа для быстрой проверки программ на соответствие рассматриваемому множеству ограничений с минимальным количеством ложных срабатываний, в том числе межпроцедурный метод обнаружения побочных эффектов, взаимных побочных эффектов, межмодульный метод анализа исключений.

4. Реализовать разработанные модели и алгоритмы на базе компиляторной инфраструктуры Clang.

5. Провести испытания анализатора на реальных программных проектах и проанализировать полученные результаты.

Научная новизна

В работе получены следующие основные результаты, обладающие научной новизной:

1. Предложена модель С и С++ программы и её памяти для применения в статическом анализе;

2. Построена и обоснована формальная модель ограничений языка программирования, позволяющая с помощью предложенной нотации на основе оригинальной модели программы задавать стилистические, синтаксические и ситуационные правила. Предложена классификация ограничений.

3. Разработаны, обоснованы и экспериментально протестированы модель памяти С и С++ программы, алгоритмы межпроцедурного анализа программ для обнаружения побочных эффектов, взаимных побочных эффектов, необработанных или неправильно обработанных исключений языка С++.

Теоретическая и практическая значимость

Предложена модель программы на основе аннотированного абстрактного семантического графа, позволяющая эффективно решать задачи, возникающие при статическом анализе. На её основе задана модель памяти, а также её семантика в виде системы переходов на модели программы. Предложен метод формального определения ограничений языков С и С++ на основе разработанных модели программы и памяти.

Результаты, изложенные в диссертации, использованы для создания подсистемы статического анализа в компиляторе Clang, на основе которой создано средство статического анализа. Оно используется для автоматической проверки

подмножества правил из сборников MISRA, HICPP и JSF, а также стандартов написания исходного кода в программах на языках С и C+-f. Предложенные и протестированные алгоритмы анализа потока данных могут быть использованы для быстрого и эффективного решения этой задачи в других статических анализаторах для поиска дефектов программ. Разработанное средство внедрено в коммерческой компании Samsung, а также используется для проверки студенческих программ на факультете ВМК МГУ.

На защиту выносятся следующие основные положения:

1. модель программы, включающая модель памяти, используемая как для задания правил, так и для их проверки программ на соответствие им;

2. формальная модель ограничений языка программирования, позволяющая с помощью предложенной нотации задавать правила на основе разработанной модели программы;

3. классификация ограничений по уровням сложности анализа, требуемого для проверки программ на соответствие им, основанная на предложенной формализации;

4. алгоритм построения модели памяти, алгоритм межмодульного анализа программ для обнаружения побочных эффектов, взаимных побочных эффектов, необработанных или неправильно обработанных исключений языка С++;

5. разработанный инструмент статического анализа, использующий предлагаемые модели и алгоритмы.

Апробация работы

Основные результаты диссертации докладывались на следующих конференциях и семинарах:

1. IEEE Seventh International Conférence on Software Testing, Vérification and Validation (ICST) (Cleveland, Ohio, USA, 2014);

2. «Майоровские чтения» (Санкт-Петербург, Россия, 2013);

3. XXI Международная научная конференция студентов, аспирантов и молодых учёных «Ломоносов-2014» (Москва, Россия, 2014);

4. научно-исследовательский семинар Института системного программирования РАН

Публикации

Материалы диссертации опубликованы в 5 печатных работах, из них 2 статьи в рецензируемых журналах [1, 2], 3 статьи в сборниках трудов конференций [3-5]. В совместной работе [2] личный вклад автора состоит в разработке и описании предлагаемого в диссертации статического анализатора, являющегося частью системы Svace.

Личный вклад автора

Все представленные в диссертации результаты получены лично автором.

Структура и объем диссертации

Диссертация состоит из введения, 4 глав, заключения и библиографии. Общий объем диссертации 121 страница, включая 8 рисунков и 8 таблиц. Библиография включает 85 наименований.

Глава 1

Способы формализации ограничений и модели программы для их проверки

В настоящей главе приведён обзор существующих исследований, связанных со статическим анализом программ. В разделе 1.1 рассмотрены основные термины, используемые в тексте диссертационной работы. В разделе 1.2 приведен обзор классификаций и формальных нотаций для задания ограничений. В разделе 1.3 описаны модели и представления программ, с помощью которых производится их анализ и проверка. В разделе 1.4 обсуждаются существующие алгоритмы получения данных для проверки правил: алгоритмы поиска побочных эффектов, построения модели памяти, анализа псевдонимов. В разделе 1.4 приведён сравнительный анализ существующих средств поиска нефункциональных ошибок методами статического анализа: Coverity SA, Klocwork Insight, Parasoft C/C++ test, Svace.

Многие ограничения языков С и С++ содержатся в уже опубликованных стандартах программирования (JSF, MISRA) и сборниках правил кодирования (HICPP). Однако проблема создания анализатора состоит в том, что поскольку данные ограничения сформулированы на естественном языке, они интерпретируются неоднозначно и неточно. Это делает их реализацию субъективной, а проверку неполной или даже некорректной, приводит к огромному количеству ложных срабатываний на прикладных программах. Поэтому, в первую очередь, для создания эффективно работающего анализатора необходимо провести их формализацию. Стандартизированной или общепринятой модели и нотации для ограничений на данный момент не существует, поэтому в этой главе приводится обзор существующих методов их формальной записи и классификации.

В разделе 1.2 рассмотрены различные модели программ, используемые для

определения и проверки ограничений. Наиболее распространенным с практической точки зрения является представление программы в виде абстрактного синтаксического дерева (АСД), а правила жестко запрограммированы непосредственно в анализаторе. Это позволяет добиться высокой производительности, однако ограничивает количество доступных для проверки правил. Кроме того, анализ только АСД, как правило, приводит к сравнительно низкой точности. Рассмотренное представление программы в виде необходимых фактов на языке Пролог позволяет задавать правила на этом же языке с использованием разработанной библиотеки, однако имеет невысокую скорость работы, а точность определяется способом извлечения фактов из программы, которая в теоретических работах обычно ограничена синтаксическим анализом. Другие представления правил, например, используемое при рефакторинге, сильно ограничивают множество правил, доступных для проверки, а также требуют создания интерпретатора. Таким образом, использование нового декларативного языка для формальной записи правил приводит к значительным накладным расходам на его интерпретацию, поскольку не задает механизма проверки. Кроме того, для освоения языка уровня Пролога и знакомства с библиотекой реализованных предикатов требуется сравнительно высокая квалификация и немалое количество времени.

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

а для реализации в анализаторе - язык, на котором написан анализатор. При этом получается декларативная и императивная форма записи правила на базе общей модели программы.

Для применения анализатора в прикладных программных проектах необходимо выдавать предупреждения только в тех ситуациях, которые действительно могут приводить к ошибкам. Как уже было отмечено, для этого в большинстве случаев недостаточно синтаксического анализа или анализа типов, а требуется информация о потоке данных и потоке управления программы. Многие алгоритмы, используемые для вычисления необходимых анализатору данных, позаимствованы из области компиляторных технологий. К ним относятся алгоритмы синтаксического и семантического анализа, построения абстрактного синтаксического дерева, графов потока управления и вызовов, поиск инварианта в цикле и метод решения задачи потока данных. Однако при создании анализатора требуется решение ряда специфичных задач, например, вычисление конкретных побочных эффектов выражений, поэтому в разделе 1.3 приводится описание существующих алгоритмов для извлечения необходимой для проверки правил информации. К ним относятся алгоритмы поиска побочных эффектов, алгоритмы построения модели памяти, анализ границ значений переменных, а также анализ исключений в программе на С++.

В разделе 1.4 проведен сравнительный обзор существующих статических анализаторов. Часть из них, осуществляя глубокий анализ исходного кода, требует огромного количества ресурсов, другие ограничиваются лишь синтаксическим анализом, что либо сокращает набор реализованных правил, либо значительно снижает качество результатов. Таким образом показано, что существующие инструменты не решают поставленных задач.

1.1. Используемая терминология

При описании алгоритмов и моделей будем предполагать, что программы заданы на языках С или С++. Все рассматриваемые алгоритмы анализа являются статическими, т.е. не требующими запуска программы для своей работы. Используемые в тексте работы английские термины из области компиляторных технологий соответствуют терминологии, принятой в книге [19]. Будем использовать понятие «выражение» (expression) для обозначения выражений языков С и С++ согласно пунктам 5.1 стандартов [20, 21], где оно определяется как последовательность операторов и операндов, задающих некоторое вычисление. Термин «оператор» (statement) мы будем понимать в контексте рассматриваемых языков программирования. Операторы определяются в указанных выше документах в главе 6 [20, 21] и задают действие, которое необходимо выполнить, например, операторы for, switch. Термин «операция» (operator) также в соответствии со стандартами используется для обозначения операций языка, например, бинарные операции сложения, умножения, унарная операция отрицания. Для обозначения некоторой атомарной операции на промежуточном представлении программы будем использовать термин «инструкция» (instruction).

Семантика и синтаксис языка определены в соответствующем стандарте, который, тем не менее, оставляет многое на усмотрение компилятора. Для этого используются специальные формулировки:

• неспецифицированное поведение (unspecified behavior}. допустимы два и более различных поведений программы, например, порядок вычисления аргументов функции;

• зависящее от реализации поведение (implementation defined behavior}. неспецифицированное поведение, которое должно быть зафиксировано в документации компилятора, например, размер и место старшего байта в цело-

численном типе;

• неопределенное поведение (undefined behavior): стандарт вообще не предлагает никаких рекомендаций к поведению программы, вплоть до возможности аварийного завершения, например, разыменование NULL.

Обобщения распространенных ошибок и неопределенностей в стандарте являются основными источниками для появления правил.

Первым формально выделяемым этапом компиляции и статического анализа программы является лексический анализ - процесс разбора входной последовательности символов, задающих программу, их группировка в лексемы с целью получения на выходе цепочки токенов для всех лексем. Токен представляет собой пару имени и необязательного атрибута. В языке С определено 5 типов токенов: ключевые слова, идентификаторы, константы, строковые константы и пунктуаторы.

Следующим этапом анализа программы, как правило, является синтаксический анализ - процесс сопоставления линейной последовательности токенов языка программирования, полученных в результате лексического анализа, с его формальной грамматикой. Результатом обычно является абстрактное синтаксическое дерево (ЛСД) - помеченное ориентированное дерево, в котором внутренние вершины сопоставлены с операторами и операциями языка программирования, а листья - с соответствующими им операндами. На следующем этапе семантического анализа проверяется наличие семантических ошибок и накапливается информация о типах для дальнейших стадий - генерации промежуточного представления и оптимизаций.

Для представления множества всех путей исполнения программы используется граф потока управления функции F - пара где V - множество вершин, соответствующих базовым блокам F, Е — V xV - множество дуг, соответствующих передаче управления между базовыми блоками, причем в множе-

стве V выделены два элемента, обозначающих вход и выход потока управления функции. Под базовым блоком будем понимать последовательность инструкций, содержащую только один вход и только один выход и не содержащую инструкций передачи управления. Таким образом, базовый блок - это последовательность инструкций, каждая из которых исполняется тогда и только тогда, когда исполняется первая инструкция из последовательности [22].

Под термином побочный эффект (side effect) мы будем понимать изменение нелокальных данных [23], например, модификацию глобальной или статической переменной в функции или генерацию исключения. Согласно [24] функция имеет побочные эффекты тогда и только тогда, если

1. производит операции ввода-вывода;

2. изменяет значение глобальной переменной;

3. изменяет значение статической переменной;

4. изменяет значение параметра функции, переданного по ссылке;

5. изменяет значение переменной, определенной глубже в стеке вызовов, например, через указатель;

6. изменяет состояние динамической памяти программы;

7. вызывает функцию, имеющую побочные эффекты.

1.1.1. Статический анализ

Как правило, программное обеспечение хорошо работает в предсказуемом (предполагаемом при разработке) окружении. В противном случае часто возникают ошибки. Для сокращения их количества разработаны различные методологии разработки ПО. В книге [25] обобщаются 7 базовых принципов разработки безопасного ПО:

1. автоматизированный анализ кода:

• статический анализ;

• инструментальная инспекция кода (code review);

2. анализ рисков;

3. тестирование на проникновение (penetration testing);

4. основанные на оценке рисков тесты безопасности;

5. возможности злоупотребления;

6. требования безопасности;

7. меры безопасности.

Рис. 1.1. Семь принципов разработки безопасного ПО по МсСгаш [25] на схеме жизненного цикла ПО

На рисунке 1.1 для каждого этапа жизненного цикла ПО цифрами отмечены соответствующие ему принципы производства безопасного ПО. Детальный анализ предложенных принципов [25] показывает, что статический анализ исходного кода программы является одним из важнейших методов для написания качественного и безопасного ПО.

Основные методологии использования статических анализаторов при разработке хорошо освещены в книге [26], где показано, что применение статического анализа не ограничивается автоматизированным поиском фиксированного набора ошибок. Предложено также использовать средства статического анализа исходных текстов для инструментальной инспекции кода. Большое внимание

План тестирована

а

в книге уделяется обнаружению ошибок безопасности и наиболее распространенным случаям их возникновения, например, переполнению буфера. Довольно часто программисты совершают ошибку, подразумевая под безопасностью ПО алгоритмы шифрования, схемы передачи паролей и ключей. Однако в [26] убедительно показано, что значительно больше проблем с безопасностью возникает из-за ошибок в исходном тексте. Проведенный авторами обзор существующих методов тестирования: на основе моделей, на проникновение, семейство методологий тестирования «черный ящик» и фаззинг (fuzzing), - показывает, что статический анализ позволяет проще находить определенные классы ошибок, например, уже отмеченную ошибку переполнения буфера, часто приводящую к уязвимостям.

По сравнению с другими методами поиска ошибок в программе статический анализатор имеет ряд существенных преимуществ.

1. Полное покрытие исходного текста. В отличие от ручной инспекции программы, статический анализатор не может пропустить «неинтересные» участки кода. В противоположность динамическим средствам обрабатывает все пути выполнения программы, причем, как правило, сложность не возрастает экспоненциально.

2. Находит ошибку, а не симптомы. Результатом работы статического анализатора является список найденных проблем с указанием точного места в исходном тексте программы и вида ошибки. Например, находится конкретное место переполнения буфера, а не факт, что при подаче на вход определенных данных программа аварийно завершается.

3. Обнаружение ошибок на самых ранних стадиях разработки Эта черта позволяет не только снизить стоимость исправления ошибки, но и предоставить быструю обратную связь: после исправления программист не будет допускать такую ошибку в дальнейшем.

4. Возможность работать с большим объемом кода и проверять одновременно несколько классов ошибок. Кроме того, в случае нахождения нового типа ошибки статический анализатор может автоматически перепроверить большое количество кода.

Разумеется, статические анализаторы имеют недостатки. В общем смысле задача статического анализа заключается в вычислении различных свойств анализируемой программы, функции, переменной. Для части таких свойств существуют алгоритмы вычисления, для некоторых - нет. С теоретической точки зрения задача статического анализа алгоритмически неразрешима [26, 27]. Это следует из теоремы Райса: «для любого нетривиального свойства вычислимых функций, определение, вычисляет ли произвольный алгоритм функцию с таким свойством, является алгоритмически неразрешимой задачей». Это легко показать на простом примере 1.

Алгоритм 1 Алгоритмически неразрешимый пример для статического анализа 1: procedure TEST(program Р)

2: if Р завершается then > Проблема останова

з: call unsafe( )

4: end if 5: end procedure

Легко увидеть, что для того, чтобы определить, вызовется ли функция UNSAFEQ, статический анализатор должен решить проблему останова, для которой Тьюрингом доказана алгоритмическая неразрешимость. Таким образом, задача статического анализа произвольной программы сводится к неразрешимой алгоритмически проблеме останова.

Более практически значимой, чем проблема останова, является алгоритмическая неразрешимость задачи анализа указателей [28], которую требуется решить при поиске нескольких классов ошибок во время статического анали-

за. Таким образом, для алгоритмически невычислимых свойств используются эвристические алгоритмы, которые могут приводить к пропуску ошибок или к ложным предупреждениям анализатора. Наряду с повышением качества алгоритмов, одним из практических решений проблемы ложных срабатываний является использование механизма их пометки, что при регулярном использовании анализатора позволяет свести к минимуму указанную проблему.

Для сравнения различных реализаций анализаторов требуется введение некоторых критериев, оценивающих их практическую применимость. На основе приведенного списка в работе оценивается эффективность предлагаемого анализатора.

Критерии сравнения статических анализаторов:

1. Множество обнаруживаемых ошибок. В зависимости от назначения и используемых алгоритмов, статические анализаторы могут обнаруживать различные типы ошибок, что непосредственно влияет на их практическую применимость. Существуют различные специализированные анализаторы, например, для проверки форматирования исходного текста, и универсальные - для поиска различных ошибок в программе.

Список литературы диссертационного исследования кандидат наук Игнатьев, Валерий Николаевич, 2015 год

Литература

6. Software Т. ТЮВЕ Software: Tiobe Index. URL: http://www.tiobe.com/ index. php/content/paperinf о/tpci/index. html.

7. С++ Coding Standards Document for the new Joint Strike Fighter (JSF): Tech. rep.: Lockheed Martin Corporation. URL: http: //digg.com/programming/C_Coding_Standards_Document_for_the_new_ Joint_Strike_Fighter_JSF.

8. MIRA Ltd. MISRA-C:2004 Guidelines for the use of the С language in Critical Systems / MIRA. Motor Industry Software Reliability Association, 2004. URL: www. misra. org. uk.

9. MIRA Ltd. MISRA С++: 2008: Guidelines for the use of the С++ language in Critical Systems. Motor Industry Software Reliability Association, 2008.

10. MIRA Ltd. MISRA С 2012 C3: Guidelines for the Use of the С Language in Critical Systems. Motor Industry Software Reliability Association, 2013.

11. Аветисян А. И., Бородин A. E. Механизмы расширения системы статического анализа Svace детекторами новых видов уязвимостей и критических ошибок // Труды Института системного программирования РАН. 2011. Т. 21. С. 39-54.

12. Jourdan J.-H., Laporte V., Blazy S. et al. Formal verification of а С static analyzer // POPL (Principles Of Programming Languages). 2015.

13. Белеванцев А. А., Велесевич В. E. Анализ сущностей программ на языках Си/Си++ и связей между ними для понимания программ. // Труды Института системного программирования РАН. 2015. Т. 27.

14. Miiller-Olm M., Seidl H. Static Analysis: 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings. Springer, 2014. Vol. 8723.

15. Reniers D., Voinea L., Ersoy O., Telea A. The Solid* toolset for software visual analytics of program structure and metrics comprehension: From research prototype to product // Science of Computer Programming. 2014. Vol. 79. P. 224-240.

16. Sreedhar V. C. System and method for static analysis using fault paths. 2014. US Patent 8,813,033.

17. Feng Y., Anand S., Dillig I., Aiken A. Apposcopy: Semantics-based detection of android malware through static analysis // SIGSOFT FSE. 2014.

18. Joshi S., Lahiri S. K., Lai A. Reducing false alarms for static analysis of concurrent programs. 2014. US Patent 8,793,664.

19. Ахо А., Лам M., Сети P., Ульман Д. Компиляторы: принципы, технологии и инструментарий. 2 изд. Вильяме, 2008.

20. ISO. ISO/IEC 9899:2011 Information technology — Programming languages — С. Geneva, Switzerland: International Organization for Standardization, 2011. — December. P. 683 (est.). URL: http://www. iso. org/iso/iso_catalogue/ catalogue_tc/catalogue_detail. htm?csnumber=57853.

21. ISO. ISO/IEC 14882:2011 Information technology — Programming languages — С++. Geneva, Switzerland: International Organization for Standardization, 2012. —Feb. P. 1338 (est.). URL: http://www. iso. org/iso/iso_catalogue/ catalogue_tc/catalogue_detail.htm?csnumber=50372

22. Cocke J. Global Common Subexpression Elimination // SIGPLAN Not. 1970. -Jul. Vol. 5, no. 7. P. 20-24.

23. Ghezzi C., Jazayeri M. Programming Languages Concepts. 2 edition. John Wiley and Sons, 1987.

24. Spuler D. A., Sajeev A. S. M. Compiler Detection of Function Call Side Effects. // Informatica (Slovenia). 1994. Vol. 18, no. 2.

25. McGraw G. Software Security: Building Security In. 2006.

26. Chess B., West J. Secure Programming with Static Analysis. 2007.

27. Sipser M. Introduction to the Theory of Computation. 1996.

28. Hind M. Pointer Analysis: Haven'T We Solved This Problem Yet? // Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. PASTE '01. New York, NY, USA: ACM, 2001. P. 54-61.

29. Anderson P. Coding standards for high-confidence embedded systems // Military Communications Conference, 2008. MILCOM 2008. IEEE. 2008.-Nov. P. 1-7.

30. Bowen J. B. Standard Error Classification to Support Software Reliability Assessment. AFIPS '80. ACM, 1980. P. 697-705.

31. Holzmann G. J. The Power of 10: Rules for Developing Safety-Critical Code // Computer. 2006. Vol. 39, no. 6. P. 95-97.

32. Marpons-Ucero G., Marino-Carballo J., Carro M. et al. Automatic Coding Rule Conformance Checking Using Logic Programming. // PADL / Ed. by P. Hudak, D. S. Warren. Vol. 4902 of Lecture Notes in Computer Science. Springer, 2008. P. 18-34.

33. Marpons-Ucero G., Marino J., Carro M. et al. A Coding Rule Conformance Checker Integrated into GCC. // Electr. Notes Theor. Comput. Sci. 2009. Vol. 248. R 149-159.

34. GCC: GNU Compiler Collection. URL: http://gcc.gnu.org.

35. Saleem S. M. A Tool For Checking Coding Standards For C++ // Indian Institute of Technology, Kanpur. 1999.

36. Matsumura T., Monden A., ichi Matsumoto K. The Detection of Faulty Code Violating Implicit Coding Rules. // ISESE. IEEE Computer Society, 2002. R 173-182.

37. Paul S., Prakash A. A Framework for Source Code Search Using Program Patterns // IEEE Trans. Softw. Eng. 1994.-Jun. Vol. 20, no. 6. P. 463-475.

38. Floyd R. W. Assigning Meanings to Programs // Proceedings of Symposium on Applied Mathematics. 1967. Vol. 19. P. 19-32.

39. Hoare C. A. R. An Axiomatic Basis for Computer Programming // Commun.. ACM. 1969.-Oct. Vol. 12, no. 10. P. 576-580.

40. Group T. P. R. High-Integrity C++ Coding Standard Manual. 2004. — May.

41. Devanbu P. T., Rosenblum D. S., Wolf A. L. Generating Testing and Analysis Tools with Aria. // ACM Trans. Softw. Eng. Methodol. 1996. Vol. 5, no. 1. P. 42-6-2.

42. Rosenblum D. S., Wolf A. L. Representing Semantically Analyzed C++ Code with Reprise // In USENIX C++ Conference Proceedings. 1991. P. 119-134.

43. Merrill J. GENERIC and GIMPLE: a new tree representation for entire functions // GCC developers summit 2003. 2003. P. 171-180.

44. Zhurikhin D., Belevantsev A., Ignatiev V. et al. Compiler-controlled and Compiler-hinted Voltage Scaling Approaches // GCC Research Opportunities (GROW'IO) / Ed. by S. M. Ryvkin. 2010.

45. Lattner C., Adve V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation // Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization. CGO '04. Washington, DC, USA: IEEE Computer Society, 2004. P. 75-105.

46. Cytron R., Ferrante J., Rosen B. K. et al. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. // ACM Trans. Program. Lang. Syst. 1991. Vol. 13, no. 4. P. 451-490. preliminary version: POPL 1989: 25-35.

47. Berger C., Rumpe B., Volkel S. Extensible Validation Framework for DSLs using MontiCore on the Example of Coding Guidelines // Symposium on Automotive/Avionics Systems Engineering 2009 (SAASE 09). 2009.-Oct.

48. Clang Static Analyzer: a source code analysis tool that finds bugs in C, C++, and Objective-C programs, http://clang-analyzer.llvm.org. URL:http: //clang-analyzer. llvm. org.

49. Clang: a production quality C, Objective-C, C++ and Objective-C++ compiler. URL: http: //clang. llvm. org.

50. GNU Coding Standards. URL: http://www.gnu.org/prep/standards/ standards. html.

51. Google C++ Style Guide. URL: http://google-styleguide.googlecode. com.

52. Meyers S. Effective C++ CD: 85 Specific Ways to Improve Your Programs and Designs. Addison-Wesley, 1999.

53. Henricson M., Nyquist E. Industrial Strength C++. Prentice Hall, 1997.

54. Sutter H., Alexandrescu A. C++ Coding Standards. Addison Wesley, 2005.

55. Spillman T. C. Exposing Side-Effects in a PL/I Optimizing Compiler. // IFIP Congress (1). 1971. P. 376-381.

56. Callahan D., Kennedy K. Analysis of Interprocedural Side Effects in a Parallel Programming Environment //J. Parallel Distrib. Comput. 1988.— Oct. Vol. 5, no. 5. P. 517-550.

57. Cooper K. D., Kennedy K. Complexity of interprocedural side-effect analysis: Tech. rep.: Lockheed Martin Corporation, 1987.— Oct.

58. Cooper K. D., Kennedy K. Interprocedural Side-effect Analysis in Linear Time // SIGPLAN Not. 1988.-Jun. Vol. 23, no. 7. P. 57-66.

59. Landi W. Undecidability of Static Analysis // ACM Letters on Programming Languages and Systems. 1992. Vol. 1. P. 323-337.

60. Andersen L. 0. Program Analysis and Specialization for the C Programming Language: Tech. rep.: 1994.

61. Steensgaard B. Points-to analysis in almost linear time // Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages / ACM. 1996. P. 32-41.

62. Kildall G. A. A Unified Approach to Global Program Optimization // Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL '73. ACM, 1973. P. 194-206.

63. Cooper K. D.; Harvey T. J., Kennedy K. Iterative data-flow analysis // Revisited, Department of Computer Science Rice University Houston, Texas, USA. 2004.

64. Khedker U., Sanyal A., Karkare B. Data Flow Analysis: Theory and Practice. 1st edition. Boca Raton, FL, USA: CRC Press, Inc., 2009.

65. Zhang J. Symbolic Execution of Program Paths Involving Pointer and Structure Variables. // QSIC. IEEE Computer Society, 2004. P. 87-92.

66. Nielson H. R., Nielson F. Semantics with Applications: A Formal Introduction. New York, NY, USA: John Wiley & Sons, Inc., 1992.

67. Coverity. Coverity Prevent: a static code analysis tool for C, C++, and Java. URL: http://coverity.com.

68. Coverity. Coverity Scan: 2012 Open Source Report. URL: http://softwareintegrity.coverity.com/rs/coverity/images/

2012-Coverity-Scan-Report.pdf.

69. Coverity. Coverity Scan: 2013 Open Source Report. URL: http://softwareintegrity.coverity.com/rs/coverity/images/

2013-Coverity-Scan-Report.pdf.

70. Klocwork. Klocwork: the set of static code analysis tools. URL: http://www. klocwork. com/.

71. GrammaTech I. GrammaTech CodeSonar: a static code analysis tool. URL: http: / / www. grammatech. com/.

72. Xie Y., Chou A., Engler D. ARCHER: Using Symbolic, Path-sensitive Analysis to Detect Memory Access Errors // SIGSOFT Softw. Eng. Notes. 2003. Vol. 28, no. 5. P. 327-336.

73. Larochelle D., Evans D. Statically Detecting Likely Buffer Overflow Vulnerabilities //In Proceedings of the 10th USENIX Security Symposium. 2001. P. 177-190.

74. Dor N., Rodeh M., Sagiv S. CSSV: towards a realistic tool for statically detecting all buffer overflows in C. / Ed. by R. Cytron, R. Gupta. ACM, 2003. P. 155-167.

75. Xie Y., Aiken A. Saturn: A Scalable Framework for Error Detection Using Boolean Satisfiability // ACM Trans. Program. Lang. Syst. 2007. Vol. 29, no. 3.

76. Cousot P., Cousot R., Feret J. et al. Combination of Abstractions in the ASTREE Static Analyzer. // ASIAN / Ed. by M. Okada, I. Satoh. Vol. 4435 of Lecture Notes in Computer Science. Springer, 2006. P. 272-300.

77. Plotkin G. D. A Structural Approach to Operational Semantics: Tech. Rep. DAIMI FN-19. University of Aarhus: 1981.

78. Карпов Ю. Г. Теория автоматов. Учебник для вузов. Питер, 2002.

79. Doxygen: a tool for automatic documetntation generation from annotated source code. URL: http: //doxygen. org.

80. Android: an operating system for mobile devices, developed in Google. URL: http: //android. com.

81. Tizen: an operating system based on the Linux kernel and the GNU С Library implementing the Linux API for mobile devices. URL: http://tizen.org.

82. Boland Т., Black P. E. Juliet 1.1 C/C++ and Java Test Suite. // IEEE Computer. 2012. Vol. 45, no. 10. P. 88-90.

83. SQLite is a software library that implements a self-contained, serverless, zero-configuration, transactional SQL database engine. URL: http://www.sqlite. org/.

84. Scratchbox: the open-source cross-compilation toolkit project. URL: http: // scratchbox. org.

85. GBS: cross-compiling infrastructure for Tizen. URL: https : //www. tizen. org.