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

• Станкевичус, Алексей Алексеевич
• кандидат технических наук
• 2009

Оглавление диссертации кандидат технических наук Станкевичус, Алексей Алексеевич

Введение.

1 Анализ возможностей защиты СРВ от вредоносного кода выполняемого задания.

1.1 Анализ особенностей СРВ с точки зрения защиты от вредоносного кода выполняемого задания.

1.1.1 Виды СРВ.

1.1.2 Особенности вычислительных заданий вычислительных СРВ

1.1.3 Современные средства организации вычислений в СРВ.

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

1.2.1 Виртуализация.

1.2.2 Безопасные языки.

1.2.3 Формальная верификация.

1.2.4 Другие частные случаи.

1.3 Выводы.

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

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

2.2 Методика защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания.

2.3 Модель безопасной ячейки памяти.

2.4 Построение алгоритма выявления потенциально вредоносного программного обеспечения.

2.5 Алгоритмы системы мониторинга.

2.6 Преобразование ПО в форму, для которой возможно доказательство безопасности.

2.7 Выбор абстракций данных.

2.8 Построение защиты диспетчера СРВ от атак типа, «отказ в обслуживании».

2.9 Выводы.

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

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

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

3.3 Функциональная модель системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания.

3.4 Безопасная библиотека.

3.4.1 Общая архитектура безопасной библиотеки.

3.4.2 Монитор обращений.

3.5 Модуль преобразования исходного кода.

3.6 Верификатор вызовов.

3.7 Верификатор обращений к памяти.

3.8 Политика безопасности.

3.9 Настройки системы.

3.10 Интерфейс разработчика программного обеспечения.

3.11 Выводы.

4 Реализация системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания.

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

4.1.1 Язык реализации верификатора.

4.1.2 Язык реализации пользовательского интерфейса.

4.1.3 Выбор препроцессора Си.

4.1.4 Реализация лексического анализатора.

4.1.5 Реализация синтаксического анализатора.

4.2 Структуры данных.

4.3 Тестирование системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания.

4.3.1 Модульное тестирование.

4.3.2 Системное тестирование.

4.4 Оценка производительности системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания.

4.4.1 Оценка производительности статического верификатора.

4.4.2 Оценка производительности защищенного кода.

4.5 Выводы.

5 Внедрение системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания.

5.1 Использование предложенной системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания для обеспечения безопасности данных, составляющих коммерческую тайну в АОЗТ «Виланд».

5.2 Применение предложенной системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания для обеспечения безопасности СРВ кафедры «Криптология и дискретная математика» МИФИ.

5.3 Выводы.

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

В настоящее время существует множество задач, для решения которых необходимы вычислительные мощности, недоступные в рамках отдельных компьютерных центров. Для решения таких задач были разработаны гетерогенные среды распределенных вычислений. Гетерогенная среда распределенных вычислений (далее СРВ) представляет собой географически распределенную инфраструктуру, в состав которой входит множество разнотипных ресурсов (таких как запоминающие устройства и процессоры, базы данных и сети) доступ к которым обеспечивается пользователю независимо от месторасположения пользователя и этих ресурсов. Для обозначения гетерогенной среды распределенных вычислений часто используется термин «Грид», образованный от английского Grid (решетка, сетка), при этом подчеркивается аналогия с сетью электропитания -подразумевается, что получать доступ к ресурсам гетерогенной среды распределенных вычислений почти так же легко и удобно, необходимо только «вставить штепсель в розетку». Одно из определений термина Грид [1-3] дано Я. Фостером и К. Кессельманом: "Грид - согласованная, открытая и стандартизованная среда, которая обеспечивает гибкое, безопасное, скоординированное разделение ресурсов в рамках виртуальной организации" [1]. "Грид предполагает коллективный разделяемый режим доступа к ресурсам и к связанным с ними услугам в рамках глобально распределенных виртуальных организаций, состоящих из предприятий и отдельных специалистов, совместно использующих общие ресурсы. В каждой виртуальной организации имеется своя собственная политика поведения ее участников, которые должны соблюдать установленные правила. Виртуальная организация может образовываться динамически и иметь ограниченное время существования." [4]

Европейский Центр Ядерных Исследований (ЦЕРН) [5]. одним из первых начал использовать технологию Грид. Грид был необходим для обработки данных, поступающих от крупнейшего в мире ускорителя заряженных частиц — Большого

