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

• Автор: Леошкевич, Илья Олегович
• Шифр специальности: 05.13.19
• Научная степень: Кандидатская
• Год защиты: 2011
• Место защиты: Москва
• Количество страниц: 154 с. : ил.

Содержание

Введение . о

Глава 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. Интерактивный дизассемблер I.
1.6.2. Статический анализатор x
1.6.3. Платформа динамического анализа Vi.
1.6.4. Платформа для комплексного анализа i
1.6.5. Анализатор времени выполнения .
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 Выводы
Глава 4. Применение системы выявления НДВ.
4.1. Работа с системой выявления НДВ.
4.2. Тестовые испытания
4.3. Внедрение ООО ИБМ Восточная ЕвроиаАзия
4.4. Внедрение Кафедра НИЯУ МИФИ
Заключение.
Список литературы


На данный момент существует множество подобных утилит для различных языков, таких как splint [| (С), cppcheck (С-Ь-ь), FindBugs 1) (Java), Perl::Oritic (Perl) и PEPS (Python). Такая функциональность также присутствует во многих компиляторах и средах разработки, выводящих помимо сообщений об ошибках предупреждения и информационные сообщения. Java вне цикла. Утилиты, использующие сигнатурный поиск, обладают высоким быстродействием, что позволяет без существенных затрат интегрировать их в процессы разработки и непрерывного тестирования. Зачастую совместно с сигнатурным анализом используется анализ потоков данных, который будет рассматриваться ниже. Отмстим лишь, что из-за повышенных требований к производительности, обусловленных сферой применения рассматриваемых утилит, используется “легковесный” анализ - зачастую локальный, контекстно-нечувствительный и отслеживающий лишь очень специфические свойства. Разработчикам может предлагаться возможность давать подсказки таким анализаторам потоков данных путём размещения в коде аннотаций. В качестве примера можно привести проверки на возможность наличия разыменовываиия нулевых указателей в Java [], где отслеживаемым для каждого указателя свойством является возможность равенства его null, а пользователь может задавать аннотации вида ONullable и @NotNull. Проверка формальных моделей (model checking) заключается в преобразовании программного кода в некоторую хорошо изученную формальную модель. Свойства, выполнимость которых требуется установить, формулируются в терминах этой модели и проверяются с помощью разработанных для неё алгоритмов. Преимуществом такого подхода является возможность использовать для решения задачи существующий математический аппарат и эффективно реализующие его инструментальные средства. Существует несколько классов систем, специализирующихся на проверю; формальных моделей, которые используются в разных областях, в том числе п для верификации. SAT-систеыы (satisfiability) позволяют установить истинность логической формулы или найти аргументы, при которых она становится ложной (так называемый контрпример). Не останавливаясь на прочих деталях, отметим, что SATABS получает описывающие программу логические формулы в несколько этапов: сначала программа переводится в SSA [), затем все базовые блоки преобразуются в логические утверждения над переменными программы (представляющие собой конъюнкции, утверждений, получаемых из каждого присваивания в составе базового блока), и, наконец, выбираются предикаты, переменными, отражающими истинность которых, замещаются подвыражения в утверждениях. SMT-системы (satisfabilily modulo theory), такие как STP и Yices, позволяют устанавливать истинность утверждений над поддерживаемыми конкретной SMT-системой теориями, такими как арифметика Преебургера. Многие SMT-задачи могут быть выражены через SAT, например, целые числа можно кодировать битовыми векторами, а арифметические операции над числами выражать через логические операции над составляющими их битами. SMT-системы, специализирующиеся на целых числах, решают соответствующие задачи быстрее, чем обобщённые SAT-систсмы, но главным преимуществом SMT-систем являются принципиально меньшие ограничения на размер решаемых задач [). Системы доказательства теорем (Isabelle, Coq) позволяют устанавливать истинность утверждений в задаваемых пользователем теориях. Абстрактная интерпретация (abstract interpretation) [, ) представляет собой метод анализа систем переходов (transition systems) с потенциально бесконечным количеством возможных состояний. Система переходов состоит из множества состояний S. С 5 х S, а также множеств начальных / С S и конечных F С S состояний. Образ множества состояний определяется как po$tt[P} = {s'|3s : s Є Р Л (s, s') Є і}. Целью анализа систем переходов является проверка их свойств; типичным примером являются свойства безопасности, гласящие, что система должна находиться только в безопасных состояниях Р: postal] С Р, то есть, за любое число переходов из любого начального состояния система может перейти только в одно из безопасных состояний.