Система выявления недекларированных возможностей программного обеспечения, влекущих нарушение конфиденциальности информации тема диссертации и автореферата по ВАК РФ 05.13.19, кандидат технических наук Леошкевич, Илья Олегович

• Леошкевич, Илья Олегович
• кандидат технических наук
• 2011

Оглавление диссертации кандидат технических наук Леошкевич, Илья Олегович

Введение

Глава 1. Задача выявления НДВ.

1.1. Методы статического анализа.

1.1.1. Поиск потенциально онасных конструкций

1.1.2. Проверка формальных ¡моделей.

1.1.3. Абстрактная интерпретация.

1.1.4. Анализ потоков данных.

1.2. Методы динамического анализа.

1.2.1. Контроль поведения.

1.2.2. Инструментальное оснащение.

1.3. Гибридные методы

1.4. Методы анализа исполняемого кода.

1.4.1. Дизассемблирование.

1.4.2. Существующие внутренние представления.

1.4.3. Особенности некоторых архитектур.

1.5. Инструментарий.

1.6. Системы анализа исполняемого кода.

1.6.1. Интерактивный дизассемблер ГОА.

1.6.2. Статический анализатор Сос1е8иг!ег/х86.

1.6.3. Платформа динамического анализа Уа^ппс!.

1.6.4. Платформа для комплексного анализа ВйВ1аге.

1.6.5. Анализатор времени выполнения Вошк1Т.

1.6.6. Прочие системы анализа исполняемого кода.

1.7. Выводы.

Глава 2. Система выявления НДВ.

2.1. Модель нарушителя.

2.2. Требования к системе.

2.3. Компоненты системы.

2.3.1. Дизассемблер.

2.3.2. Анализатор потоков данных.

2.3.3. Интерфейс к системам компьютерной алгебры.

2.3.4. Статический анализатор.

2.3.5. Модуль выявления НДВ-К.

2.4. Выводы.

Глава 3. Элементы системы выявления НДВ.

3.1. Язык описания архитектур процессоров

3.1.1. Внутреннее представление.

3.1.2. Структура описания.

3.1.3. Адресные пространства

3.1.4. Выражения.

3.1.5. Правила.

3.1.6. Типы.

3.1.7. Прочее.

3.1.8. Компиляция.

3.1.9. Применение правил.

3.2. Граф потока управления.

3.3. Моделирование ввода-вывода.

3.3.1. Компоненты модели ввода-вывода.

3.3.2. Язык описания модели ввода-вывода.

3.3.3. Анализ модели ввода-вывода.

3.4. Численные домены

3.4.1. Абстрактные значения.

3.4.2. Абстрактные суммы

3.4.3. Мультисуммы.

3.4.4. Выровненные адреса.

3.4.5. Битовые поля.

3.5. Анализатор потоков данных.

3.6. Домен простых состояний

3.6.1. Состояния участков памяти.

3.6.2. Состояния программы.

3.7. Домен символьных состояний.

3.8. Символьный анализ циклов

3.9. Проверка политики обработки информации.

3.10. Выводы.

Глава 4. Применение системы выявления НДВ.

4.1. Работа с системой выявления НДВ.

4.2. Тестовые испытания.

4.3. Внедрение - ООО ИБМ Восточная Европа/Азия

4.4. Внедрение - Кафедра №42 НИЯУ МИФИ

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

Актуальность работы. Недекларпрованные возможности программного обеспечения (НДВ) определяются руководящим документом Гостехкомиссии от 4 июня 1999 года как "функциональные возможности программного обеспечения, не описанные или не соответствующие описанным в документации, при использовании которых возможно нарушение конфиденциальности, доступности или целостности обрабатываемой информации"[1]. Конфиденциальная информация определяется руководящим документом Гостехкомиссии от 30 марта 1992 года как "информация, требующая защиты"[2].

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

Закладки в программных средствах криптографической защиты информации (ПСКЗИ) могут сохранять производную от секретного ключа информацию на диск или передавать её по сети - как в виде отдельных файлов или сетевых соединений, так и их фрагментов. Эта дополнительная информация может позволить злоумышленнику существенно ускорить восстановление секретного ключа или открытого текста.