Адронного Коллайдера (Large Hardon Collider, LHC) [6]. В настоящее время СРВ используются для решения множества задач по самым разным фундаментальным и прикладным направлениям - в физике высоких энергий и космофизике, микробиологии и медицине, метеорологии, самолетостроении и целом ряде других областей.

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

В СРВ можно выделить следующие действующие лица:

- пользователь вычислительного задания;

- производитель вычислительного задания;

- владелец ресурса СРВ;

- владелец диспетчера СРВ;

- производитель промежуточного ПО СРВ.

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

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

Защита от вредоносного кода может быть реализована путем применения:

- технологий виртуализации;

- безопасных языков программирования;

- верификации исполнимого кода;

- верификации исходного кода.

Во многих используемых системах применяются именно технологии виртуализации. К сожалению, это, как правило, ведет к существенному падению производительности [7] вычислительных ресурсов СРВ, либо налагает дополнительные требования на среду выполнения и аппаратное обеспечение этих ресурсов. Кроме того, безопасность многих виртуальных машин не имеет строгого доказательства, и в различных виртуальных машинах периодически выявляются уязвимости, способные повлечь исполнение произвольного кода на реальной машине [8; 9].

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

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

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

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

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

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

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

Язык программирования Си является широко распространенным, существуют компиляторы этого языка для практически любой платформы, кроме того, производительность программ на языке Си во многих случаях превышает производительность аналогичных программ на других языках программирования, что делает этот язык удобным для разработки вычислительных заданий СРВ. Однако, этот язык не является типобезопасным и в общем случае корректность для программ на этом языке на данный момент доказать не удается, что часто является следствием высокой производительности. Таким образом, существует необходимость в доказательстве безопасности исходного кода вычислительного задания для СРВ на языке Си.

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

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

Направления исследований:

1. Поиск путей повышения уровня защищенности ресурсов СРВ от вредоносного кода на основе анализа состояния вопросов теории и практики защиты СРВ, современных тенденций развития.

2. Систематизация способов защиты от вредоносного кода, оценка их эффективности.

3. Развитие теоретических положений по защите СРВ от вредоносного программного обеспечения.

4. Поиск и разработка новых решений в области защиты СРВ от вредоносного кода на основе известных теоретических положений и новых методов защиты.

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

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

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

11

- построение модели нарушителя и анализ угроз;

- разработка методики защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания;

- разработка алгоритма проверки безопасности кода программ;

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

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

На защиту выносятся:

- результаты анализа методов защиты гетерогенной среды распределенных вычислений от вредоносного кода;

- построенная модель нарушителя и сформулированный перечень угроз;

- алгоритм проверки безопасности исходного кода программ;

- методика защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания;

- архитектура системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания;

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

Заключение диссертации по теме «Методы и системы защиты информации, информационная безопасность», Станкевичус, Алексей Алексеевич

5.3 Выводы

1. Опытный образец системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания на языке Си применен для обеспечения защиты от вредоносного кода вычислительного задания узлов СРВ АОЗТ «Виланд», что позволило компании без закупки дополнительного оборудования повысить производительность вычислений приблизительно на 310%.

2. Опытный образец системы защиты гетерогенной среды распределенных вычислений от вредоносного кода выполняемого задания на языке Си применен для обеспечения защиты от вредоносного кода вычислительного задания узлов СРВ кафедры «Криптология и дискретная математика» МИФИ, что позволило обеспечить безопасность применения СРВ в образовательной и научно-исследовательской деятельности, требующей исполнения программного обеспечения, разработанного студентами, аспирантами и сотрудниками Кафедры, в том числе и выполнения студентами лабораторных работ по дисциплине «Криптографические методы защиты информации».

Заключение

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

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

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

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

4. Предложен алгоритм проверки безопасности кода программ.

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

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

7. Разработанное программное обеспечение применено для защиты данных, составляющих коммерческую тайну в АОЗТ «Виланд» и для защиты гетерогенной среды распределенных вычислений, объединяющей ЭВМ кафедры «Криптология и дискретная математика» НИЯУ МИФИ от вредоносного кода вычислительных заданий.

Список литературы диссертационного исследования кандидат технических наук Станкевичус, Алексей Алексеевич, 2009 год

1. Foster I., Kesselman С. The Grid. Blueprint for a new computing infrastructure. -Morgan Kaufman, 1998.

