Электронная библиотека диссертаций и авторефератов России
dslib.net
Библиотека диссертаций
Навигация
Каталог диссертаций России
Англоязычные диссертации
Диссертации бесплатно
Предстоящие защиты
Рецензии на автореферат
Отчисления авторам
Мой кабинет
Заказы: забрать, оплатить
Мой личный счет
Мой профиль
Мой авторский профиль
Подписки на рассылки



расширенный поиск

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

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

Диссертация - 480 руб., доставка 10 минут, круглосуточно, без выходных и праздников

Автореферат - бесплатно, доставка 10 минут, круглосуточно, без выходных и праздников

Леошкевич, Илья Олегович. Система выявления недекларированных возможностей программного обеспечения, влекущих нарушение конфиденциальности информации : диссертация ... кандидата технических наук : 05.13.19 / Леошкевич Илья Олегович; [Место защиты: Нац. исслед. ядерный ун-т].- Москва, 2011.- 154 с.: ил. РГБ ОД, 61 11-5/2861

Содержание к диссертации

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1.6.1. Интерактивный дизассемблер IDA 28

1.6.2. Статический анализатор CodeSurfer/x86 29

1.6.3. Платформа динамического анализа Valgrind 33

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

1.6.5. Анализатор времени выполнения BoundT 34

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

1.7. Выводы 38

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

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

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

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

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

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

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

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

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

2.4. Выводы 63

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

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

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

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

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

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

3.1.5. Правила 70

3.1.6. Типы 73

3.1.7. Прочее 74

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.10. Выводы 130

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

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

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

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

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

Заключение 143

Список литературы 146

Введение к работе

Актуальность работы. Обеспечение конфиденциальности информации является одной из важнейших задач в сфере информационной безопасности. Действующий стандарт ГОСТ Р ИСО/МЭК 17799-2005 определяет конфиденциальность как "обеспечение доступа к информации только авторизованным пользователям" . Серьёзным источником угрозы конфиденциальности информации является наличие в обрабатывающем её программном обеспечении недекларированных возможностей (НДВ), которые определяются руководящим документом Гостехкомиссии от 4 июня 1999 года как "функциональные возможности программного обеспечения, не описанные или не соответствующие описанным в документации, при использовании которых возможно нарушение конфиденциальности, доступности или целостности обрабатываемой информации".

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

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

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

Проблемой выявления НДВ-К в последнее десятилетие занималось множество исследователей, из которых особо можно выделить Nicholas Nethercote

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В основе поиска потенциально опасных конструкций лежит предположение, что определённые последовательности операций в коде практически всегда влекут нежелательные последствия. Впервые этот метод был использован в 1979 году в утилите lint, проверявшей исходные коды на языке С и поставлявшейся с операционной системой UNIX V7. На данный момент существует множество подобных утилит для различных языков, таких как splint [10] (С), cppcheck {C++), FindBugs [11] (Java), Perl:-.Critic (Perl) и PEP8 (Python). Такая функциональность также присутствует во многих компиляторах и средах разработки, выводящих помимо сообщений об ошибках предупреждения и информационные сообщения.

Естественным приёмом поиска потенциально опасных конструкций является сигнатурный анализ, который позволяет выявить нарушения принятого стиля и рекомендаций по написанию кода. В качестве примеров обнаруживаемых сигнатурным анализом ошибок можно привести нарушение рекомендаций по реализации operator= в языке C++, который должен проверять на присваивание объекта самому себе и возвращать ссылку на объект, которому было присвоено значение, или использование метода wait () в языке Java вне цикла. Утилиты, использующие сигнатурный поиск, обладают высоким быстродействием, что позволяет без существенных затрат интегрировать их в процессы разработки и непрерывного тестирования.

Зачастую совместно с сигнатурным анализом используется анализ потоков данных, который будет рассматриваться ниже. Отметим лишь, что из-за повышенных требований к производительности, обусловленных сферой применения рассматриваемых утилит, используется "легковесный" анализ - зачастую локальный, контекстно-нечувствительный и отслеживающий лишь очень специфические свойства. Разработчикам может предлагаться возможность давать подсказки таким анализаторам потоков данных путём размещения в коде аннотаций. В качестве примера можно привести проверки на возможность наличия разыменовывания нулевых указателей в Java [12], где отслеживаемым для каждого указателя свойством является возможность равенства его null, а пользователь может задавать аннотации вида ONullable и @NotNull.

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