Программы во время работы обычно хранят конфиденциальную информацию в оперативной памяти в открытом виде и перезаписывают её при завершении. Если этого не происходит, то злоумышленник, получив после сеанса работы пользователя физический доступ к ЭВМ, может сделать снимок физической памяти или физических дисков и получить остаточную информацию. Проблема усугубляется тем, что в последние годы стала возможной эффективная реализация атаки "холодного старта" [3], в результате которой снимок памяти может быть получен в течение нескольких минут после выключения ЭВМ.

Необходимость выявления НДВ-К обусловлена тем, что во многих современных операционных системах предполагается корректность программ, обрабатывающих конфиденциальную информацию от имени пользователя. Это допущение отсутствует в системах, работающих по модели Белла-Лапа-дула^], где выполняется свойство "звезды" - процессы с более высоким уровнем конфиденциальности не могут писать в области с более низким уровнем конфиденциальности. Хотя реализации модели Белла-Ланадула для современных операционных систем существуют, зачастую они не используются, в том числе из соображений удобства.

Задачи исчерпывающего анализа поведения программного кода в общем случае алгоритмически неразрешимы, что следует из результата, полученного Аланом Тьюрингом в 1936 году[5]; задача выявления НДВ-К не является исключением. Кроме того, даже для частных случаев, важных на практике, её решение связано с рядом сложностей. Во-первых, зависимость какой-либо информации от конфиденциальной не очевидна, и во многих случаях может быть отслежена лишь по длинной цепочке присваиваний и преобразований, вытекающей из применения нетривиальных структур данных и алгоритмов. Во-вторых, факт сохранения такой информации может быть скрыг на уровне исходного кода - например, даже если разработчик принял меры по её перезаписи, компилятор на фазе оптимизации может удалить код очистки как неиспользуемый. В-третьих, НДВ-К может активироваться только при определённых и явно не выраженных в коде условиях.

Проблемой выявления НДВ-К в последнее десятилетие занималось множество исследователей, из которых особо можно выделить Nicholas Nethercote (автора утилиты Valgrind)[6], Dawn Song (университет Беркли) [7], Jim Chow (Стэнфордский университет) [8], и Вартана Падаряна (Институт системного программирования РАН) [9]. Ими спроектированы и разработаны средства динамического анализа, позволяющие отслеживать зависимости между обрабатываемыми работающей программой данными, и таким образом позволяющие обнаруживать в ней НДВ-К. Однако, они не позволяют доказать отсутствие НДВ-К, так как с их помощью невозможно исследовать поведение программы при всех возможных входных данных.

Автором данной работы предлагается новая система статического анализа, предназначенная для выявления НДВ-К и работающая на уровне исполняемого кода. Статический анализ предоставляет больше возможностей по рассмотрению всех путей выполнения программы, нежели динамический, а работа на уровне исполняемого кода повышает точность за счёт того, что он является конечным результатом процесса сборки и не подлежит изменениям перед выполнением на ЭВМ конечного пользователя. Применение такой системы позволит существенно ускорить и уменьшить затраты на выявление НДВ-К.

Объектом исследования диссертационной работы является исполняемый код программного обеспечения.

Предметом исследования диссертационной работы являются НДВ, влекущие нарушение конфиденциальности информации.

Целью диссертационной работы является выявление НДВ, влекущих нарушение конфиденциальности информации.

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

• анализ существующих методов выявления НДВ, влекущих нарушение конфиденциальности информации;

• анализ существующих методов верификации исполняемого кода;

• синтез архитектуры системы выявления НДВ, влекущих нарушение конфиденциальности информации;

• синтез алгоритма построения формальной модели программного обеспечения по его исполняемому коду;

• реализация системы выявления НДВ, влекущих нарушение конфиденциальности информации.

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

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

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

• построены два абстрактных домена для представления адресов, позволяющие анализировать низкоуровневые идиомы работы с указателями, основывающиеся па побитовых операциях;

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

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

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

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

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

• построенные численные абстрактные домены: домен выровненных адресов, позволяющий точно учитывать результаты операции выравнивания указателей, и домен битовых нолей, позволяющий описывать работу с адресами, в неиспользуемые биты которых помещена дополнительная информация;

• построенные домены абстрактных состояний: домен простых состояний, позволяющий эффективно проводить различные виды анализа потоков данных, и домен символьных состояний, позволяющий точно описывать поведение участков кода;

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

Внедрение результатов работы. Результаты работы используются в ООО ИБМ Восточная Европа/Азия при разработке программного обеспечения, а также в учебном процессе кафедры №42 "Криптология и дискретная математика" Национального исследовательского ядерного университета «МИФИ».