2. Foster I. What is the Grid? A Three Point Checklist Электронный ресурс. -2002. http://www-ip.mcs.anl.gov/~foster/Articles/WhatIsTheGrid.pdf.

3. Foster I., Kesselman C., Tuecke St. The Anatomy of the Grid: Enabling Scalable Virtual Organizations Электронный ресурс. — http://www.globus.org/alliance/ publications/papers/anatomy .pdf.

4. GridClub Электронный ресурс. http://www.gridclub.ru.

5. CERN. Электронный ресурс. http://www.cern.ch.

6. LHC Электронный ресурс. http://lhc.web.cern.ch.

7. MacKinnon Ch. A. Server Virtualization Performance. Love The Benefits, But Beware The Pitfalls Электронный ресурс. // Processor. 2007. - Vol.29, Issue 31.-http://www.processor.com/editorial/article.asp?article=articles/P2931/3 lp31/31рЗ 1 .asp.

8. VMware Fusion 2 Release Notes Электронный ресурс. -http://www.vmware.com/support/fusion2/doc/releasenotesfusion204.html/.

9. Microsoft Security Bulletin MS02-052. Flaw in Microsoft VM JDBC Classes Could Allow Code Execution (Q329077) Электронный ресурс. -http://www.microsoft.com/technet/security/bulletin/MS02-052.mspx.

10. Distributed European Infrastructure for Supercomputing Applications. Электронный ресурс. http://www.deisa.eu/

11. Chien A., Calder В., Elbert S., Bhatia K. Entropia: Architecture and Performance of an Enterprise Desktop Grid System // Journal of Parallel Distributed Computing. -2003.-pp. 597-610.

12. Calder В., Chien A., Wang J., Yang D. The Entropia Virtual Machine for Desktop Grids . Электронный ресурс. http://www-cse.ucsd.edu/ Dienst/ UI/ 2.0/ Print/ ncstrl.ucsdcse/ CS2003-0773, 2003.

13. Entropia PC Grid Computing Электронный ресурс. -http://www.entropia.com/.

14. Parabon's Frontier Grid Platform Электронный ресурс. -http://www.parabon.com/.

15. Голуб В.А., Овчинникова М.В. Проблема корректного определения термина «вредоносная программа» // Вестник Воронежского государственного университета. 2008. - №1. - С. 138-141.

16. Разумов С.А. и др. Комментарий к УК РФ / отв. ред. Лебедев В. М. 3-е изд., доп. и испр.— М.: Юрайт-Издат, 2004. — 223 с.

17. Касперский Е.В. Компьютерные вирусы: что это такое и как с ними бороться. М.: СК Пресс, 1998. - 288 с.

18. Крылов В.В. Информационные компьютерные преступления. М.: Издательская группа ИНФРА.М-НОРМА, 1997. - 285 с.

19. Chakrabarti A. Grid Computing Security. Springer, 2007. - 332 p.

20. Virtual Machine Technology Overview Электронный ресурс. -http://support.citrix.com/article/ CTX107587.

21. Самойленко А. Виртуализация для бизнеса Электронный ресурс. -http://www.vmworld.ru/.

22. Thinstall, Application Virtualization: A Technical Overview of the Thinstall Application Virtualization Solution Электронный ресурс. www.creekpointe.com/ helpdesk/pdf7Tb installApplicVirtualization.pdf.130

23. Altiris. Электронный ресурс. http://www.altiris.com/Support/ Documentation.aspx.

24. AppZero. Электронный ресурс. http://www.appzero.com/content/what-appzero.

25. App-V. Электронный ресурс. http://www.microsoft.com/systemcenter/ appv/default.mspx.

26. Potzl H. Linux-VServer technology Электронный ресурс. 2004. -http://linux-vserver.org/Linux-VServer-Paper.

27. SWsoft. Virtuozzo for windows & Linux server virtualization Электронный ресурс. http://www.virtuozzo.com/en/products/virtuozzo/.

28. OpenVZ Электронный ресурс. http://wiki.openvz.org/.

29. Sun Microsystems. Sun Blueprint: Solaris Containers Technology Architecture Guide Электронный ресурс. 2006. - http://www.sun.eom/blueprints/0506/819-6186.pdf.

30. Jails: Confining the omnipotent root Электронный ресурс. -http://phk.freebsd.dk/pubs/sane2000-jail.pdf.