SAT-системы (satisfability) позволяют установить истинность логической формулы или найти аргументы, при которых она становится ложной (так называемый контрпример). В качестве примера использующего SAT решения можно привести анализатор программ на языке Си SATABS [13], поддерживающий помимо прочего работу со структурами и указателями. Не останавливаясь на прочих деталях, отметим, что SATABS получает описывающие программу логические формулы в несколько этапов: сначала программа переводится в SSA [14], затем все базовые блоки преобразуются в логические утверждения над переменными программы (представляющие собой коньюнкции. утверждений, получаемых из каждого присваивания в составе базового блока), и, наконец, выбираются предикаты, переменными, отражающими истинность которых, замещаются подвыражения в утверждениях.

SMT-системы (satisfabiliiy modulo theory), такие как STP и Yices, позволяют устанавливать истинность утверждений над поддерживаемыми конкретной SMT-системой теориями, такими как арифметика Пресбургера. Многие SMT-задачи могут быть выражены через SAT, например, целые числа можно кодировать битовыми векторами, а арифметические операции над числами выражать через логические операции над составляющими их битами. SMT-системы, специализирующиеся па целых числах, решают соответствующие задачи быстрее, чем обобщённые SAT-системы, но главным преимуществом SMT-систем являются принципиально меньшие ограничения на размер решаемых задач [15]. Системы доказательства теорем (Isabelle, Coq) позволяют устанавливать истинность утверждений в задаваемых пользователем теориях. Абстрактная интерпретация (abstract interpretation) [16, 17] представляет собой метод анализа систем переходов (transition systems) с потенциально бесконечным количеством возможных состояний. Система переходов состоит из множества состояний S, отношения перехода t С S х S, а также множеств начальных /С5и конечных F С S состояний. Образ множества состояний определяется как postt[P] = {s \3s : s Є Р A (s,s ) Є t]. Целью анализа систем переходов является проверка их свойств; типичным примером являются свойства безопасности, гласящие, что система должна находиться только в безопасных состояниях Р: posty[I] С Р, то есть, за любое число переходов из любого начального состояния система может перейти только в одно из безопасных состояний.

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

IDA (Interactive DisAssembler) представляет собой визуальную среду для анализа исполняемого кода. IDA изначально разрабатывался компанией Datarescue, а теперь HexRays. Основной функционал IDA заключается в статическом анализе, хотя стоит отметить, что него встроен и отладчик. IDA строит листинг программы, выделяет процедуры и их параметры, строит графы потока управления и вызовов, разрешает вызовы внешних функций. IDA является коммерческим продуктом, его исходный код закрыт. Пробная версия доступна на официальном сайте http: //www. hex-rays. com/idapro/.

Поддержка различных архитектур в IDA осуществляется модулями процессоров. Они экспортируют функцию ana О, отвечающую за дизассемблиро-вание команд данной архитектуры. Для построения графа потока управления экспортируется функция emu(), которая для данной инструкции определяет, на какие адреса она может передать управление. Таким образом, описание инструкций произвольных архитектур в IDA ограничивается жёстко задан ными рамками, определёнными задачей построения листинга. IDA поддерживает более 50 видов различных процессоров. В IDA нет функционала для проверки свойств программного обеспечения, однако, он может быть добавлен с помощью модулей-расширений. IDA может служить базой для создания систем верификации, поскольку предоставляет возможности по визуализации результатов. Кроме того, его алгоритмы дизассемблирования, хоть и построены на эвристиках и не работают корректно в общем случае, могут для большинства реальных программ построить приемлемый граф потока управления, который может служить отправной точкой для анализа.

Система статического анализа исполняемого кода для архитектуры х86 CodeSurfer/x86 [49], реализованная как модуль расширения для IDA, разработана в университете Висконсин-Мэдисон. В ходе анализа проводится уточнение графа: восстанавливаются переменные, вычисляются их возможные значения и зависимости между ними, разрешаются косвенные переходы. CodeSurfer/x86 является закрытым исследовательским проектом: исходный и исполняемый код не распространяются.

CodeSurfer/x86 предполагает, что анализируемый исполняемый файл подчиняется стандартной .модели компиляции: в нём могут использоваться глобальные переменные и нсмодифицируемый код, имеющие фиксированные адреса, процедуры, имеющие фиксированную структуру стекового фрейма, а также функции динамического выделения памяти и произвольные внешние библиотеки в формате DLL. В случае обнаружения возможности отклонения от такой модели CodeSurfer/x86 выдаёт предупреждение и продолжает анализ так, как будто отклонения не существует. Это полезно в случаях, когда возможности отклонений являются ложными срабатываниями - например, CodeSurfer/x86 может сделать вывод, что цикл заполнения массива может перезаписать адрес возврата, поскольку возможные значения индекса при записи в этот массив не могут быть достоверно определены из-за его сложности.