Публикации и апробация работы. Основные положения диссертации изложены в 8 публикациях, 4 из которых в изданиях, включенных в Перечень ведущих рецензируемых изданий. Результаты работы докладывались и получили одобрения на следующих конференциях:

• XV Всероссийская научная конференция. Проблемы информационной безопасности в системе высшей школы. 2008;

• XVII Всероссийская научная конференция. Проблемы информационной безопасности в системе высшей школы. 2010;

• 12-й Национальный форум информационной безопасности. Информационная безопасность России в условиях глобального информационного общества. 2010;

• VII межрегиональная научно-техническая конференция студентов и аспирантов. Применение кибернетических методов в решении проблем общества XXI века. 2010;

• Научная сессия МИФИ. 2010.

Структура и объем диссертации. Диссертация состоит из введения, обзора литературы, 4 глав, заключения и библиографии из 101 позиции. Общий объем диссертации составляет 155 страниц, включая 11 рисунков и 8 таблиц.

Заключение диссертации по теме «Методы и системы защиты информации, информационная безопасность», Леошкевич, Илья Олегович

3.10. Выводы

В данной главе подробно рассмотрены принципы функционирования разработанной системы выявления НДВ-К.

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

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

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

Глава 4

Применение системы выявления НДВ 4.1. Работа с системой выявления НДВ

С точки зрения пользователя система состоит из двух основных компонентов - анализатора и программы для просмотра результатов. Вызов анализатора имеет следующий вид: fa --module <имя-файла> [--ext <расширения>] [--arg <аргументы загрузчика>]

Опции имеют следующее значение:

• -module - имя модуля. Поддерживаются модули в форматах raw (без заголовка), РЕ и zmod.

• -ext - набор расширений для дизассемблера. Политика обработки информации должна быть реализована как расширение.

• -arg - аргументы для загрузчика модуля. Для загрузчика формата zmod это базовый адрес каждого сегмента и содержимое некоторых полей PSW.

Поверхностный отчёт о ходе работы системы, включающий в себя наименование проводимой в данный момент фазы анализа и её результаты, печатается на стандартный вывод. Более подробная информация - граф потока управления и отчёт о возможности наличия НДВ-К, помещается в директорию, имя которой совпадает с именем модуля. Граф потока управления можно просмотреть с помощью графической утилиты vis, реализованной на языке С# с использованием библиотеки Microsoft Automatic Graph Layout, реализующей алгоритм визуализации графов Сугиямы [96]. Отчёт представляет собой текстовый файл, содержащий адреса инструкций, предположительно реализующих НДВ-К.

4.2. Тестовые испытания

Были подвергнуты анализу 64 тестовые программы, из которых:

• Группа А, 47 программ: имеют небольшой размер и служат для проверки корректности анализа распространённых конструкций;

• Группа Б, 17 программ: реализуют различные вариации НДВ-К.

Для группы А целью являлось получение полной формальной модели безотносительно наличия или отсутствия в них НДВ-К. Результат использования разработанной систему представлен в таблице 4.1.

Для группы Б целью являлось успешное выявление НДВ-К. Программы в группе Б также имеют небольшой размер и реализуют следующие виды НДВ-К:

• Наличие остаточной информации, напрямую зависящей от конфиденциальной, в локальной переменной;

• Остаточная информация, зависящая от конфиденциальной по управлению;

• Остаточная информация, зависящая от конфиденциальной по адресу;

• Сохранение конфиденциальной информации через двойное разымено-вывание;

• Неполная или отсутствующая очистка динамической копии конфиденциального массива;

• Остаточная информация в полях классов.

Система успешно выявила все НДВ-К, реализованные в программах группы Б.

Наименование Кол-во Время анализа инструкций (сек.) addesp 27 8 alias 1 25 8 and esp 23 7 ascendingloop 26 8 bad loop 1 26 8 bsf obx eax 27 8 bubble 28 8 cmp addjmp 26 8 dead flags 23 7 defl 28 7 demand 1 22 8 dcscend i ng loop post ,jnz 25 8 descend ing loop pre j 1 24 7 fmode 2820 309 fuzz 371 58 gen 2041 236 if-1 995 128 infeasible 23 7 keyfileO 578 88 linear 25 7 livel 658 75 loops 5962 835 malloc 150 22 mallocl 967 121 maychangel 184 30 memory counter 25 7 misc 896 96 ofn 158 28 overwrite static 23 8 proc 589 73 rdtsc 27 8 repstosd 23 7 sample4 3872 483 sample5 2354 247 sample6 4260 488 selfmodifyingl 28 9 selfmodifying2 23 7 simpleloop 26 8 smloop 24 8 strlen 25 8 two counters 24 8 uncertain fill 150 26 unreachable loop 23 8 unsigned ascending loop 30 9 unsigned descending loop 23 7 xorl 24 7 zero tricks 27 7