31. Ермаков A.B., Никитин К.Е. Использование паравиртуального монитора XEN в Грид-сайте ИПМ : препринт ИПМ им. М.В.Келдыша РАН. М., 2008:

32. Stockinger Н. Defining the Grid: A Snapshot on the Current View // The Journal of Supercomputing. Springer, 2006. - V. 42, N. 1. - pp. 3-17.

33. Foster I., Tuecke St. Enterprise Distributed Computing // ACM Queue. ACM, 2005. - Vol.3, No. 6. - pp. 26-29.

34. VMware Products Электронный ресурс. http://www.vmware.com/ products/.

35. Virtualiron Электронный ресурс. http://www.virtualiron.com/.

36. Microsoft Virtual PC Электронный ресурс. http://www.microsoft.com/ windows/products/winfamily/ virtualpc/defaultmspx.

37. VirtualBox Электронный ресурс., -http://www.virtualbox.org/.

38. Bochs. Электронный ресурс. — http://bochs.sourceforge.net/.

39. PearPC Электронный ресурс.-http://pearpc.sourceforge.net/.

40. QEMU Электронный ресурс., -http://www.nongnu.org/qemu/qemu-doc.html.

41. HerculesEmulator Электронный ресурс. http://www.hercules-390.org/.

42. Фергюсон Н., Шнайер Б. Практическая криптография. — М.: Издательский дом Вильяме, 2005. 424с.

43. Bruce К. В. Foundations of Object-Oriented Languages: Types and Semantics. -The MIT Press, 2002. 404 p.

44. Liberty J. Visual C# 2005: A Developer's Notebook. O'Reilly Media, Inc., 2005.-239p.

45. Saraswat V. Java is not type-safe Электронный ресурс. -http://www.cis.upenn.edu/~bcpierce/ courses/629/papers/Saraswat-javabug.html.

46. Necula G. C., McPeak S., Weimer W. CCured: type-safe retrofitting of legacy code // Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM, 2002. - pp. 128-139.

47. Merrill Br., Drayton P., Albahari B. C# Essentials, 2nd Edition. O'Relly, 2002. -216 p.

48. Barnes J., High Integrity Software: The SPARK Approach to Safety and Security. Boston, MA: Addison-Wesley Longman Publishing Co., Inc, 2003. - 448 p.

49. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. / пер. с англ. ; под ред. Р. Смелянского. М.: МЦНМО, 2002. - 416 е.: ил.

50. Cousot P. Abstract interpretation based formal methods and future challenges. Informatics, 10 Years Back 10 Years Ahead // Lecture Notes in Computer Science 2000. - Springer, 2001. - pp. 138-156.

51. Necula G. Proof carrying code // Principles of Programming Languages. ACM, 1997.-pp. 106-119.

52. Necula G., Lee P. The design and implementation of a certifying compiler // Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation. New York: ACM, 1998. - pp. 333 - 344.

53. Клименко B.B. Мобильный код: классификация, технологии, архитектуры и области применения // Информационное противодействие угрозам терроризма— 2005.-№3.-С. 109-111.

54. Sekar R., Ramakrishnan C.R., Ramakrishnan I.V., Smolka S.A. Model-Carrying Code (MCC): A New Paradigm for Mobile-Code Security // Proceedings of the 2001 workshop on New security paradigms. New York: ACM, 2001. - pp. 23-30.

55. Robinson A., Voronkov A. Handbook of Automated Reasoning. The MIT Press, 2001.-996 p.

56. Hamlen K. Security policy enforcement by automated program-rewriting. Doctor of Philosophy. Ithaca, NY, USA: Cornell University, 2006. - 201 p.

57. Hamlen K. W., de Oliveira A. S. Rewriting-Based Access Control Policies // Electronic Notes in Theoretical Computer Science (ENTCS). Amsterdam, The Netherlands: Elsevier Science Publishers В. V., 2007. - V. 171 , I. 4. - pp. 59-72.

58. ГОСТ 19781-83. Вычислительная техника. Терминология: Справочное пособие. / рецензент канд. техн. наук Ю. П. Селиванов. — М.: Издательство стандартов, Выпуск 1. 1989. - 168 с.

59. Dahn Ch., Mancoridis Sp. Using Program Transformation to Secure С Programs Against Buffer Overflows // Proceedings of the 10th Working Conference on Reverse Engineering. Washington, DC, USA: IEEE Computer Society, 2003. - p. 323.

