Содержание к диссертации
Введение
1 Автоматизированное обнаружение уязвимостей в программах на языке C 10
1.1 Типы существующих программных дефектов 11
1.1.1 Некорректные операции с памятью 12
1.1.2 Некорректные операции с целыми типами 15
1.1.3 Операции чтения неопределенного значения 18
1.1.4 Некорректное использование функций стандартной библиотеки 19
1.1.5 Утечки памяти v 20
1.2 Методы и средства обнаружения программных дефектов 20
1.2.1 Методы лексического и синтаксического анализа 22
1.2.2 Программный комплекс Splint 30
1.2.3 Программный комплекс BOON 35
1.2.4 Метод абстрактной интерпретации программ 35
1.3 Выводы 37
2 Метод обнаружения дефектов в программах на языке С 38
2.1 Введение 38
2.2 Общий подход к решению задачи обнаружения дефектов в программах на языке С 39
2.2.1 Лексический и синтаксический анализ С-программы 39
2.2.2 Преобразование .дерева разбора в промежуточное представление 39
2.2.3 Верификация программы на языке промежуточного представления . 41
2.3 Описание языка IAL 42
2.3.1 Синтаксическая структура IAL-программы 43
2.3.2 Типы данных 43
2.3.3 Константы 48
2.3.4 Инструкции 48
2.4 Математическая модель языка IAL 59
2.5 Инварианты IAL-программы 66
2.6 Базовый алгоритм генерирования инвариантов 68
2.6.1 Алгоритм обхода управляющего графа 69
2.6.2 Свойства систем интервальных уравнений 75
2.6.3 Определение инвариантов в вершинах 83
2.6.4 Теорема о корректности алгоритма генерирования инвариантов 86
2.7 Построение и проверка индуктивных гипотез 91
2.8 Выводы 92
3 Программная реализация средства автоматизированного обнаружения дефектов в программах на языке С 94
3.1 Требования к программному комплексу 94
3.2 Основные этапы метода автоматизированного обнаружения уязвимостей 95
3.2.1 Лексический и синтаксический анализ С программы 95
3.2.2 Трансляция абстрактного синтаксического дерева в промежуточное представление 96
3.2.3 Верификация IAL-программы 96
3.3 Выводы -. 104
4 Исследование эффективности средства автоматизированного обнаружения уязвимостей в программах на языке С 105
4.1 Модельные примеры 105
4.1.1 Модельный пример stack-overflow 105
4.1.2 Модельный пример heap-overflow 107
4.2 Анализ программы xorg-server 109
4.3 Выводы 112
Заключение 113
Список использованных источников 114
- Некорректное использование функций стандартной библиотеки
- Общий подход к решению задачи обнаружения дефектов в программах на языке С
- Основные этапы метода автоматизированного обнаружения уязвимостей
- Трансляция абстрактного синтаксического дерева в промежуточное представление
Введение к работе
Актуальность
Одним из важнейших условий успешного функционирования практически значимых объектов, потенциально уязвимых для кибератак, является защита используемого в их составе программного обеспечения от возможных сбоев в работе. Это условие становится особенно важным при проектировании автоматизированных систем с высоким уровнем требований к их защищенности, в том числе — при разработке и реализации программно-технических средств защиты информации, что отражено в соответствующих Руководящих документах ФСТЭК РФ [1-3]. Появление подобных сбоев зачастую связано с наличием уязвимостей (ошибок, дефектов) в программных средствах подобных систем. В их числе такие, использование которых злоумышленником может привести к нерегламентированному политикой информационной безопасности повышению его привилегий на том или ином узле системы, подлежащей защите. Кроме того, сбои в работе программ могут приводить к аварийному завершению работы важных программно-аппаратных компонентов, создавая угрозу отказа для системы в целом. Имея в виду существующие подходы к разработке и последующему сопровождению программного обеспечения [12-14,35,37,44,55], в частности, на основе уже существующих средств с открытым исходным кодом, на первый план выходят следующие задачи:
создание эффективных механизмов обнаружения потенциальных уязвимостей в программном обеспечении;
применение указанных механизмов для обнаружения и устранения уязвимостей используемого программного обеспечения;
обоснование отсутствия других уязвимостей (дефектов) в используемом программном обеспечении.
Актуальность выбора для анализа именно программ, написанных с использованием языка программирования С, обусловлена широкой распространенностью этого языка в среде программного обеспечения с открытым исходным кодом. Согласно проведенным исследованиям [63,64], на долю языка С приходится более 80% объема кода, используемого в современных программных средствах. Дополнительным фактором такого выбора является и то обстоятельство, что обеспечение корректности операций с памятью и указателями в языке С является задачей разработчика программного обеспечения.
Следует отметить, что в настоящее время эффективных и широко распространенных автоматизированных средств, позволяющих проверять корректность программ на языке С и выявлять в них возможные уязвимости, не существует. Традиционные средства статического анализа (аудита) исходного кода недостаточно точно анализируют семантику программы, и, как следствие, — приводят к большому количеству ложных предупреждений. Например, программный комплекс ITS4 [36, 74] анализирует лишь наборы лексем, сопоставляя их с образцами «потенциально опасных конструкций», хранящимися в специальной базе данных. Подобный алгоритм проверки может выдавать до 100% ложных предупреждений, не обнаружив при этом в исследуемой программе ни одной реальной уязвимости. Программный комплекс Splint [47,76] позволяет находить лишь простейшие уязвимости такие, как, например, выход за границу статического массива при обращении по фиксированному индексу. Для обнаружения уязвимостей в более сложных ситуациях анализатору необходимо предоставить специальные аннотации, составление которых представляется весьма трудоемкой процедурой. Программный комплекс BOON [58,67] реализует один из простейших вариантов «интервального анализа» — для каждой целочисленной пер'еменной х вычисляется интервал [а, Ь] ее возможных значений такой, что в каждой точке программы справедливо соотношение а < х < Ь. К недостаткам алгоритма можно отнести следующие факторы, значительно снижающие точность анализа.
Алгоритм анализа нечувствителен к потоку управления. Анализируются лишь инструкции присваивания, причем независимо от порядка, в котором они встречаются в исследуемой программе.
Отсутствует анализ указателей.
Не исследуются зависимости между различными переменными.
На рынке информационных технологий представлен также ряд коммерческих продуктов (Coverity [70], PolySpace [75]), позволяющих (по мнению их разработчиков) проводить более точный анализ исходного кода 'программ. Однако, результаты использования указанных продуктов, а также применяемые методы и алгоритмы не были опубликованы.
Программный комплекс ASTREE [65] позволяет верифицировать программы на языке С, не содержащие операций динамического выделения/освобождения памяти, а также не использующие рекурсию.
Средства динамического анализа, применяемые непосредственно во время работы исследуемой программы (например, Valgrind [49,77]), могут быть весьма эффективными для обнаружения «ошибок времени выполнения» (runtime errors). Однако, во-первых, они существенно замедляют работу программы, а во-вторых, указанные средства проверяют корректность выполнения программы лишь на конечном множестве наборов входных данных (тестов) и не могут гарантировать корректность работы исследуемой программы в процессе ее дальнейшей эксплуатации. По этой причине, методы динамического анализа не являются полноценной заменой статическим методам аудита исходного кода С-программ.
С учетом представленных выше доводов, задача создания методов и средств, позволяющих в автоматизированном режиме находить в программах на языке С потенциально уязвимые места, а именно — конструкции, выполнение которых может быть некорректным (неопределенным) согласно спецификации языка программирования С, а также гарантировать корректность выполнения других участков кода, является в настоящее время крайне актуальной.
Цель работы
Целью диссертационной работы является исследование и разработка математических моделей, алгоритмов и программных средств автоматизированного обнаружения дефектов (уязви-мостей) в программах на языке С, которые основаны на использовании формальных методов верификации и статического анализа таких программ, ориентированных на применение к крупным программным комплексам с открытым исходным кодом, содержащим до 500 тыс. строк кода.
Основные результаты работы
На защиту выносятся следующие основные результаты диссертационной работы:
систематизирована исследуемая предметная область, введено понятие программного дефекта, предложена классификация существующих программных дефектов С-программ;
предложен метод автоматизированного обнаружения дефектов в программах на языке С, основанный на преобразовании исходной программы в промежуточный формат «IAL» (от Intermediate Analyser Language) с последующей верификацией полученной IAL-программы;
разработан язык IAL промежуточного представления С-программ, описаны его синтаксис и семантика, разработана математическая модель языка IAL, в рамках которой формализована задача верификации IAL-программ;
разработан базовый алгоритм верификации программ в формате промежуточного представления, сформулирована и доказана его корректность, предложен не нарушающий корректности алгоритма способ проверки индуктивных гипотез, позволяющий повысить точность
анализа;
5) создан прототип программного комплекса автоматизированного обнаружения дефектов в
программах на языке С, эффективность которого продемонстрирована как на ряде специ
ально подобранных модельных примеров, так и на примере программы xorg-server — ос
новной части подсистемы управления графикой в UNIX-подобных операционных системах.
Методы исследования
В работе применяются методы верификации программ, методы дискретной оптимизации, методы программной инженерии. При изложении результатов диссертационной работы используется аппарат математической логики, дискретной математики, теории графов.
Научная новизна
Автором разработан новый, доказательно обоснованный метод статического анализа исходного кода программ на языке С, позволяющий гарантированно выявлять в таких программах некоторые классы дефектов (уязвимостей). Отличительными особенностями разработанного метода являются: строгая формализация задачи обнаружения программных дефектов в рамках построенной математической модели; использование этой модели для обоснования корректности представленного базового алгоритма; возможность корректного расширения базового алгоритма, позволяющего значительно повысить его эффективность (метод проверки индуктивных гипотез).
Практическая значимость
Автором совместно с К. А. Шапченко и О. О. Андреевым разработан прототип программного комплекса автоматизированного обнаружения дефектов в программах на языке С, который реализует метод, представленный во второй главе диссертации. В работе продемонстрированы функциональные возможности созданного прототипа, а также его эффективность для анализа существующих крупных программных комплексов.
Апробация работы
Основные результаты диссертации докладывались на международной научной конференции «Информационная безопасность регионов России (ИБРР-2003)», на международных конференциях «Математика и безопасность информационных технологий» (2004-2006), «Ломоносовские чтения» (2006-2007), на механико-математическом факультете МГУ имени М.В. Ломоносова на семинаре «Проблемы современных информационно-вычислительных систем» под руководством д.ф.-м.н., проф. В.А. Васенина .(2004, 2009).
Публикации
По теме диссертации опубликовано 10 научных работ, в том числе в зарубежных журналах, из них одна статья [24] в журнале из перечня ВАК ведущих рецензируемых журналов, а также — 4 патента на изобретения [29-32]. Материалы работы вошли в главу 7 опубликованной в 2008
году книги «Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия» под ред. д.ф.-м.н., проф. В.А. Васенина [27].
Структура и объем диссертации
Работа состоит из введения, четырех глав, заключения, списка литературы. Общий объем диссертации — 120 страниц. Список литературы включает 77 наименований.
Первая глава является вводной и посвящена исследованию и систематизации подходов к классификации уязвимостей (дефектов) программного обеспечения, а также методам и средствам их обнаружения. В заключении главы представлено общее описание разработанного автором метода (основные этапы) автоматизированного обнаружения программных дефектов в программах на языке С.
Во второй главе представлен разработанный автором метод гарантированного обнаружения дефектов в программах на языке С, который основан на преобразовании исходной программы в промежуточный формат «IAL» (от Intermediate Analyser Language) с последующей верификацией полученной IAL-программы. В разделе 2.3 приведено описание языка промежуточного представления IAL. С целью обоснования полноты метода, в разделах 2.4-2.5 представлена разработанная автором математическая модель, в рамках которой формализована задача верификации IAL-программы. В разделе 2.6 описан разработанный автором базовый алгоритм верификации IAL-программ, сформулирована и доказана его корректность. В разделе 2.7 предложен не нарушающий корректности базового алгоритма способ проверки индуктивных гипотез, позволяющий существенно повысить точность анализа.
В третьей главе рассматривается архитектура разработанного автором прототипа программного комплекса автоматизированного обнаружения программных дефектов («Анализатора»). В разделе 3.1 представлен перечень функциональных требований к разработанному программного средству. В разделе 3.2 рассматриваются основные этапы метода: лексический и синтаксический анализ; преобразование дерева разбора в промежуточное представление; верификация IAL-программы. В подразделе 3.2.3 приведена структура модулей IAL-анализатора, а также рассматриваются вопросы соответствия «IAL-анализатора» разработанным математическим моделям и алгоритмам.
Четвертая глава посвящена исследованию эффективности (тестированию) созданного прототипа программного комплекса. Тестирование проводится на ряде модельных примеров — специально подготовленных программах небольшого размера, а также на примере программы xorg-server (основной части графической подсистемы X.Org, используемой в большинстве UNIX-подобных операционных систем).
В заключении перечисляются основные результаты диссертационной работы.
Некорректное использование функций стандартной библиотеки
Каждый раз при прохождении строки 4 выделяется новый участок памяти. Указатель на старый участок при этом перезаписывается. В строке 7 выполняется освобождения участка памяти, выделенного на последней итерации цикла 3-6. Однако, первые несколько выделенных участков остаются в динамической памяти. Вместе с этим, в программе не сохранились указатели на выделенные участки памяти. Таким образом, в строке 7 невозможно ни получить доступ, ни удалить выделенные участки памяти, кроме последнего.
Реализация злоумышленником уязвимостей данного типа не может привести к повышению его привилегий на атакуемом вычислительном узле, а лишь к его отказу в обслуживании. По этой причине, утечки памяти редко относят к критическим уязвимостям. Тем не менее, на практике утечки памяти встречаются достаточно часто. Примерами известных уязвимостей данного типа являются CVE-2009-3612, CVE-2009-2903, CVE-2009-3228 (утечки памяти в ядре ОС Linux версий 2.4.x, 2.6.x), CVE-2008-6194 (утечка памяти в DNS-сервере Microsoft Windows) и другие.
Существующие в настоящее время методы автоматизированного обнаружения уязвимостей можно условно разделить на два класса. К первому классу относятся методы статического анализа, применяемые на этапе компиляции программы. Такие методы активно используются на ряде важных направлений в сфере информационных технологий, включая такие направления, как информационная безопасность (например, для автоматизированного обнаружения возможых ошибок в исходном коде программы), разработка компиляторов (например, для разработки алгоритмов оптимизации объектного кода). В качестве входных данных методы статического анализа принимают исходный или объектный код исследуемой программы. В процессе анализа проводится лексический, синтаксический и, возможно, семантический анализ кода. Выходными данными является определенным образом структурированная информация о свой- ствах исследуемой программы. Таким образом, методы статического анализа, ориентированные на выявление возможных программных дефектов и уязвимостей, могут на выходе выдавать список «подозрительных точек», то есть участков кода, выполнение которых может быть некорректно. Примерами средств статического анализа являются ITS4 [36,74], FlawFinder [71], Splint [47,76], BOON [58,67], (i)CSSV [41,42], PolySpace [75], Coverity [70] и другие.
Ко второму, классу относятся методы динамического анализа. Методы динамического анализа применяются непосредственно во время выполнения исследуемой программы. Такие методы как правило используются на этапе тестирования. Принцип их работы основан на использовании специальной программной оболочки, позволяющей интерпретировать машинный код и эмулировать его выполнение. При этом, кроме выполнения операций самой программы, оболочка производит специальные проверки, которые позволяют определить, является ли соответствующая операция исследуемой программы корректной. Примером широко используемого средства динамического анализа является программный комплекс Valgrind [49,77]. В его состав входит модуль memcheck, позволяющий проверить корректность всех адресов памяти, по которым обращается исследуемая программа. Из недостатков метода можно отметить неизбежность дополнительных накладных расходов, связанных с проверками корректности операций исследуемой программы. Например, использование memcheck замедляет работу исследуемой программы в среднем в 35.5 раза [48]. Помимо указанного недостатка, необходимо также отметить, что методы динамического анализа могут гарантировать лишь корректность выполнения программы на тех входных данных, которые были для этого сформированы. По этой причине, для доказательства отсутствия в исследуемой программе дефектов определенных классов (например, ошибок при выполнении потенциально небезопасных операций с памятью) указанные методы не подходят.
Существующие технологии аудита исходного кода можно разделить на две категории. К первой категории относятся методы лексического и синтаксического анализа, основанные на использовании базы шаблонов корректных и некорректных синтаксических конструкций [36,71,74]. Их достоинством является простота реализации и высокая скорость работы. Главным недостатком является недостоверность с их помощью получаемого результата, поскольку соответствие/несоответствие исходного кода фиксированной базе шаблонов синтаксических конструкций не является признаком наличия или отсутствия в анализируемой программе уязвимостей или ошибок. Более подробно методы лексического и синтаксического анализа рассмотрены в 1.2.1.
Ко второй категории относятся методы, осуществляющие какой-либо семантический анализ [18,39,41,42,47,58,67,75,76]. Принцип работы подобных методов в общем виде можно представить следующим образом: по исходному коду программы на основе семантики используемого языка программирования строится некоторая формальная модель ее функционирования; построенная модель анализируется на предмет возможности перехода вычислительной системы в одно из множества отмеченных состояний.
Отмеченные состояния могут означать выполнение некорректной операции либо, наоборот, успешное завершение выполнения программы. При этом как сама модель, так и алгоритмы ее анализа определяются целью проведения такого анализа. Более подробно методы, позволяющие учитывать семантику программы, рассматриваются в подразделах 1.2.2-1.2.4.
Общий подход к решению задачи обнаружения дефектов в программах на языке С
В данном разделе рассмотрим общее описание разработанного автором метода обнаружения дефектов в программах на языке С. Метод, предлагаемый в настоящей работе, состоит из трех этапов: 1) проведение лексического и синтаксического анализа С-программы, построение дерева разбора/абстрактного синтаксического дерева; 2) преобразование дерева разбора в промежуточное представление; 3) верификация программы на языке промежуточного представления. Рассмотрим задачи, решаемые на каждом из указанных этапов. Лексический и синтаксический анализ представляет собой процесс сопоставления линейной последовательности символов программы с формальной грамматикой языка С (согласно стандарта «С99»). Результатом является дерево разбора или абстрактное синтаксическое дерево (см. раздел 1.2.1). Данная часть алгоритма является достаточно известной и подробно описана, например, в [4] (главы 3, 4). Структура абстрактного синтаксического дерева С-программы является весьма сложной. По этой причине на втором шаге осуществляется преобразование дерева в более простой формат, называемый «промежуточным представлением». Промежуточное представление является программой, написанной на специально разработанном для этого языке IAL (от Intermediate Analyser Language). Подробное описание языка IAL (синтаксиса и семантики) представлено в разделе 2.3. В данном подразделе рассматриваются лишь основные особенности синтаксиса и семантики языка IAL.
Программа на языке IAL является однопроцедурной и представляет собой конечный упорядоченный набор инструкций. Функции, определенные в исходной С-программе, непосредственно встраиваются в код основной процедуры. Для С-программ, не содержащих рекурсивных вызовов функций, возможность такого встраивания следует из ацикличности графа вызовов функций программы. Если же исходная С-программа содержит рекурсивные вызовы функций, то необходимо предварительно вызов каждой рекурсивной функции преобразовать в эквивалентную итерационную конструкцию, использующую динамически выделяемый массив для моделирования стека вызовов функций. Внешние по отношению к исследуемой Сопрограмме функции (например, библиотечные) заменяются на соответствующие аннотации — наборы IAL-инструкций, адекватно отражающие выполненные в рамках вызова внешней функции операции с параметрами и возвращаемым значением. Переменные в IAL-программе играют роль «регистров». А именно, они позволяют хранить значения различных типов, однако для переменной отсутствует понятие адреса или участка памяти, содержащего ее значение. Участки памяти, доступные по указателю, выделяются в IAL-программе динамически инструкцией new, а освобождаются — инструкцией del. В языке IAL принята упрощенная система типов. Определено восемь целых типов, а именно: int8, intl6, int32, int64, uint8, uintl6, uint32, uint64, а также тип указателя ptr.
Для каждого из представленных типов в точности определена его разрядность, множество допустимых значений, а также семантика арифметических операций со значениями этого типа. Вместе с тем, отсутствуют типы чисел с плавающей точкой, массивы, структуры, объединения. Операции с объектами этих типов моделируются соответствующими операциями с участками памяти. Язык IAL представляет собой разновидность трехадресного кода. Сложные выражения представлены в виде последовательности «атомарных» инструкций, а управляющие конструкции преобразованы в эквивалентные с использованием операторов if-goto и goto. Семантика IAL-программы является строгой. Любая некорректная операция (например, арифметическое переполнение или обращение к памяти по недействительному указателю) должна немедленно приводить к аварийной остановке всей программы. Преобразование С-программы к виду программы на языке IAL обладает тем свойством, что если исходная С-программа содержит дефекты, проявляющиеся при определенном воздействии на внешнее окружение, то при аналогичном воздействии на внешнее окружение IAL-программы, ее выполнение завершится в одном из аварийных состояний. Таким образом, задача обнаружения дефектов в С-программе может быть сведена к задаче верификации соответствующей ей IAL-программы. Верификация IAL-программы представляет собой основную часть разработанного метода. Целью верификации IAL-программы является выявление списка опасных инструкций, в результате выполнения которых возможен переход программы в одно из аварийных состояний. Определение 2.5. Инструкцию IAL-программы будем называть опасной, если при выполнении программы возможен переход из этой инструкции в одно из аварийных состояний. Определение 2.6. Алгоритм верификации будем называть корректным, если для любой заданной IAL-программы получаемый на выходе список инструкций содержит все ее опасные инструкции (и, возможно, некоторые другие инструкции). Свойство корректности алгоритма верификации IAL-программ (в предположении корректности алгоритма преобразования С-программ в промежуточное представление) является необходимым и достаточным условием полноты всего алгоритма обнаружения программных дефектов в программах на языке С. Для корректного решения задачи верификации IAL-программ используется подход, основанный на построении инвариантов с последующей проверкой в каждой точке программы выводимости условий корректности из инвариантов в соответствующей точке. Определение 2.7. Пусть п — номер некоторой инструкции IAL-программы Р. Инвариантом программы Р в точке п будем называть логическую формулу (р, связывающую значения переменных и состояние памяти программы, истинную всякий раз, когда текущая выполняемая инструкция имеет номер п. Определение 2.8. Пусть п — номер некоторой инструкции IAL-программы Р. Условием корректности програмлш Р в точке п будем называть логическую формулу ф, связывающую значения переменных и состояние памяти программы, которая выражает необходимые и достаточные условия, при которых выполнение инструкции с номером п не приведет к аварийному состоянию. Замечание. Класс рассматриваемых в опр. 2.7, 2.8 логических формул и способ их интерпретации будет формально определен в разделе 2.5.
Основные этапы метода автоматизированного обнаружения уязвимостей
Здесь vector, set, map — стандартные структуры данных «вектор», «множество» и «отображение» соответственно. Класс IAL_Statement описывает инструкцию IAL-программы, сопоставляемую некоторой вершине ее управляющего графа. Класс Invariant описывает инвариант (условие) в некоторой точке управляющего графа. Описание класса Invariant приведено ниже. Рассмотрим основные данные-члены класса ContextGraph. Поле v_num используется для хранения количества инструкций программы (что соответ ствует количеству вершин управляющего графа в графовой модели); вершины нумеру1 ются с индекса 0. Поле start_v обозначает номер (индекс) вершины, объявляемой начальной (обычно start_v = 0). Поле stop_v обозначает номер (индекс) конечной вершины, соответствующей инструкции STOP (обычно stop_v = v_num-l). Поле base (типа set Instruction ) используется для хранения упорядоченного набора инструкций, соответствующего телу программы.
Поля nextl, next2 (типа vector int ) определяют для каждой вершины v управляющего графа соответствующие соседние вершины next+(v) и next (v), либо равны -1, если соответствующие значения отображений next+,next равны nil. Поле prev (типа vector set int») определяет для каждой вершины набор предшествующих соседних с ней вершин, в соответствии с введенным ранее отображением prev. В поле inv (типа vector Invariant ) для каждой вершины графа хранится сгенерированный инвариант (условие), которое гарантированно выполняется при каждом попадании в эту вершину до выполнения записанной в ней инструкции.
Сгенерированные инварианты, зависят от предусловий анализа программы. Таким образом, при различных предусловиях сгенерированные инварианты будут различаться. Это обстоятельство"используется в дальнейшем для проведения межпроцедруного анализа. Все функции-члены класс ContextGraph делятся на три части: функции-члены для построения графовой модели по исходному коду IAL программы. основные (интерфейсные) функции-члены для работы с графовой моделью, вызываемые управляющим модулем; вспомогательные функции-члены, в которых заложен алгоритм генерирования инвариантов и проверки условий корректности. Для построения графовой модели необходимо вызвать конструктор класса ContextGraph. Затем, необходимо вызвать парсер (ContextGraph::parse) языка внутреннего представления IAL, во время работы которого будут заполнены поля v_num, start_v, stop_v, base. Для построения графовой модели необходимо представить описание переходов (ребер графа). Для этого используется метод ContextGraph: :link. Во время его работы будут заполнены поля nextl, next2, prev. Основные функции работы с графовой моделью включают: задание предусловий для анализа в точке графа (ContextGraph: :set_acond); анализ графовой модели с заданными предусловиями анализа (ContextGraph: : analyse); процедура принимает на вход заданное количество итераций; результат анализа при этом будет сохранен в поле inv; доказанные условия корректности будут добавлены в множество deduced); получение наиболее общего инварианта в точке, связывающего только специфицированное подмножество переменных путем избавления от «лишних» переменных (ContextGraph::bound); такая процедура необходима во всех точках программы, где происходит обращение к другой функции; а таком случае необходимо ограничить инвариант на множество передаваемых параметров функции, с тем, чтобы использовать его в качестве предусловия для анализа вызываемой функции. Приведем также краткую характеристику вспомогательных функций для работы с графовой моделью.
Функция ContextGraph: :reachable(v, arcs) определяет список вершин, достижимых из вершины v по ребрам графа, за исключением ребер, указанных в параметре arcs. Каждому ребру можно поставить в соответствие целое неотрицательное число следующим образом: ребру (г;, next+(v)) сопоставляем число 2v, где v — индекс вершины; ребру (v, next (v)) сопоставляем число 2v + 1. Функция ContextGraph: :r_reachable(v, arcs) определяет список вершин, из которых достижима вершина v по ребрам графа, за исключением ребер, указанных в параметре arcs. Функция scc(v, arcs) определяет сильно связанную компоненту графа, содержащего вершину v, получающегося из исходного управляющего графа удалением ребер множества arcs. Функция root_scc(x, arcs) определяет сильно связанную компоненту графа, получающегося из исходного управляющего графа удалением ребер множества arcs; искомая сильно связанная компонента должна содержать по крайней мере одну из вершин множества х, в которую нельзя попасть по ребрам графа из других вершин множества х. Функция merge_data_f lows (arcs) принимает на вход множество ребер, входящих в некоторую вершину v, и строит инвариант, соответствующий вершине и. Результирующий инвариант является возвращаемым значением функции.
Функция fixed(loop, inv) по заданному множеству вершин и инварианту, выполненному перед выполнением инструкций из loop, строит инвариант, истинный для в любой 103 момент при прохождении любого количества и в любом порядке инструкций из loop. Фактически, функция fixed оставляет только те условия в inv, которые связывают переменные, значения которых не меняются при выполнении инструкций из loop. Функция process_simple_loop(entry, loop, black) позволяет обрабатывать «простые» циклы (простой цикл представляет собой набор вершин передача управления в который осуществляется через единственную вершину, называемую входом, entry, в цикл). Функция позволяет в вершинах цикла генерировать простые инварианты, более сильные, чем инварианты, выдаваемые процедурой fixed (loop, inv). К их числу относится генерация инварианта-условия выхода из цикла; генерация инвариантов «синхронных изменений переменных»; генерация инвариантов для монотонных изменений переменных и некоторые другие эвристические приемы. Функция process_complex_loop(entries, loop, black) позволяет корректно обрабатывать «сложные» циклы (сложный цикл представляет собой набор вершин передача управления в который осуществляется через некоторое количество вершин этого цикла, называемых входами, entries). Функция использует процедуру fixed генерирования инвариантов в циклах. Поскольку сложные циклы на практике практически не встречаются, использование этого грубого алгоритма является оправданным, а также не нарушает консервативности всего алгоритма. Функция iterate () производит одну итерацию алгоритма обхода графа. Алгоритм обхода графа был описан в предыдущей главе. Функция check, с с (v) осуществляет проверку выводимости условия корректности в точке v из сгенерированных в этой же точке инвариантов. Она вызывается для каждой вершины v, для которой определены условия корректности.
Трансляция абстрактного синтаксического дерева в промежуточное представление
В настоящее время нет общепринятого определения понятию «уязвимости вычислительной системы». Как правило, оно ассоциируется с нарушением политики информационной безопасности системы, которое может быть вызвано неправильным заданием набора правил или ошибкой в программной реализации подсистемы, отвечающей за выполнение установленных правил. В данном исследовании будем придерживаться следующих определений.
Определение 1.1. Уязвимость вычислительной системы — такое ее состояние, которое позволяет субъекту (потенциальному злоумышленнику) получить несанкционированный политикой информационной безопасности доступ к ее ресурсам, вызвать отказ в обслуживании, или каким-либо другим образом нарушить штатный режим функционирования.
Определение 1.2. Уязвимость программного обеспечения (программы) — такое ее свойство, которое позволяет субъекту (потенциальному злоумышленнику) привести систему в уязвимое состояние, воздействуя определенным образом на внешнее окружение, в котором выполняется программа.
Определение 1.3. Под внешним окружением программы будем понимать любые данные, получаемые ею из внешних источников (из файлов, из входного потока, из устройств ввода, из переменных окружения и так далее).
Определение 1.4. Под внутренним окружением программы будем понимать значения переменных и состояние памяти программы в момент ее выполнения.
В рамках настоящего исследования будем рассматривать лишь такие программные уязвимости, которые возникают из-за наличия в исходном тексте так называемых «программных дефектов».
Определение 1.5. Программным дефектом (применительно к программам на некотором языке программирования) будем называть операцию в программе, результат выполнения которой (при определенном воздействии на внешнее окружение программы) приводит к аварийному завершению работы программы, либо является неопределенным согласно спецификации используемого языка программирования.
Таким образом, идентификация синтаксической конструкции, как программного дефекта, зависит лишь от спецификации используемого языка программирования, состояния памяти и регистров процессора в момент выполнения указанной операции, и не зависит от назначения/спецификации исследуемой программы или функции. Одним из известных программных дефектов, часто приводящих к возникновению уязвимостей, является «переполнение буфера» — операция записи в массив (буфер) данных, превышающих по размеру длину самого массива (листинг 1.1). Другим примером программного дефекта является операция деления на ноль.
Полное описание существующих типов программных дефектов содержится в международном стандарте ISO/IEC 9899:1999 «Programming Languages — С» ([34], приложение J, 2), далее для краткости обозначаемом как «С99». Часть из них относится к лексическим и синтаксическим ошибкам, ошибкам статической типизации, ошибкам определения областей видимости и другим подобным ошибкам. К числу таких дефектов относится, например, использование переменной до ее объявления. Такие дефекты можно условно назвать «дефектами описания» программы, поскольку для их обнаружения не требуется запускать программу на выполнение. Дефекты описания программы могут быть выявлены большинством современных компиляторов. По этой причине в настоящем исследовании такие дефекты рассматриваться.не будут.
Оставшееся множество программных дефектов можно условно назвать «дефектами функционирования» программы. Для их обнаружения наряду с исходным кодом необходима информация о внутреннем окружении программы, которое можно получить либо путем непосредственного запуска программы, либо путем проведения глубокого статического анализа, учитывающего семантику программных конструкций. Методы обнаружения «дефектов функционирования» программ на языке С являются основным объектом исследования в рамках данной работы.
Дефекты функционирования программ можно, в свою очередь, разделить на несколько типов: некорректные операции с памятью; некорректные операции с объектами целых типов; некорректное использование функций стандартной библиотеки; чтение неопределенного значения; другие. Дополнительно, в настоящей работе также будет рассмотрена возможность обнаружения утечек памяти. Определение 1.6. К некорректным операциям с памятью будем относить такие, для которых выполнено одно из следующих условий: операция является операцией обращения (на запись или на чтение) к несуществующему на момент обращения объекту; операция является операцией разыменования недействительного указателя; операция является операцией обращения к элементу массива по индексу, выходящему за границы массива; операция является операцией вызова функции, причем типы формальных параметров (formal parameters) или их количество не совместимы с типами или количеством действительных параметров (actual parameters). Иногда в литературе для обозначения того же типа программных дефектов используют термин переполнение буфера [15]. Некорректные операции с памятью являются одним из наиболее опасных типов программных дефектов. Связано это с тем обстоятельством, что, зачастую такие дефекты являются критическими уязвимостями вычислительной системы, и могут быть легко использованы злоумышленником для получения несанкционированного доступа к системе. В качестве примера рассмотрим сценарий классической атаки, называемой «срыв стека», на следующем простом примере:
На рис. 1.1 а), б), в) показаны состояния стека в зависимости от вводимых данных. Можно заметить, что в случае в) в процессе копирования строки будут перезаписаны данные на стеке, включая передаваемый в качестве аргумента указатель bar, указатель кадра, адрес возврата (то есть адрес инструкции родительской функции, следующей за инструкцией вызова функции foo). На рис. 1.1 в) адрес возврата изменен таким образом, что он указывает на начало массива с, лежащего в стеке. В случае использования уязвимости злоумышленником в начале этого массива вместо повторяющихся символов А можно расположить произвольный машинный код. Наиболее часто для этой цели используется код, запускающий командную оболочку (так называемый «шеллкод», shellcode). В результате описанных выше действий, злоумышленник получает привилегии пользователя, от имени которого запущена скомпрометированная им программа. Этот вид атаки называется «срывом стека».
В операционной системе существуют различные механизмы защиты от подобных атак. В основном, такие механизмы позволяют затруднить проведение атаки, однако не могут гарантировать безопасность системы. К числу таких механизмов относятся следующие.
Защита стека путем добавления специальных «контрольных байтов». Проверка целостности стека осуществляется непосредственно перед выходом из функции (по адресу воз врата) путем сравнения значения контрольных байтов с некоторым «эталонным» значением. В работе [40] указанная технология рассматривается более подробно. Отметим, что технология внедрения «контрольных байтов» не предоставляет надежной защиты программы от атаки типа «срыв стека». Злоумышленник, зная об используемой защите, может добиться своей цели, переписывая лишь некоторые адреса стека, сохранив, тем самым, целостность контрольных значений.
Защита стека путем обращения направления его роста. В большинстве аппаратных архитектур стек растет в направлении уменьшения адресов. Таким образом, при выходе за верхнюю границу локального массива может произойти затирание адреса возврата (поскольку адрес возврата расположен дальше от вершины стека). Однако, легко понять, что переполнение массива может также происходить и в случае выхода за нижнюю границу массива (то есть обращение к элементам с отрицательным индексом). Таким образом, данное решение также не является достаточно надежным.
Организация «неисполнимого» стека. В современных ЭВМ на аппаратном уровне имеется возможность реализовать следующий механизм защиты. Перед выполнением машинной команды проверяется ее расположение в памяти, и, в случае, если адрес команды относится к секции, отведенной для хранения стека, исполнение команды запрещается. Однако, технология неисполнимого стека, также не является надежным средством предотвращения атак, использующих переполнение буфера в стеке. Данное обстоятельством связано с тем, что нужный машинный код часто удается разместить не в стеке, а в секции динамической памяти (в куче). Переполнение буфера в стеке используется лишь для того, чтобы установить значение адреса возврата в стеке равным адресу заранее подготовленного машинного кода.
Кроме того, технология неисполнимого стека не защищает от атаки, называемой «возвратом к системной библиотеке». При реализации этого вида атаки, как и в случае простого срыва стека, злоумышленник затирает адрес возврата в родительскую функцию. Однако, в данном случае, ему не требуется размещать «шеллкод» в памяти программы. Он заменяет адрес возврата указателем на некоторую, уже существующую функцию, определенную в системной библиотеке и загружаемую в память в момент вызова программы. Значение этого указателя может быть вычислено статическим анализом. Примером системной библиотеки, используемой подавляющим большинством программ, работающих под управлением ОС Linux, является библиотека GNU libc. Она содержит определения всех стандартных функций языка С. По этой причине другим распространенным названием данного вида атаки является «return to libc». Более подробно способы проведения атаки типа «return to libc», а также некоторые способы защиты от таких атак описаны в работе [57].