CodeSurfer/x86 представляет оперативную память как набор регионов. Регионы - это непересекающиеся участки памяти с заранее неизвестными адресами. Регионы служат для описания глобальной памяти, стека и фрагментов кучи. Регионы создаются и уничтожаются но мере необходимости: в точках входа и выхода из программы, при вызовах и возвратах из процедур, а также при выделении и освобождении памяти. Например, с каждой процедурой связывается свой стековый регион, моделирующий её локальные переменные. Внутри регионов содержатся абстрактные ячейки (abstract locations), представляющие переменные, имеющие фиксированные размер и смещение. Изначально множество абстрактных ячеек строится с помощью "наивного" алгоритма, ориентированного на типовые операции обращения к памяти: например, из наличия в процедуре команды mov еах, [ebp-OxlO] может быть сделан вывод о наличии абстрактной ячейки размера 4 байта по смещению -16 в её стековом фрейме. Кроме того, все регистры считаются абстрактными ячейками. Затем в ходе анализа множество абстрактных ячеек уточняется.

Анализ численных значений и указателей CodeSurfer/x86 проводит одновременно. В основе этого процесса лежат абстрактные адреса, представляющие собой пары (регион Ь смещение). Если регион глобальный, то абстрактный адрес представляет собой либо адрес абстрактной ячейки в нём, либо численное значение. В противном случае абстрактный адрес представляет собой адрес абстрактной ячейки в соответствующем регионе. Смещения представляются в виде интервалов с шагом (strided intervals) - значений вида s[l,u] — {i\l і и,і = l(mod s)}, где s - шаг, I - нижняя граница, и - верхняя граница. Использование интервалов с шагом помогает более точно представлять обращения к элементам массивов. Наконец, возможные значения (value sets) представляют собой множества абстрактных адресов, а более точно - отображения из множества регионов в множество интервалов с шагом. Возможные значения позволяют отслеживать значения переменных, которые могут указывать на более чем один регион. CodeSurfer/x86 проводит анализ именно с помощью возможных значений.

Абстрактные состояния представляют собой соответствия возможных значений абстрактным ячейкам. Абстрактные состояния в близких друг к ДРУГУ точках программы отличаются незначительно; CodeSurfer/x86 использует этот сракт для оптимизации объёма занимаемой памяти с помощью совместного использования общих частей состояний. Для этого вводится отношение полного порядка на множестве абстрактных ячеек и для их храпения создаются неизменяемые балансированные деревья. При добавлении или удалении вершины создаётся повое дерево, в котором от оригинального отличаются лишь logn вершин; сам процесс занимает 0{1одп) времени, где п - количество вершин в дереве. Оставшиеся п — log п вершин являются общими и не требуют дополнительной памяти.

Вершины графа потока управления представляют собой дизассемблиро-ванные инструкции архитектуры х86. Кроме того, в графе всегда присутствуют две дополнительные вершины "вход" и "выход". Рёбра помечаются инструкцией, соответствующей вершине-источнику. За счёт этого с ними связываются абстрактные преобразования входных абстрактных состояний в выходные. Когда инструкция представляет собой условный переход, ребро помечается условием, при котором по нему происходит переход. Так как в архитектуре х86 условный переход осуществляется с помощью пар инструкций стр и j ее, сначала ищется предшествующая инструкция стр, и условие генерируется исходя из её операндов. Кроме того, для некоторых форм инструкций применяются специальные преобразования. Например, в общем виде инструкция хог производит побитовое сложение своих операндов по модулю 2, однако, в случае, когда они одинаковы, она рассматривается как обнуление.

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

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

Работа на уровне исполняемого кода. Обнаружение некоторых НДВ-К на уровне исходного кода невозможно, например, в случае проведения компилятором нежелательной оптимизации (уязвимость CWE-14) или его компрометации (вирус Win32/Induc.A [68]). Так как исполняемый код является "последней инстанцией" и выполняется непосредственно на ЭВМ конечного пользователя, его анализ позволяет получить более точные данные о поведении программы, чем анализ исходных текстов. При работе на уровне исполняемого кода не требуется явно поддерживать множество языков программирования, их диалектов и, в случае многоязыковых программ, их комбинаций и интерфейсов между ними [69]. Исключениями являются чисто интерпретируемые языки; невозможность их анализа в рамках предлагаемого подхода является принципиальным ограничением. Если в программе присутствуют ассемблерные вставки, то применение методов анализа исполняемого кода является единственным способом проверки их на наличие НДВ-К.