Заключение

В работе рассмотрена актуальная задача' выявления разновидности недекларированных возможностей программного обеспечения, влекущих нарушение конфиденциальности информации - НДВ-К, связанной со случайным или умышленным внедрением в программный код логики, нарушающей жизненный цикл конфиденциальной информации. Наличие НДВ-К может привести к компрометации систем, использующих для защиты информации надёжных алгоритмов и протоколов. Предложен метод выявления НДВ-К с помощью статического анализа исполняемого кода программного обеспечения.

Проанализировано более 20 существующих средств выявления НДВ и анализа исполняемого кода; на основании анализа сделаны следующие выводы:

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

2. Выявление НДВ-К необходимо проводить на уровне исполняемого кода программного обеспечения;

3. Существующие средства статического анализа исполняемого кода не обладают функционалом по выявлению НДВ-К;

4. Существующие средства статического анализа исполняемого кода не могут быть использованы в качестве основы системы выявления НДВ-К.

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

НДВ-К относительно политики обработки информации. К системе предъявлен ряд требований, из которых можно выделить универсальность - поддержку различных целевых процессоров и операционных систем, и возможность анализа всех путей выполнения программного обеспечения. Основным принципом работы системы является продвижение меток конфиденциальности: информация, зависящая от конфиденциальной также является конфиденциальной, если только политика обработки информации не утверждает обратного; все возможные источники конфиденциальная информация и допустимые приёмники конфиденциальной информации описываются политикой её обработки; любое отклонение является признаком наличия НДВ-К.

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

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

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

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

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

Практичекую значимость результатов работы определяет успешный опыт использования системы в ООО ИБМ Восточная Европа/Азия для проверки фрагментов кода диагностических компонентов базовой контрольной программы операционной системы z/OS, а также в учебном процессе кафедры №42 "Криптология и дискретная математика" Национального исследовательского ядерного университета «МИФИ» в рамках курсов "Информатика" и "Защита программного обеспечения".

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

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

• построенные численные абстрактные домены: домен выровненных адресов, позволяющий точно учитывать результаты операции выравнивания указателей, и домен битовых полей, позволяющий описывать работу с адресами, в неиспользуемые биты которых помещена дополнительная информация;

• построенные домены абстрактных состояний: домен простых состояний, позволяющий эффективно проводить различные виды анализа потоков данных, и домен символьных состояний, позволяющий точно описывать поведение участков кода;

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

Список литературы диссертационного исследования кандидат технических наук Леошкевич, Илья Олегович, 2011 год

1. Гостехкомиссия. Руководящий документ. Защита от несанкционированного доступа к информации. Часть 1. Программное обеспечение средств защиты информации. Классификация по уровню контроля отсутствия иедекларированных возможностей / 1999.

2. Гостехкомиссия. Руководящий документ. Защита от несанкционированного доступа к информации. Термины и определения / 1992.

3. Halderman, J. Alex. Lest We Remember: Cold Boot Attacks on Encryption Keys / J. Alex Halderman // Proceedings of the USENIX Security Symposium — 2008. — pp. 45-60.

4. Bell, D. Eliott. Secure Computer Systems: Mathematical Foundations. Tech. rep. №2547. 1973.

5. Turing, Alan. On computable numbers, with an application to the Entscheidungsproblem / Alan Turing // Proceedings of the London Mathematical Society — 1936. — №42. — pp. 230-265.

6. Nethercote, Nicholas. Dynamic Binary Analysis and Instrumentation. PhD thesis. University of Cambridge, 2004.

7. Song, Dawn. BitBlaze: A New Approach to Computer Security via Binary Analysis / Dawn Song // ICISS — 2008.

8. Chow, Jim. Understanding Data Lifetime via Whole System Simulation / Jim Chow — 2004.

9. Падарян, В.А. Программная среда для динамического анализа бинарного кода / В.А. Падарян, А.И. Гетьман, М.А. Соловьев // Труды Института системного программирования РАН — 2009.