60. Prasad M., Chiueh Т. A Binary Rewriting Defense against Stack based Buffer Overflow Attacks // Usenix Annual Technical Conference, General Track. June 2003.

61. Corbett J. C., Dwyer M. В., Hatcliff J., Laubach S., Pasareanu C. S., Robby, Zheng H. Bandera: Extracting finite-state models from Java source code // Proc. of the 22nd Int. Conf. on Software Eng., June 2000. Programs. John Wiley & Sons, 1999.

62. Naumovich G., Avrunin G.S., Clarke L.A. Data flow analysis for checking properties of concurrent java programs // Proceedings of the 21st international conference on Software engineering. New York, NY, USA: ACM, 1999. - pp. 399 - 410.

63. Bull J. M., Smith L. A., Pottage L., Freeman R. Benchmarking Java against С and Fortran for Scientific Applications // Proceedings of the 2001 joint ACM-ISCOPE conference on Java Grande. New York, NY, USA: ACM, 2001. - pp. 97 - 105.

64. Chaki S., Clarke E., Grace A. Modular Verification of Software Components in С // IEEE Transactions on Software Engineering. Piscataway, NJ, USA: IEEE Press, 2004. - V. 30 , I. 6. - pp. 388 - 402.

65. Valgrind Электронный ресурс. http://valgrind.org/.

66. Poly Space Embedded Software Verification Электронный ресурс. -http://www.mathworks.com/ products/polyspace/index.html.

67. Safer C: The toolset Электронный ресурс. http://www.oakcomp.co.uk/ SCT.html.

68. The ASTREE Static Analyzer Электронный ресурс. -http://www.astree.ens.fr/.

69. Litzkow M.J., Livny M., Mutka M.W. Condor A hunter of idle workstations // Proceedings of the Eighth International Conference on Distributed Computing Systems (ICDCS). - Washington, DC: IEEE Computer Society, 1988. - pp. 104-111.

70. Miller B.P., Christodorescu M., Iverson R., Kosar Т., Mirgorodskii A., Popovici F. Playing inside the black box: using dynamic instrumentation to create security holes // Parallel Process. Lett. 11 (2,3). 2001. - pp. 267-280.

71. Bharadwaj R. SOL: A verifiable synchronous language for reactive systems // Electronic Notes in Theoretical Computer Science. 2002. - V. 65,1. 5. - pp. 140-154.

72. Непомнящий В. А. и др. На пути к верификации С-программ. Часть 1. Язык C-Light: препр. РАН. Сиб. Отд-ние. ИСИ; N 87. Новосибирск, 2001.

73. Непомнящий В. А. и др. На пути к верификации С-программ. Часть 2. Язык C-Light-Kernel и его аксиоматическая семантика : препр. РАН. Сиб. Отд-ние. ИСИ; N 87. Новосибирск, 2001.

74. Cowan С., Wagle P., Ри С., Beattie S., Walpole J. Buffer Overflows: Attacks and Defenses for the Vulnerability of the Decade // DARPA Information Survivability Conference and Exposition. January 2000. - pp. 119-129.

75. Xu J., Kalbarczyk Zb., Patel S., Iyer R. K. Architecture Support for Defending Against Buffer Overflow Attacks // Proc. 2nd Workshop Evaluating and Architecting System Dependability (EASY 02). 2002.

76. Vendicator. Stack Shield technical info file v0.7. Электронный ресурс. -2001. -http://www.angelfire.com/ sk/stackshield/.

77. Piromsopa Kr., Enbody R. J. Secure Bit21: Transparent, Hardware Buffer-Overflow Protection // IEEE Transactions on Dependable and Secure Computing. Los Alamitos, CA, USA: IEEE Computer Society Press, 2006. - V. 3 , I. 4. - pp. 365-376.

78. Grevstad E. CPU-Based Security: The NX Bit Электронный ресурс. 2004. - http://hardware.earthweb.com/ chips/article.php/3358421.

79. Berger E. D., Zorn B. G. DieHard: Probabilistic Memory Safety for Unsafe Languages // ACM SIGPLAN Notices. New York, NY, USA: ACM, 2006. - V. 41 , 1.6.-pp. 158-168.

80. Mirkovic J., Reiher P., A taxonomy of DDoS attack and DDoS defense mechanisms // ACM SIGCOMM Computer Communication Review. ACM, 2004. -V.34 N.2. — pp. 39-53.