Поддержка нескольких процессоров и операционных систем. У работы на уровне исполняемого кода есть недостаток - в отличие от исходного кода, семантика которого зачастую определена для всех возможных целевых платформ, исполняемый код специфичен для конкретного процессора. Это значит, что полученная информация об НДВ-К будет справедлива лишь для того процессора, для которого был скомпилирован анализируемый код. В настоящий момент происходит переход от архитектуры IA-32 к AMD-64; существует множество ошибок, связанных с некорректным портированием существующего программного обеспечения [70]; многие программы распространяются в вариантах для обеих архитектур. Кроме того, существует потребность и в анализе программного обеспечения, работающего на мобильных и встраиваемых устройствах (например, под управлением ARM-процессоров), а также на высокопроизводительных системах (Power, System z). Операционная система, под управлением которой работает программное обеспечение, также имеет существенное значение -нужно учитывать, какой эффект оказывают на состояние программы вызовы системных сервисов. Таким образом, система анализа должна поддерживать различные процессоры и операционные системы, а также предоставлять возможности по добавлению новых, каковой

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

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

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

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

Другие примитивы включают в себя описание ввода-вывода (io), управление метками (taint, untaint), атрибутами ячеек памяти (setAttributes) и завершение (exit). Они будут введены и более подробно описаны в следующих разделах. В следующих подразделах вводится язык описания архитектур процессоров и функций операционных систем, управляющий преобразованием машинных инструкций в микрокод.

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

Элемент address space class задаёт класс адресного пространства. Каждый класс содержит статические атрибуты, атрибуты ячеек памяти и атрибуты доступа. Значения статических атрибутов связываются с каждым адресным пространством; к ним можно обращаться во время декодирования. Например, с каждым регистровым адресным пространством можно связать номер соответствующего ему регистра. Атрибуты ячеек памяти связываются с диапазонами адресов и используются командой setAttributes. Примерами атрибутов ячеек памяти являются параметры защиты и кеширования. Наконец, атрибуты доступа связываются с каждым обращением к адресному пространству. С каждым видом атрибутов может быть связано значение по умолчанию. address space member type ::= "property" "access" ! "attribute" ; address space member ::= expression type address space member type identifier [ = expression ] ";" ; address space ::= "$" identifier "=" identifier "(" argument list ")" ";" ; Элемент address space отвечает за определение адресного пространства. При задании адресного пространства должен быть указан его класс и значения статических атрибутов.

I unary operation 1 binary operation I ternary operation I function invocation I memory reference "(" expression ")" Целочисленные константы ( integer constant ) могут задаваться в десятичном или шестнадцатеричном виде. Логические константы ( boolean constants) могут принимать значения true или false. Переменные ( variable ) представляют собой именованные сущности, хранящие выражения и использующиеся во время дизассемблирования. Параметры (parameter) также могут хранить выражения, но, в отличие от переменных, используются во время компиляции.

Обращения к памяти ( memory ref erence ) строятся из типа данных, адресного пространства, смещения и атрибутов доступа. Здесь и далее вместо конкретных нетерминалов, например, address space , в реальных описаниях могут использоваться обобщённые выражения ( expression ). Это объясняется тем, что многие значения, включая типы и адресные пространства, могут являться результатами применения встроенных функций или макросов, подстановки значений параметров времени компиляции или переменных времени выполнения. Для большей ясности здесь и далее будут использоваться нетерминалы, соответствующие тем значениям, которые должны получаться после всех таких преобразований. memory reference ::= [ type ] "[" address space identifier [ ":" expression [ ":" argument list ] ] "] "; 3.1.5. Правила Правила являются центральной частью описаний архитектур, они содержат синтаксис и семантику машинных инструкций и их полей. Правило характеризуется именем, списком параметров, опциями и телом, состоящим из набора цепочек-вариантов. Для каждой уникальной комбинации аргументов создаётся своя копия правила, в теле которой все вхождения параметров ( parameter ) заменены конкретными значениями. В списке параметров можно указать их типы. В Q действует второстепенная система типизации, отвечающая за проверку корректности выражений. В рамках этой системы определены следующие типы - целый, логический, массив, тип адресного пространства и неопределённый тип. Многие операции требуют, чтобы в них использовались значения определённых типов, например, операция сложения может быть применена лишь к целым операндам.

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

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

Условный оператор if служит двум целям: генерации микропрограммы и условному разбору. Микропрограмма генерируется по следующему правилу: сначала выполняются элементы обеих ветвей, которые генерируют соответствующие микропрограммы, затем они объединяются и дополняются микрокомандами условного перехода, служащими для проверки условия. Если условие можно вычислить во время разбора, то элементы, соответствующие недостижимым ветвям, включая даже те из них, что отвечают за разбор, игнорируются.