10. Evans, David. Improving Security Using Extensible Lightweight Static Analysis / David Evans, David Larochelle // IEEE Software — 2002.

11. Hovemeyer, David. Finding bugs is easy / David Hovemeyer, William Pugh // Object-Oriented Programming, Systems, Languages and Applications — 2004. — pp. 92-106.

12. JetBrains. Nullable How-To URL: http : / /www . jetbrains . com/ idea/documentation/howto.html.

13. Clarke, Edmund. Predicate Abstraction of ANSI-C Programs using SAT / Edmund Clarke // Formal Methods in System Design — 2004.pp. 105-127.

14. Cytron, R. An Efficient Method of Computing Static Single Assignment Form / R. Cytron // POPL — 1989. — pp. 25-35.

15. Rushby, John. SMT Solvers: A Disruptive Technology. http://fm. cs.uiuc.edu/talks/060406/slides.pdf. 2006.

16. Cousot, Patrick. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints / Patrick Cousot, Radhia Cousot // POPL — 1977. — pp. 238-252.

17. Cousot, Patrick. Refining Model Checking by Abstract Interpretation / Patrick Cousot, Radhia Cousot // Automated Software Engineering1999. — №1. — pp. 69-95.

18. Ope, О. Теория графов (второе издание). Москва: Наука, 1980.

19. Cousot, Patrick. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation / Patrick Cousot, Radhia Cousot // Programming Language Implementation and Logic Programming — 1992. — pp. 269-295.

20. Schmidt, David A. Data flow analysis is model checking of abstract interpretations / David A. Schmidt — 1998. -— p. 11.

21. Mit, Michael Ernst. Static and Dynamic Analysis: Synergy and Duality / Michael Ernst Mit, Michael D. Ernst — 2003. — pp. 2427.

22. Clarke, Edmund. Counterexample-Guided Abstraction Refinement / Edmund Clarke // CAV — 2000. — pp. 154-169.

23. Sen, Koushik. CUTE and jCUTE: Concolic unit testing and explicit path mo del-checking tools / Koushik Sen, Gul Agha — 2006. — pp. 419423.

24. Ball, Thomas. The SLAM project: debugging system software via static analysis / Thomas Ball, Sriram K. Rajamani // Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages — 2002.

25. Beyer, Dirk. The Software Model Checker Blast: Applications to Software Engineering / Dirk Beyer // STTT — 2007. — pp. 505-525.

26. Ball, T. SLAM2: Static Driver Verification with Under 4% False Alarms / T. Ball // Formal Methods in Computer Aided Design — 2010.

27. Gulwani, Sumit. Bound Analysis using Backward Symbolic Execution. Tech. rep. 2009.

28. Moura, Leonardo. Z3: An Efficient SMT Solver / Leonardo Moura, Nikolaj Bj0rner // Conference on Tools and Algorithms for the Construction and Analysis of Systems — 2008.

29. Beckman, Nels. Proofs, from Tests / Nels Beckman // MSR-TR — 2008.

30. Lai, Akash. MCDASH: Refinement-Based Property Verification for Machine Code / Akash Lai, Junghee Lim, Thomas Reps — 2009.

31. Intel. Intel 64 and IA-32 Architectures Software Developer's Manual Volume 2A: Instruction Set Reference, A-M.

32. Guilfanov, Ilfak. Decompilers and beyond / Ilfak Guilfanov — 2008.

33. Valgrind Source Code URL: http://valgrind.org/downloads/ current.html.

34. Dullien, Thomas. REIL: A platform-independent intermediate representation of disassembled code for static code analysis. Tech. rep. Zynamics, 2009.

35. Lim, Junghee. A system for generating static analyzers for machine instructions / Junghee Lim, Thomas Reps // CC —■ 2008.

36. Ramsey, Norman. Specifying Instructions' Semantics Using Lambda-RTL / Norman Ramsey, Jack Davidson — 1999.

37. Cai, Hongxu. Certified Self-Modifying Code / Hongxu Cai, Zhong Shao, Alexander Vaynberg // YALEU/DCS/TR — 2010.

38. Appel, Andrew W. A semantic model of types and machine instructions for proof-carrying code / Andrew W. Appel, Amy P. Felty // POPL — 2000.

39. Neophytos, Michael G. Machine Instruction Syntax and Semantics in Higher Order Logic / Michael G. Neophytos, Andrew W. Appel // TR — 2000.