81. Song Sh., Chen M. C. Y.,, Zhou R., Lou X. GridSec: Trusted Grid Computing with Security Binding and Self-defense Against Network Worms and DDoS Attacks // Computational Science ICCS 2005.-Springer Berlin/Heidelberg, 2005. -pp. 187-195.

82. Mirkovic J., Reiher P. D-WARD: A Source-End Defense Against Flooding Denial-of-Service Attacks // IEEE Transactions on Dependable and Secure Computing. Los Alamitos, CA, USA: IEEE Computer Society Press, 2005. - V. 2 , I. 3. - pp. 216 - 232.

83. Mirkovic J., Prier Gr., Reiher P. Attacking DDoS at the Source // Proceedings of the 10th IEEE International Conference on Network Protocols. Washington, DC, USA: IEEE Computer Society, 2002. - pp. 312 - 321.

84. Wu J., Cheng D., Zhao W. Detecting Grid-Abuse Attacks by Source-based Monitoring // Proceedings of the ISCA 17th International Conference on Parallel and Distributed Computing Systems. 2004. - pp. 565-571.

85. Mirkovic J., Prier Gr., Reiher P. Source-End DDoS Defense // Proceedings of the Second IEEE International Symposium on Network Computing and Applications. -Washington, DC, USA: IEEE Computer Society, 2003. p. 171.

86. Chen Y., Hwang K., Kwok Y.-K. Collaborative Defense against Periodic Shrew DDoS Attacks in Frequency Domain // ACM Transactions on Information and SystemSecurity (TISSEC). ACM, 2005.

87. Chen Y., Hwang K. Collaborative Change Detection of DDoS Attacks on Community and ISP Networks // Proceedings of the International Symposium on Collaborative Technologies and Systems. Washington, DC, USA: IEEE Computer Society, 2006. - pp. 401 - 410.

88. Федеральный закон Российской Федерации от 10 января 2002 г. N 1-ФЗ ОБ ЭЛЕКТРОННОЙ ЦИФРОВОЙ ПОДПИСИ.

89. National Research Council. Realizing the Information Future: The Internet and Beyond. National Academy Press Электронный ресурс. 1994. - http://www.nap.edu/ readingroom/books/rtif/.

90. Руководящий документ. КОНЦЕПЦИЯ ЗАЩИТЫ СРЕДСТВ ВЫЧИСЛИТЕЛЬНОЙ ТЕХНИКИ И АВТОМАТИЗИРОВАННЫХ СИСТЕМ ОТ НЕСАНКЦИОНИРОВАННОГО ДОСТУПА К ИНФОРМАЦИИ

91. Jones N.D. Abstract Interpretation: a- Semantics-Based Tool for Program Analysis // Handbook of logic in computer science. Oxford, UK: Oxford University Press, 1995. - vol. 4 : semantic modeling. — pp. 527 - 636.

92. Naur P. Checking of Operand Types in ALGOL Compilers // BIT Numerical Mathematics. Springer Netherlands, 1965. - V. 5, N. 3. - pp. 151-163.

93. Reynolds J. Automatic Computation of Data Set Definitions // Information Processing 68. North-Holland: Elsevier Science Publisher, 1969. - pp. 456-461.

94. Sintzoff M. Calculating Properties of Programs by Valuations t on Specific Models // Proceedings ACM Conference on Proving Assertions about Programs. ACM, 1972.-pp. 203-207.

95. Hecht M. S. Flow Analysis of Computer Programs. Elsevier Science Ltd,1977.

96. Aho A. V., Sethi R., Ullman J.D. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986. - 1009 p.

97. Kam J.B., Ullman J.D. Monotone Data Flow Analysis Frameworks // Acta informatica. Springer Berlin / Heidelberg, 1977. - V. 7, N. 3. - pp. 305-317.

98. Cousot P., Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints // Conf. Ree. 4th ACM Symp. on Principles of Prog. Lang., POPL '77. ACM, 1977. - pp. 238-252.

99. Нариньяни A.C. Недоопределенность в- системах представления и обработки знаний // Изв. АН СССР. Техн. кибернетика. 1986. - №5. - С. 3-28.

100. Нариньяни A.C. и др. Программирование в ограничениях и недоопределенные модели // Информационные технологии. 1998. - № 7. - С. 13— 22.