Оператор while служит для генерации циклической микропрограммы. Он устроен схоже с оператором if , с той разницей, что вторая генерируемая им микроинструкция перехода осуществляет прыжок назад. Оператор while нельзя использовать для реализации циклов времени разбора, требуемых для обработки некоторых сложных инструкций. Циклический разбор можно реализовать с помощью комбинации рекурсивного вызова правил и оператора if .Синтаксически похожее на присваивание связывание ( binding ) отвечает за присваивание значения переменной времени разбора и не выполняет никаких действий по генерации микрокода. Декодирование константы ( constant decoding ) - основная операция, на которой строится разбор, отвечает за извлечение значения определённого типа из входного потока (о том, что это за тип, будет сказано ниже), размер которого равен её второму операнду и сравнении его со своим первым операндом. Операции декодирования констант из различных цепочек одного правила объединяются в графы разбора. У операции декодирования константы есть две дополнительные модификации: в первом случае сравнения не происходит и значение, полученное из потока, отбрасывается, а во втором случае поток не задействован вообще, а сравнение производится с содержимым переменной. Операция декодирования переменной ( variable decoding ) позволяет получить значение заданного типа из входного потока и присвоить его переменной времени разбора.

Если все цепочки начинаются с элементов constant decoding с одинаковыми значениями var, то производится их объединение. Для этого определяется минимальная длина элемента птт, затем для значения каждого элемента г с помощью операции substr вычисляются его основной (длины Птгп) и остаточный (длины щ — nmin) фрагменты. Затем рассмотренные элементы удаляются из цепочек; если какие-либо соответствующие им отстаточные фрагменты имеют ненулевую длину, то они помещаются в начало соответствующих цепочек. Получившиеся цепочки группируются по значениям основных фрагментов, для всех цепочек в каждой группе рекурсивно вызывается рассматриваемый алгоритм. Результатом в этом случае является вершина Constant(peek,nmin,var), соединяемая рёбрами с получившимися в результате рекурсивных вызовов графами. Рёбра помечаются значениями основных фрагментов, соответствующих группам. Значение реек равно 0 за исключением особого случая, рассматриваемого ниже.

Если все цепочки начинаются с идентичных элементов е, то они удаляются, и рассматриваемый алгоритм вызывается рекурсивно для укороченных цепочек. Результатом в этом случае является вершина, соответствующая е, соединенная ребром с графом, полученным в результате рекурсивного вызова. Большинство получаемых таким образом вершин соответствуют породившим их элементам. Дополнительную обработку проходят лишь следующие элементы: 1. rule invocation Компилятор использует так называемый кеш правил, ключом в котором является имя правила и комбинация его параметров, а значением - граф, получающийся при компиляции правила с этими параметрами. Кеш нужен не только для улучшения производительности, но и для поддержки рекурсивно вызываемых правил. Перед началом компиляции правила в кеш добавляется соответствующая ему запись, состоящая лишь из вершины Null. Затем производится сама компиляция с помощью рассматриваемого алгоритма; граф, получаемый в результате, соединяется с исходной вершиной Null. Это необходимо для того, чтобы компилируемое в данный момент правило могло обратиться к самому себе. 2. if . Проводится компиляция цепочек для thenGraph и elseGraph. 3. while . Проводится компиляция цепочек для bodyGraph. Если цепочки начинаются с различных элементов, то проводятся две попытки нормализации. Первая заключается в подстановке содержимого вызовов правил, если таковые имеются в начале каких-либо цепочек и если это разрешено их свойствами. Подстановка заключается в приписывании каждой цепочки подставляемого правила к началу текущей цепочки (то есть, на место элемента rule invocation ). При этом предварительно производится разрешение параметров приписываемого правила. Вторая попытка заключается в упреждающем декодировании, необходимом в случаях, когда формат машинных инструкций подразумевает запись кода операции после операндов (например, в z/Architecture для инструкцияй AY, NY и т.д.). Компилятор связывает с каждым элементом его размер, соответствующий количеству получаемых им из потока битов (-1 в случае, если это число невозможно определить). Тогда с каждым элеметом цепочки можно связать его смещение, определяемое как сумма размеров предшествующих элементов или -1. Для упреждающего декодирования компилятор пытается обнаружить, существует ли такое смещение, по которому располагаются лишь элементы constant decoding с var = 0. Если результат положительный, то эти элементы переносятся в начало цепочек и с ними связывается атрибут реек, равный их смещению. Вместо них на старые позиции добавляются элементы skip с соответствующими удалённым элементам длинами. Если обе попытки нормализации не удаются, то есть, даже после них первые элементы цепочек различны, то компиляция завершается с ошибкой.

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