40. Ray, Sandip. Towards a Formalization of the X86 Instruction Set Architecture / Sandip Ray — 2008.

41. Rogers, Ian. Static Single Assignment / Ian Rogers.

42. Tu, Peng. Gated SSA-based demand-driven symbolic analysis for parallelizing compilers / Peng Tu, David Pradua // ICS — 1995. — pp. 414-423.

43. Dijkstra, Edsger. Guarded commands, nondeterminacy and formal derivation of programs / Edsger Dijkstra // Communications of the ACM — 1975. — №8. — pp. 453-457.

44. Holzmann, Gerard J. The SPIN MODEL CHECKER: Primer and Reference Manual. Addison-Wesley.

45. ЦБИ. Анализатор исходных текстов "АИСТ-С" URL: http: //www. cb i-inf о.ru/group s/page-343.htm.

46. ЦБИ. Программа исследования программного обеспечения "EMU" -URL: http://www.cbi-info.ru/groups/page-342.htm.

47. Газинформсервис. IRIDA контроль и защита потоков управления в исполняемых кодах программ - URL: http://bit-info.com/GAZ-IS/irida.

48. БНТИ. Анализатор механизма очистки оперативной памяти "НКВД 2.5" URL: http://www.bnti.ru/des.asp?itm=2244.

49. Balakrishnan, Gogul. WYSINWYX: What You See Is Not What You eXecute. PhD thesis. University of Wisconsin-Madison, 2007.

50. Nethercote, Nicholas. How to Shadow Every Byte of Memory Used by a Program / Nicholas Nethercote, Julian Seward // VEE — 2007. — pp. 65-74.

51. Holsti, Niklas. Computing Time as a Program Variable: A Way Around Infeasible Paths / Niklas Holsti // WCET — 2008.

52. Holsti, Niklas. Analysing Switch-Case Tables by Partial Evaluation / Niklas Holsti // WCET — 2007.

53. Pugh, William. Counting Solutions to Presburger Formulas: How and Why. Tech. rep. University of Maryland, 1993.54. lpsolve — URL: http://lpsolve.sourceforge.net/.

54. Kinder, Johannes. Jakstab: A Static Analysis Platform for Binaries / Johannes Kinder, Helmut Veith // CAV — 2008. — pp. 423-427.

55. Kinder, Johannes. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries / Johannes Kinder, Helmut Veith, Florian Zuleger // VMCAI — 2009. — pp. 214-228.

56. Kinder, Johannes. Static Analysis of x86 Executables. PhD thesis. 2010.

57. Wang, Tielei. IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution / Tielei Wang — 2008.

58. GiNaC is Not a CAS URL: http: //www. ginac. de/.

59. Dullien, Thomas. Platform-independent static binary code analysis using a meta-assembly language / Thomas Dullien, Sebastian Porst // CSW — 2009.

60. Sharif, Monirul. Eureka: A Framework for Enabling Static Malware Analysis / Monirul Sharif // ESORICS — 2008. — pp. 481-500.

61. Vanegue, Julien. Next Generation Debuggers for Reverse Engineering / Julien Vanegue // BHEU — 2007.

62. Durden, Tyler. Automated vulnerability auditing in machine code / Tyler Durden // Phrack — 2007.

63. Visser, W. Model Checking Programs / W. Visser // ASE — 2003.№2.

64. Allen, Matthew. Slicing Multi-threaded Java Programs: A Case Study / Matthew Allen, Susan Horwitz // PPoPP — 2003. — pp. 44-54.

65. Shumow, Daniel. Side Channel Leakage Profiling in Software / Daniel Shumow, Peter L. Montgomery — 2010.

66. Common Weaknesses Enumeration url: http: //ewe.mitre. org/.

67. Eset. Tlireat Encyclopaedia Win32/Induc.A - URL: http://www. eset. eu/ encyclopaedia/win32-induc-a-virus.

68. Меньшов, B.C. Применение низкоуровневого исследования программного обеспечения на наличие недекл.арируемых возможностей / B.C. Меньшов, В.Н. Липовенко // Информационное противодействие угрозам терроризма — 2008. — С. 187-195.

69. Nicholson, Andy. 64-bit programming in a 32-bit world: writing-portable code for 16-, 32-, and 64-bit architectures / Andy Nicholson // Dr. Dobb's Journal — 1993.