101. Корнеенко В.П. Методы оптимизации : учебник. М.: Высш. шк., 2007. — 664 е.: ил.

102. Marriott К., Stuckey P. J. Programming with constraints: an introduction. -Cambridge, Massachussets: The MIT Press, 1998. 483 p.

103. Cousot P., Cousot R. On Abstraction in Software Verification // Computer Aided Verification. Springer Berlin / Heidelberg, 2002. - pp. 1-21.

104. Miné A. Weakly Relational Numerical Abstract Domains. PhD thesis, École Polytechnique, Palaiseau, France (2004) Электронный ресурс. 2004. -http://www.di.ens.fr/mine/these/.

105. Cousot P., Cousot R Static determination of dynamic properties of Programs // ISOP'76. Dunod, Paris, France. Электронный ресурс. http://www.di.ens.fr/~cousot/ COUSOTpapers/ISOP76.shtml, 1976.-pp. 106-130.

106. Левин В. И. Интервальная математика и изучение неопределенных систем // Интеллектуальные системы. 2005. - №5.

107. Mine A. Symbolic Methods to Enhance the Precision of Numerical Abstract Domains // 7th Int. Conf. on Verification, Model Checking and Abstract Interpretation VMCAI '06, LNCS 3855. Springer, 2006. - pp. 348-363.

108. Cousot P., Halbwachs N. Automatic discovery of linear restraints among variables of a program // ACM POPL'78. New York, USA: ACM, 1978. - pp. 84-96.

109. Chen L., Mine A., Cousot P. A Sound Floating-Point Polyhedra Abstract Domain // Programming Languages and Systems. Springer Berlin / Heidelberg, 2008. -pp. 3-18.

110. Claris'o R., Cortadella J. The Octahedron Abstract Domain // SAS'04. -Springer, 2004. Vol. 3148 of LNCS. - pp. 312-327.

111. Mine A. The Octagon Abstract Domain // Higher-Order and Symbolic Computation. Hingham, MA, USA: Kluwer Academic Publishers, 2006. - V. 19,1. 1. -pp. 31-100.

112. Feret J. The Arithmetic-Geometric Progression Abstract Domain // Proceedings of VMCAI'05. Springer, 2005. - Vol. 3385 of LNCS. - pp. 2-18.

113. IDEF0 Overview Электронный ресурс. -http://www.idef.com/IDEF0.html.

114. INTERNATIONAL STANDARD ISO/IEC 9899:1999 TECHNICAL CORRIGENDUM 3 Электронный ресурс. Published 2007-11-15. -http://www.iso.org/iso/isocatalogue/cataloguetc/cataloguedetail.htm?csnumber=50510.

115. Rationale for International Standard Programming Languages— С Revision 5.10. Электронный ресурс. - 2003. - http://www.open-std.org/JTCl/ SC22/WG14/ www/docs/ C99RationaleV5.10.pdf.

116. Standard ECMA-334 C# Language Specification 4th edition (June 2006) Электронный ресурс. 2006. - http://www.ecma-international.org/publications/ standards/Ecma-334.htm.

117. Арчер Т. Основы С#: Новейшие технологии / пер. с англ. и под ред. В.Г. Вшивцева; гл. ред. А.И. Козлов. М.: Издательско-торговый дом "Русская Редакция", 2001. - 421 е.: ил.

118. Мсрр a portable С preprocessor with Validation Suite Электронный ресурс. - http://mcpp.sourceforge.net/.

119. Flex: The Fast Lexical Analyzer Электронный ресурс. -http://flex.sourceforge.net/.

120. Bison GNU parser generator. Электронный ресурс. -http://www.gnu.org/software/bison/.

121. Просиз Дж. Программирование для Microsoft .NET / пер. с англ. М.: Издательско-торговый дом "Русская редакция", 2003. — 704 е.: ил.

122. MSDN: Windows.Forms reference documentation Электронный ресурс. -http://msdn.microsoft.com/ en-us/library/dd30h2yb.aspx.

123. Mono project Электронный ресурс. http://www.mono-project.com/.

124. Gosling J., Joy В., Guy S., Bracha G. The Java Language Specification. Second Edition Электронный ресурс. 2000. - http://java.sun.com/docs/books/jls/ secondedition/html/j.title.doc.html.

125. Котляров В.П. Основы тестирования программного обеспечения. М.: Интернет-университет информационных технологий. — ИНТУИТ.ру, 2006. - 288 с.