70. Ахо, А. Компиляторы, принципы, технологии и инструментарий, 2-е изд. Москва: Вильяме, 2008.

71. Laviron, Vincent. Refining Abstract Interpretation-Based Static Analyses with Hints / Vincent Laviron, Francesco Logozzo // LNCS — 2009. — pp. 343-358.

72. Cooper, Keith D. A Simple, Fast Dominance Algorithm / Keith D. Cooper, Timothy J. Harvey, Ken Kennedy — 2001.

73. Schwartzbach, Michael. Lecture Notes on Static Analysis / Michael Schwartzbach — 2008.

74. Cousot, Patrick. Static Determination of Dynamic Properties of Programs / Patrick Cousot, Radhia Cousot // Proceedings of the Second International Symposium on Programming — 1976. — pp. 106-130.

75. Cousot, Patrick. Automatic discovery of linear restraints among variables of a program / Patrick Cousot, Nicolas Halbwachs — 1978. — pp. 84-97.

76. Mine, A. The Octagon Abstract Domain / A. Mine // Higher-Order and Symbolic Computation — 2006. — pp. 31-100.

77. Logozzo, Francesco. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses / Francesco Logozzo, Manuel Fahndrich // SAC — 2008. — pp. 184-188.

78. Sotin, Pascal. Quantifying the Precision of Numerical Abstract Domains / Pascal Sotin — 2010.

79. Balakrishnan, Gogul. Analyzing Memory Accesses in x86 Executables / Gogul Balakrishnan, Thomas Reps // CC — 2004. — pp. 5-23.

80. Reps, Thomas. Static Program Analysis via 3-Valued Logic / Thomas Reps // LNCS — 2002.

81. Warren, Henry S. Hacker's Delight. Addison-Wesley Professional, 2003, p. 320.

82. Tarjan, Robert. Depth-first search and linear graph algorithms / Robert Tarjan // Switching and Automata Theory — 1971. — pp. 114121.

83. Muchnick, Steven S. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997.

84. Yorsh, Greta. Generating precise and concise procedure summaries / Greta Yorsh, Eran Yahav, Satish Chandra // POPL — 2008. — pp. 221-234.

85. Fahringer, Thomas. Advanced Symbolic Analysis for Compilers / Thomas Fahringer, Bernhard Scholz // LNCS — 2003.

86. Sinha, Nishant. Symbolic program analysis using term rewriting and generalization / Nishant Sinha // FMCAD — 2008.

87. Wies, Thomas. Verifying Complex Properties using Symbolic Shape Analysis / Thomas Wies // Workshop on Heap Abstraction and Verification — 2006.

88. Kovacs, Laura. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover / Laura Kovacs, Andrei Voronkov // FASE — 2009.

89. Dijkstra, Edsger W. A Discipline of Programming. Upper Saddle River, NJ, USA: Prentice Hall PTR, 1997, p. 240.

90. Carette, Jacques. Program Verification by Calculating Relations / Jacques Carette, Ryszard Janicki, Yun Zhai // Applied Simulation and Modeling — 2006.

91. Balakrishnan, Gogul. Refining the control structure of loops using static analysis / Gogul Balakrishnan — 2009. — pp. 49-58.

92. GNU Linear Programming Kit URL: http: //www. gnu. org/software/ glpk/.

93. Parametric Integer Programming URL: http://piplib.org/.

94. Scholz, Bernhard. User-input dependence analysis via graph reachability / Bernhard Scholz, Chenyi Zhang, Cristina Cifuentes — 2008.

95. Sugiyama, Kozo. Methods for Visual Understanding of Hierarchical System Structures / Kozo Sugiyama, Shojiro Tagawa, Mitsuliiko Toda // IEEE Transactions on Systems, Man, and Cybernetics — 1981. — pp. 109-125.

96. IBM. z/Architecture Principles of Operation, 8th Edition / 2009.

97. Anckaert, Bertrand. A model for self-modifying code / Bertrand Anckaert, Matias Madou, Koen De Bosschere // Proceedings of the 8th international conference on Information hiding — 2006.

98. Schmitz, Karl. z/OS System Integrity: Authorized Software without Security Holes / Karl Schmitz // SHARE — 2003.

99. Беззубцев, И.О. Материалы курса "Информатика" / И.О. Беззубцев, И.О. Леошкевич, О.С. Варламов.101. orz online judge URL: https://code.google.eom/p/orzoj/.