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

На правах рутписи

Калинин Максим Олегович

АВТОМАТИЗИРОВАННЫЙ АНАЛИЗ ВЫПОЛНЕНИЯ ПРАВИЛ ПОЛИТИК БЕЗОПАСНОСТИ В ИНФОРМАЦИОННЫХ СИСТЕМАХ

Специальность:

05.13.19- Методы и системы защиты информации, информационная безопасность

Автореферат диссертации на соискание ученой степени кандидата технических наук

Санкт-Петербург — 2003

Работа выполнена в Санкт-Петербургском государственном политехническом университете

Научный руководитель:

Официальные оппоненты:

кандидат технических наук, доцент Зегжда Дмитрий Петрович

доктор технических наук, профессор Корниенко Анатолий Адамович

кандидат технических наук Сидоров Игорь Анатольевич

Ведущая организация:

Санкт-Петербургский государственный университет аэрокосмического приборостроения

Защита состоится " ЩЩ$Ь 2003 г. в часов на заседании диссертационного совета Д 212.229.27 Санкт-Петербургского государственного политехнического университета 195251, Санкт-Петербург, ул. Политехническая, 29, корп.{^, ауд. ш

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

Автореферат разослан - /Л ¡/ШЯ^ 2003 г.

Ученый секретарь

диссертационного совета _(Платонов В.В.)

А

Общая характеристика работы

Актуальность. В наши дни обеспечение безопасности информационных систем (ИС) входит в круг интересов всех участников информационного процесса. Функционирование государственных и коммерческих ИС становится невозможным без поддержания их безопасности и целостности. Прогресс в области защищенных информационных технологий сопровождается усилением требований поддержания безопасности. Однако динамика статистики нарушений свидетельствует о кризисе информационной безопасности, основными причинами которого являются недостатки проектирования и эксплуатации средств защиты. Функции ИС должны выполняться при осуществлении надлежащего контроля информации, что гарантировало бы защиту информации от нежелательного распространения, изменения или потери. Для задания политики безопасности (ПБ) потребители вынуждены использовать решения, предлагаемые производителем. Отсутствие у потребителя гарантий, кроме утверждений разраббтчиков, что в используемой системе ПБ выполняется корректно, является одной из основных причин нарушений безопасности. Эта проблема особенно остро стоит в ИС, к которым предъявляются повышенные требования гарантированности защиты: в системах управления технологическими процессами, движением транспорта, проведения банковских операций, обработки секретной информации.

Значительным шагом на пути решения указанной проблемы является разработка и применение ГОСТ Р ИСО 15408, который совместим с системой международной стандартизации и предписывает составление профиля защиты (ПЗ), включающего ПБ. Стандарт накладывает требования обеспечения гарантированности выполнения системой правил ПБ. Согласно стандарту установление гарантированности основывается на активном исследовании ИС, в результате чего должны быть выявлены причины невыполнения ПБ. Поэтому введение нового ГОСТ требует создания методов и инструментария проверки выполнения ПБ. Автоматизация анализа выполнения ПБ позволит придать ему объективный характер, обеспечить

I НОС. НАЦИОНАЛЬНАЯ БИБЛИеТЕКА

надежность защиты информации и качество сертификационных исследований.

Моделирование выполнения правил ПБ — это новое научное направление, теоретическая и методологическая базы которого в настоящее время только формируются в работах таких ученых как Грушо А.А., Расторгуев С. П., Щербаков А.Ю., Деннинг Д.Е., МакЛин Д., Сандху Р., Самарати П. Специалисты Гостехкомиссии и ее подведомственных организаций разрабатывают средства автоматизации анализа защитных свойств (например, НКВД, АИСТ). Однако упомянутые средства не решают задачу в полном объеме. Данная работа опирается на результаты указанных исследований и развивает их отдельные положения применительно к задачам моделирования защитных механизмов и автоматизации проверки выполнения правил ПБ.

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

Целью работы является обеспечение сертификационных исследований информационных систем по ГОСТ Р ИСО 15408 средствами проверки выполнения правил политик безопасности, основанными на применении метода автоматизированного анализа безопасности достижимых состояний.

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

1. Анализ моделей контроля и управления доступом (КУД), средств защиты современных ИС, а также методов моделирования ПБ.

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

3. Разработка метода проверки выполнения правил ПБ путем автоматизированного анализа безопасности достижимых состояний.

4. Разработка системы проверки выполнения правил ПБ, позволяющей автоматизировать процесс исследования ИС на предмет соблюдения ПБ.

5. Создание методики проверки выполнения правил ПБ в ходе сертификационных исследований ИС по ГОСТ Р ИСО 15408.

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

I

математической логики.

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

моделирования и исследования ПБ.

2. Предложен и обоснован подход к проверке выполнения правил ПБ путем автоматизированного анализа достижимых состояний ИС.

3. Разработаны концептуальные модели подсистем КУД для современных операционных систем (ОС).

4. Разработана форма представления системных состояний, требований модели КУД и правил ПБ в виде системы логических предикатов.

5. Предложен метод проверки выполнения правил ПБ путем анализа безопасности достижимых состояний на основе вычисления предикатов, описывающих ПБ, в контексте системных состояний и модели КУД.

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

7. Разработана методика проверки выполнения правил ПБ в ходе сертификационных исследований ИС по ГОСТ Р ИСО 15408.

Практическая ценность работы определяется возможностью использования полученных в ходе работы результатов для проведения анализа ПБ и проверки ИС на соответствие ПБ. Метод автоматизированной проверки выполнения ПБ и средство описания системных состояний, правил ПБ и требований модели безопасности использованы при разработке программ и методик сертификационных исследований специализированной ИС (акт об использовании от ЗАО "РНТ", г. Москва). Подход к проверке ПБ

путем автоматизированного анализа достижимых состояний испытываемой системы использован при разработке представления модели КУД, реализованной в системе мониторинга безопасности сложных информационных комплексов (акт об использовании от ЗАО "АРГО-Технолоджи", г. Москва). Метод автоматизированного анализа выполнения правил ГШ и разработанный комплекс средств оценки защищенности использованы при создании системы проверки выполнения ПБ организаций (акт об использовании от НИИ системотехники ХК "Ленинец", г. С.Петербург). На основе теоретических и практических результатов работы разработаны учебно-методические материалы, используемые для подготовки специалистов в области защиты вычислительных систем по дисциплинам "Теоретические основы защиты информации" и "Безопасность ОС" в СПбГУАП (акт об использовании от СПбГУАП) и СПбГПУ.

Апробация работы. Основные теоретические и практические результаты диссертационной работы доложены и обсуждены: на Российской научно-технической конференции "Методы и технические средства обеспечения безопасности информации" (СПбГПУ, 1998-2002 гг.); на Санкт-Петербургском семинаре "Информационная безопасностъ-99" (СПбГТУ, 1999 г.); на ведомственной конференции "Проблемы обеспечения информационной безопасности на федеральном железнодорожном транспорте" (Внедренческий центр ГУН "Аттестационный центр Желдоринформзащита МПС РФ", 2001 г.); на Межрегиональной конференции "Информационная безопасность регионов России" (Институт информатики и автоматизации РАН, 2001, 2002 гг.); на Российской научно-технической конференции "Проблемы информационной безопасности в системе высшей школы" (МИФИ, 2002,2003 гг.).

Публикации. По теме диссертации опубликовано 32 научные работы, в том числе 3 учебных пособия.

Основные положения, выносимые ня чяшиту

1. Обоснование подхода к проверке выполнения правил ПБ путем автоматизированного анализа безопасности достижимых состояний ИС.

2. Метод проверки выполнения правил ПБ, основанный на вычислении предикатов, описывающих системные состояния, требования модели КУД и правила ПБ. J

3. Система проверки выполнения правил ПБ.

4. Методика проверки выполнения правил ПБ на основе автоматизированного анализа безопасности состояний.

Объем и структура. Диссертация состоит из введения, четырех глав, * заключения и списка литературы из 95 наименований.

^ Содержание работы

Во введении обоснована и сформулирована задача разработки автоматизированных средств анализа выполнения правил ПБ.

В первой главе рассмотрены основные классы моделей КУД и их реализации в современных ОС, проведен анализ методов моделирования ПБ, сформулирована задача автоматизированной проверки выполнения правил ПБ с использованием логического подхода.

На основании потребительских требований, сформировавшихся на рынке информационных технологий, разработчики ИС предлагают готовые решения по обеспечению безопасности. В работе проанализированы теоретические и практические аспекты, связанные с базовыми моделями КУД, служащими основой для разработки защитных механизмов современных ИС: дискреционными и мандатными, рассмотрены реализации ' подсистем безопасности в ОС Windows 2000 и Linux. В настоящее время

наблюдается развитие моделей КУД по пути комбинирования принципов различных классических моделей безопасности. Решением проблемы проверки выполнения правил ПБ является создание концептуальной модели системы в контексте модели КУД и правил ПБ и дальнейшая ее обработка с целью выявления нарушений безопасности и противоречий. В работе осуществлен анализ методов моделирования ПБ, в результате чего выделены аналитические (AM), графовые (ГМ), объектные (ОМ) и логические (JIM) методы.

AM, имеющие в своей основе аппарат представления в виде математических функций, наиболее точны и строги, но лишены наглядности для пользователя и требуют специальной подготовки. ГМ базируются на теории графов и топологии, обладают свойством наглядности. Недостатком ГМ является статичность моделирования, т.е. демонстрация определенных состояний без указания их взаимосвязи. ОМ позволяют моделировать защищенность крупных систем, поскольку правила применяются к группам сущностей. Принципы инкапсуляции и наследования способствуют универсальности и расширяемости представления. К недостаткам ОМ следует отнести сложность объектной декомпозиции ИС и необходимость поиска оптимального уровня абстрагирования. JIM, использующие аппарат матлогики, позволяют добиться простоты реализации и проведения автоматического анализа ПБ, т.к. программа исследований может быть задана в виде логических предикатов.

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

Сравнение методов моделирования ПБ

Характеристика AM ГМ ом JIM

Выразительная способность — + — +

Моделирование иерархических структур — + + +

Объяснение результатов вывода + — — +

Программная реализация — — + +

Удобство применения — + — —

Близость к естественному языку — — — +

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

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

понятных человеку конструкций.

Анализ методов показал, что наиболее перспективным в рамках моделирования правил ПБ и автоматизации анализа проверки их выполнения является логический подход, поскольку только этот способ обладает необходимыми характеристиками.

Во второй главе рассмотрен предложенный автором подход к проверке выполнения правил ПБ путем автоматизированного анализа достижимых состояний испытываемой системы. Приведена разработанная форма представления системных состояний, правил ПБ и требований модели КУД в виде логических предикатов.

Машина состояний — распространенный инструмент моделирования различных аспектов ИС. В частности он используется при создании моделей

I

КУД, т.н. моделей безопасности состояний. К этому классу относятся модели КУД большинства ОС. Базовыми элементами таких моделей являются 1 состояния и переходы между йами. В общем случае под состоянием

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

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

операции, выполняемые с информацией. С другой стороны, сущности могут быть пассивными, т.е. являться контейнерами информации. Активные сущности назовем субъектами, пассивные — объектами. Объекты являются предметом операций, которые могут выполняться субъектами. В случае, когда субъект сам является предметом операции (например, при изменении членства в группе), над субъектом могут производиться действия, как над объектом. Субъекты и объекты обладают определенными атрибутами, которые содержат информацию, позволяющую ИС функционировать правильно. Некоторые атрибуты, например, параметры управления доступом, предназначены исключительно для осуществления ПБ. Последние назовем атрибутами безопасности. Обозначим через 5 — множество субъектов, О — множество объектов, ЗА — множество атрибутов безопасности. Тогда множество St есть декартово произведение8хОх БА.

Переход из состояния в состояние возможен как результат действий над сущностями ИС и их атрибутами. С точки зрения безопасности разрешения на операции выдаются в соответствии с требованиями, указанными в модели КУД. В ИС компонент, выполняющий разрешительные функции, называется монитором обращений, он выполняет проверку соответствия между запросом на доступ и требованиями модели. Обозначим через К требования модели КУД. При выполнении требований ИС переходит из состояния ¿1 в состояние где я!, я? е St (например, успешное создание субъекта приводит к смене состояния). Обозначим переход из состояния в состояние посредством функции переходов 5, а запрос на доступ через q, тогда последующее состояние — В общем случае, существует

последовательность пар "запрос-состояние": <(до, Ло), ..., Л*)>, которая моделирует изменения системы от начального состояния е St до некоторого состояния я?* е Л, называемого достижимым.

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

которые должны выполняться в каждом состоянии системы. Правила преобразуются в простые высказывания (ограничения С) путем применения аппарата исчисления высказываний. Например, приведенное правило преобразуется в совокупность двух ограничений: "секретарям запрещено читать файлы менеджеров" и "секретарям запрещено читать файлы директора". Тогда выполнение правил ПБ в системе, находящейся в некотором состоянии, состоит в контроле выполнения всех ограничений из множества С для этого состояния.

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

Реализация подхода включает разработку средств моделирования состояния ИС, требований модели КУД и ограничений. На основе исследования средств защиты современных ОС предложены их концептуальные модели, которые были обобщены и представлены в виде концептуального графа системных состояний, требований модели КУД и правил ПБ, на базе чего была разработана и реализована система логических предикатов, позволяющая описывать элементы и характеристики безопасности ИС по следующей форме:

атрибут_субъекта {имя__а трибу та_субъекта) . атрибут_объекта (имя_атрибута_объекта) .

субъект (имя_субъекта,имя_^атрибута субъекта! (значение_а_с1#значение_а_сл),

имя_атрибута_субъектал (значение_а_С1, ..., эначение_а_сс) ) . объект(имя_объекта,имя_атрибута_объекта1 (значение_а_01, ..., значение_а_о/),...,

имя_атрибута_объекта„(эначение_а_с>1, •■•/ значение_а_ой)) . правило (параметр_правилах, — I параметр_правилая) : - логическая_функция.

Система предикатов реализована как совокупность логических термов и правил на языке Пролог и позволяет задать субъекты, объекты ИС, их атрибуты безопасности, требования модели КУД и ограничения. В работе приведены примеры применения предложенных предикатов при описании ПБ, основанных на дискреционных, мандатных и комбинированных моделях КУД, что показало применимость предложенного подхода для моделирования широкого класса ПБ.

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

Зададим требование rule е R модели КУД в форме логического предиката rule(st, sf), определенного на декартовом произведении множеств состояний St у. St и определяющего допустимость перехода в новое состояние st'. Ограничение constraint е С зададим в форме предиката constraint(st\ определенного на множестве St и проверяющего соответствие состояния st правилам политики. В работе предлагается следующий критерий: в ИС выполняются правила ПБ, если выполняются условия:

1. constraint(sto) истинен для Vconstraint е Си stQ е St. st0— начальное состояние.

2. rule(st, sf) истинен для У rule е R и Vsf, sf е St: sf = 8 (q, st).

3. constraint(st*) истинен для Vconstraint s C, st0 e St: st0— начальное состояние и \fst*e St: st* ' b(q*, 8(... (q1, 8(qo, st0))...)).

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

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

СРмулипХ ^ Трасса V проверки^/ 4_vwiomy

Рис. 1. Модуль резолюций

Модуль реализован на платформе ОС Windows в виде динамической библиотеки с использованием ядра системы SWI-Prolog. Входные параметры MP составляют три описания, которые моделируют начальное состояние системы, требования модели КУД и ограничения. В процессе логического вывода (резолюции) MP для каждого полученного состояния обрабатывает список ограничений для проверки их выполнения. По результатам работы создается протокол анализа с трассой логического вывода.

На базе MP была разработана архитектура системы проверки (СП) выполнения правил ПБ, позволяющей автоматизировать процесс исследования ИС путем моделирования системных состояний и правил ПБ, вычисления предикатов и интерпретации результатов (рис. 2).

Заданное состояние исследуемой ИС, требования модели КУД и правила ПБ записываются посредством предложенной в работе системы предикатов. Генератор описания начального состояния предназначен для автоматического создания описания заданного состояния ИС. Правила ПБ преобразуются экспертом в ограничения, которые с помощью редактора ограничений записываются в соответствующее описание. Описание

требований модели КУД — единственное описание, требующее ручной работы эксперта на основании анализа спецификации системы, но данное описание создается один раз для заданной системы.

Рис. 2. Архитектура СП

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

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

В четвертой главе рассмотрена разработанная автором методика проверки выполнения правил ПБ на основе автоматизированного анализа безопасности состояний, приведен пример применения СП при анализе подсистемы защиты, реализованной в ОС Windows 2000.

Разработанная методика представлена на рис. 3.

Анализ трасс состояний,в Предварительный Обработка описаний которых не выполняется ПБ,

анализ средствами СП и определение причин

невыполнения

Рис. 3. Методика проверки выполнения правил ПБ

На этапе предварительного анализа выполняется определение степени детализации ИС: определяется, какие субъекты, объекты, атрибуты безопасности следует вносить в описание системных состояний. Выбирается, какие требования КУД из реализованной в системе модели безопасности следует записывать в форме предикатов и правила ПБ, по которым будет проверяться ИС. После этого формируются логические описания, которые затем обрабатываются средствами СП.

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

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

В качестве примера применения методики проведена проверка ОС Windows 2000 на предмет невыполнений ПБ, возникающих из-за некорректной реализации модели КУД данной ОС. В частности при проверке данной ОС обнаружены следующие нарушения ПБ:

• настройки безопасности имеют приоритет выше, чем права * пользователей,

• файлы можно копировать при наличии разрешения на их запуск, 1

• копирование файла может привести к смене владельца,

• пользователь из группы Power User может оперировать членствами субъектов, которых сам не создавал,

• пользователь не может удалить каталог, которым владеет.

Использование СП позволило автоматически выявить те состояния

Windows 2000, в которых из-за ошибок разработчиков ОС не выполняется ПБ, что позволило повысить гарантированность защиты информации.

Разработанную СП можно использовать как средство проверки разрешительной подсистемы ИС на предмет выполнения правил ПБ в соответствии с требованиями ГОСТ Р ИСО 15408. Применение СП •*

гарантирует выполнение функций защиты существующих и создаваемых ИС.

Макет СП и результаты, полученные при реализации проекта, неоднократно демонстрировались на различных конференциях и семинарах.

В заключении приведены результаты и выводы, полученные автором в ходе выполнения работы.

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

1.Ha основании анализа моделей КУД и методов моделирования ПБ обоснован подход к проверке выполнения правил ПБ путем логического моделирования и вычисления предикатов.

2. Разработаны концептуальные модели подсистем КУД для современных ОС и на их базе реализована система предикатов для описания

системных состояний, требований модели КУД и правил ПБ в качестве формы представления средств защиты.

3. Впервые предложен метод проверки выполнения правил ПБ на основе вычисления логических предикатов, описывающих системные состояния, требования модели КУД и правила ПБ, который закладывает основы для автоматизации сертификационных исследований по ГОСТ РИСО 15408.

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

5. Разработана система проверки выполнения правил ПБ, применяемая для автоматизированных исследований ИС.

6. Разработана методика проверки выполнения правил ПБ в хо^е сертификационных исследований ИС по ГОСТ Р ИСО 15408.

Основные результаты диссертационной работы изложены в 32 печатных трудах. Ниже приведены основные из них:

1. Калинин М.О. Язык описания политик безопасности информационных систем. // Современное машиностроение: Сб. трудов молодых ученых. Вып. 1. — СПб: Изд-во СПбИМаш, 1999. С. 69-74.

2. Зегжда Д.П., Калинин М.О. Моделирование политик безопасности для исследовательских и обучающих целей // Проблемы информационной безопасности. Компьютерные системы. 2000. №2. С. 105-111.

3. Калинин М.О. Лабораторное моделирование и исследование политик безопасности // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2000. С. 204-207.

4. Зегжда П.Д., Калинин М.О. Тестирование систем разграничения доступа, основанных на формальных политиках безопасности // Проблемы обеспечения информационной безопасности на федеральном железнодорожном транспорте: Доклады, тезисы, статьи. СПб: Изд-во СПб фил. "Внедренческий центр" ГУЛ "Атгест. центр Желдоринформзащита МПС РФ". 2001. С. 123-127.

5. Калинин М.О. Моделирование политик безопасности с применением метода графов // ИБРР-2001: Материалы конф. СПб: Политехника-сервис. 2001. Т. 1.С. 150.

6. Калинин М.О. Структура и применение языка описания политик безопасности // Проблемы информационной безопасности. Компьютерные системы. 2002. №1. С. 18-26.

7. Калинин М.О. Автоматическое доказательство защищенности систем дискреционного управления доступом // Методы и технические средства обеспечения безопасности информации: Докл. СПб: Изд-во СПбГТУ. 2002. С. 9-11.

8. Калинин М.О. Классификация методов моделирования политик безопасности // Методы и технические средства обеспечения безопасности информации: Докл. СПб: Изд-во СПбГТУ. 2002. С. 12-15.

9. Калинин М.О. Средство автоматического доказательства безопасности систем дискреционного управления доступом // ИБРР-2002: Материалы конф. СПб: Политехника-сервис. 2002. С. 144.

10. Зегжда Д.П., Калинин М.О. Оценка защищенности информационных систем // Проблемы информационной безопасности. Компьютерные системы. 2002. №3. С. 7-12.

11. Калинин М.О. Методы моделирования политик безопасности // ИБРР-2002: Материалы конф. СПб: Политехника-сервис. 2002. С. 144.

12. Зегжда Д.П., Калинин М.О. Безопасность операционных систем. Модели контроля и управления доступом: Лаб. практикум. 4.1. Дискреционные модели. СПб: Изд-во СПбГПУ, 2003. 104 с.

13. Зегжда Д.П., Калинин М.О. Безопасность операционных систем. Модели контроля и управления доступом: Лаб. практикум. 4.2. Мандатные, информационные и комбинированные модели. СПб: Изд-во СПбГПУ, 2003. 76 с.

14. Калинин М.О. Автоматический анализ состояний операционной системы Windows 2000 // Проблемы информационной безопасности. Компьютерные системы. 2003. №1. С. 4-6.

Лицензия ЛР №020593 от 07.08.97.

Подписано в печать /57 ¿>£~. <£¿>¿>3. Объем в п.л. ^ О

Тираж /СО. Заказ

Отпечатано с готового оригинал-макета, предоставленного автором, в типографии Издательства СПбГПУ 195251, Санкт-Петербург, Политехническая ул., 29.

Отпечатано на ризографе ЯЫ-2000 ЕР Поставщик оборудования — фирма "Р-ПРИНТ" Телефон: (812) 110-65-09 Факс: (812) 315-23-04

??s<¿>

§8f

ВВЕДЕНИЕ.

ГЛАВА 1. АНАЛИЗ МОДЕЛЕЙ КОНТРОЛЯ И УПРАВЛЕНИЯ ДОСТУПОМ И МЕТОДОВ МОДЕЛИРОВАНИЯ ПОЛИТИК БЕЗОПАСНОСТИ.

1.1. Основные классы моделей контроля и управления доступом.

1.1.1. Дискреционные модели контроля и управления доступом.

Модель Харрисона-Руззо-Ульмана.

1.1.2. Мандатные модели контроля и управления доступом.

Модель Белла-ЛаПадулы.

1.2. Реализация моделей контроля и управления доступом в современных операционных системах.

1.2.1. Модель контроля и управления доступом операционной системы Linux.

1.2.2. Модель контроля и управления доступом операционной системы Microsoft Windows 2000.

1.3. Методы моделирования политик безопасности.

1.3.1. Аналитические методы.

1.3.2. Графовые методы.

1.3.3. Объектные методы.

1.3.4. Логические методы.

1.3.5. Общая характеристика методов моделирования политик безопасности.

1.4. Выводы к главе.

ГЛАВА 2. ПОДХОД К ПРОВЕРКЕ ВЫПОЛНЕНИЯ ПРАВИЛ ПОЛИТИК БЕЗОПАСНОСТИ И ЕГО РЕАЛИЗАЦИЯ.

2.1. Обобщенное представление моделей контроля и управления доступом.

2.2. Правила политики безопасности.

2.3. Подход к проверке выполнения правил политик безопасности.

2.4. Инструментарий моделирования.

2.4.1. Концептуальные модели подсистем контроля и управления доступом.

2.4.2. Реализация концептуальной модели.

2.5. Применение инструментария моделирования.

2.5.1. Описание дискреционной системы.

2.5.2. Описание мандатной системы.

2.5.3. Описание комбинированной системы.

2.6. Выводы к главе.

ГЛАВА 3. СРЕДСТВА ПРОВЕРКИ ВЫПОЛНЕНИЯ

ПРАВИЛ ПОЛИТИК БЕЗОПАСНОСТИ.

3.1. Метод автоматизированного анализа выполнения правил политик безопасности.

3.2. Модуль резолюций.

3.2.1. Структура модуля.

3.2.2. Принцип анализа выполнения правил политики безопасности средствами модуля резолюций.

3.2.3. Пример использования модуля резолюций для анализа выполнения правил политик безопасности.

3.3. Система проверки выполнения правил политик безопасности.

3.3.1. Общая архитектура.

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

3.4. Выводы к главе.

ГЛАВА 4. МЕТОДИКА ПРОВЕРКИ ВЫПОЛНЕНИЯ ПРАВИЛ ПОЛИТИКИ БЕЗОПАСНОСТИ И ЕЕ ПРИМЕНЕНИЕ.

4.1. Описание методики.

4.2. Пример применения методики на базе операционной системы Microsoft Windows 2000.

4.2.1. Предварительный анализ.

4.2.2. Логические описания.

4.2.3. Анализ выполнения правил политики безопасности.

4.3. Выводы к главе.

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

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

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

Значительным шагом на пути решения указанной проблемы является разработка и применение ГОСТ Р ИСО 15408, который приходит на смену нормативным документам Гостехкомиссии [1-7]. ГОСТ совместим с системой международной стандартизации и предписывает составление профиля защиты, включающего ПБ (рис. В.2) [8-11].

Организация

Разработчик

Рис. В.1. Влияние средств защиты на выполнение правил политики безопасности

Профиль защиты (ПЗ)

Рис. В.2. Политика безопасности в структуре профиля защиты согласно ГОСТ Р ИСО 15408

Стандарт накладывает требования обеспечения гарантированности * выполнения системой правил ПБ. Согласно стандарту установление гарантированности основывается на активном исследовании ИС, в результате чего должны быть выявлены причины невыполнения ПБ [8-10, 12]. Поэтому введение нового ГОСТ требует создания методов и инструментария проверки выполнения ПБ. Автоматизация анализа выполнения ПБ позволит придать ему объективный характер, обеспечить надежность защиты информации и качество сертификационных исследований.

Моделирование выполнения правил ПБ — это новое научное направление, теоретическая и методологическая базы которого в настоящее время только формируются в работах таких ученых как Грушо А.А., Расторгуев С. П., Щербаков А.Ю., Деннинг Д.Е., МакЛин Д., Сандху Р., Самарати П. Специалисты Гостехкомиссии и ее подведомственных организаций разрабатывают средства автоматизации анализа защитных свойств (например, НКВД, АИСТ). Однако упомянутые средства не решают задачу в полном объеме. Данная работа опирается на результаты указанных исследований и развивает их отдельные положения применительно к задачам моделирования защитных механизмов и автоматизации проверки выполнения правил ПБ.

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

Целью работы является обеспечение сертификационных исследований информационных систем по ГОСТ Р ИСО 15408 средствами проверки выполнения правил ПБ, основанными на применении метода автоматизированного анализа безопасности достижимых состояний.

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

1. Анализ моделей КУД, средств защиты современных ИС, а также методов моделирования ПБ.

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

3. Разработка метода проверки выполнения правил ПБ путем автоматизированного анализа безопасности достижимых состояний.

4. Разработка системы проверки выполнения правил ПБ, позволяющей автоматизировать процесс исследования ИС на предмет соблюдения ПБ.

5. Создание методики проверки выполнения правил ПБ в ходе сертификационных исследований ИС по ГОСТ Р ИСО 15408.

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

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

1. Проведен сравнительный анализ методов, используемых для моделирования и исследования ПБ.

2. Предложен и обоснован подход к проверке выполнения правил ПБ путем автоматизированного анализа достижимых состояний ИС.

3. Разработаны концептуальные модели подсистем КУД для современных операционных систем (ОС).

4. Разработана форма представления системных состояний, требований модели КУД и правил ПБ в виде системы логических предикатов.

5. Предложен метод проверки выполнения правил ПБ путем анализа безопасности достижимых состояний на основе вычисления предикатов, описывающих ПБ, в контексте системных состояний и модели КУД.

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

7. Разработана методика проверки выполнения правил ПБ в ходе сертификационных исследований ИС по ГОСТ Р ИСО 15408.

Практическая ценность работы определяется возможностью использования полученных в ходе работы результатов для проведения анализа ПБ и проверки ИС на соответствие ПБ. Метод автоматизированной проверки выполнения ПБ и средство описания системных состояний, правил ПБ и требований модели безопасности использованы при разработке программ и методик сертификационных исследований специализированной ИС (акт об использовании от ЗАО "РНТ", г. Москва). Подход к проверке ПБ путем автоматизированного анализа достижимых состояний испытываемой системы использован при разработке представления модели КУД, реализованной в системе мониторинга безопасности сложных информационных комплексов (акт об использовании от ЗАО "АРГО-Технолоджи", г. Москва). Метод автоматизированного анализа выполнения правил ПБ и разработанный комплекс средств оценки защищенности использованы при создании системы проверки выполнения ПБ организаций (акт об использовании от НИИ системотехники ХК "Ленинец", г. С.-Петербург). На основе теоретических и практических результатов разработаны учебно-методические материалы, используемые для подготовки специалистов в области защиты вычислительных систем по дисциплинам "Теоретические основы защиты информации" и "Безопасность ОС" в СПбГУАП (акт об использовании от СПбГУАП) и СПбГПУ.

Основные теоретические и практические результаты диссертационной работы доложены и обсуждены: на Российской научно-технической конференции "Методы и технические средства обеспечения безопасности информации" (СПбГПУ, 1998-2002 гг.); на Санкт-Петербургском семинаре "Информационная безопасность-99" (СПбГТУ, 1999 г.); на ведомственной конференции "Проблемы обеспечения информационной безопасности на федеральном железнодорожном транспорте" (Внедренческий центр ГУП "Аттестационный центр Желдоринформзащита МПС РФ", 2001 г.); на Межрегиональной конференции "Информационная безопасность регионов России" (Институт информатики и автоматизации РАН, 2001, 2002 гг.); на Российской научно-технической конференции "Проблемы информационной безопасности в системе высшей школы" (МИФИ, 2002, 2003 гг.).

Основные положения, выносимые на защиту:

1. Обоснование подхода к проверке выполнения правил ПБ путем автоматизированного анализа безопасности достижимых состояний ИС.

2. Метод проверки выполнения правил ПБ, основанный на вычислении предикатов, описывающих системные состояния, требования модели КУД и правила ПБ.

3. Система проверки выполнения правил ПБ.

4. Методика проверки выполнения правил ПБ на основе автоматизированного анализа безопасности состояний.

Диссертация состоит из введения, четырех глав, заключения и списка литературы из 95 наименований.

4.3. Выводы к главе

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

Предложенная методика позволила провести автоматический анализ выполнения примера ПБ в ОС Windows 2000. Для данной системы были построены описания начального состояния, правил модели КУД, реализованной в системе, и правил ПБ. Описания были обработаны с помощью средств СП.

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

Разработанная СП применима как средство проверки разрешительной подсистемы ИС на предмет выполнения правил ПБ в соответствии с требованиями ГОСТ Р ИСО 15408. Использование СП гарантирует выполнение функций защиты существующих и создаваемых ИС.

ЗАКЛЮЧЕНИЕ

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

Создание на практике системы и методики проверки выполнения правил ПБ подтвердило правильность принципов, а использование разработанных средств позволяет обеспечить сертификационные исследования по ГОСТ Р ИСО 15408 в плане анализа выполнения правил ПБ. Все вместе это составляет основу для развития безопасных информационных технологий.

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

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

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

3. Впервые предложен метод проверки выполнения правил политик безопасности на основе вычисления логических предикатов, описывающих системные состояния, требования модели контроля и управления доступом и правила политик безопасности, который закладывает основы для автоматизации сертификационных исследований по ГОСТ Р ИСО 15408.

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

5. Разработана система проверки выполнения правил политик безопасности, применяемая для автоматизированных исследований информационных систем.

6. Разработана методика проверки выполнения правил политик безопасности в ходе сертификационных исследований информационных систем по ГОСТ Р ИСО 15408.

1. Концепция защиты средств вычислительной техники от несанкционированного доступа к информации. Руководящий документ. М.: Гостехкомиссия России, 1992. 9 с.

2. Средства вычислительной техники. Защита от несанкционированного доступа к информации. Показатели защищенности средств вычислительной техники от несанкционированного доступа к информации. Руководящий документ. М.: Гостехкомиссия России, 1992. 25 с.

3. Автоматизированные системы. Защита от несанкционированного доступа к информации. Классификация автоматизированных систем и требования по защите информации. Руководящий документ. М.: Гостехкомиссия России, 1992. 39 с.

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

5. Калинин М.О. Организационно-правовые аспекты лицензирования и сертификации в сфере защиты информации // Проблемы информационнойбезопасности: Сб. рефератов студ. научн. раб. СПб: Изд-во СП6ГУ.1999. С. 10-14.

6. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. ГОСТ Р ИСО 15408-1-99: В 3 ч. Ч. 1: Введение и общая модель. Первая редакция. М.: Госстандарт России, 1999. 51 с.

7. Зегжда Д.П., Ивашко A.M. Как построить защищенную информационную систему. СПб: НПО "Мир и семья-95", 1997. 312 с.

8. Щербаков А.Ю. К вопросу о гарантированной реализации политики безопасности в компьютерной системе //Безопасность информационных технологий. 1997. №1. С. 15-26.

9. Зегжда Д.П., Калинин М.О. Безопасность операционных систем. Модели контроля и управления доступом: Лаб. практикум. 4.1. Дискреционные модели. СПб: Изд-во СПбГПУ, 2003. 104 с.

10. Зегжда Д.П., Калинин М.О. Безопасность операционных систем. Модели контроля и управления доступом: Лаб. практикум. 4.2. Мандатные, информационные и комбинированные модели. СПб: Изд-во СП6ГПУ,2003.76 с.

11. Математические основы информационной безопасности /Баранов А.П., Борисенко Н.П., Зегжда П.Д. и др. Орел: ВИПС, 1997. 354 с.

12. Теоретические основы информационной безопасности. Доп. главы /Баранов А.П., Зегжда Д.П., Зегжда П.Д. и др. СПб.: Изд-во СПбГТУ, 1998. 174 с.

13. Теория и практика обеспечения информационной безопасности/ Под ред. Зегжды П.Д. М.: Изд-во аг-ва "Яхтсмен", 1996. 298 с.

14. Harrison М.А., Ruzzo W.L., Ullman J.D. Protection in operating systems. Comm. of the ACM, 19(8), 1976. p. 461-471.

15. Denning D.E. Cryptography and Data Security. Addison-Wesley, 1982.400 p.

16. Castano S., Fugini M.G., Martella G., Samarati P. Database Security. Addison-Wesley, 1995. 456 p.

17. Bell D.E., LaPadula L.J. Secure Computer Systems: Mathematical Foundations. MITRE Technical Report 2547, Vol. II, MITRE, Bedford, MA, 1973. 31 p.

18. Bell D.E., LaPadula L.J. Secure computer systems: Unified exposition and Multics interpretation. MITRE Technical Report 2997, MITRE, Bedford, MA, 1975. 134 p.

19. Просихин В.П. Формализация условий безопасности и моделирование действий нарушителя в системах, построенных на основе модели Белла-ЛаПадула //Проблемы информационной безопасности. Компьютерные системы. 2000. №2. С. 57-64.

20. McLean J. A Comment on the 'Basic Security Theorem' of Bell and LaPadula / Information Processing Letters, Vol. 20(2), 1985. P. 67-70.

21. McLean J. Security models and information flow. In Proceedings of the 1990 IEEE Symposium on Research in Security and Privacy. IEEE Computer Society Press, 1990. p. 180-187.

22. Goguen J. A., Meseguer J. Security Policies and Security Models. Proc. 1982 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1982. p. 11-20.

23. Иртегов Д.В. Введение в операционные системы. СПб.: БХВ-Петербург, 2002. 616 с.

24. Таненбаум Э. Современные операционные системы. СПб: Питер, 2002. 1040 с.

25. Gollmann D. Computer Security. John Wiley and Sons, 1999. 320 p.

26. Morgan R., McGilton H. Introducing UNIX System V. McGraw-Hill Book Company, 1987. 612 p.

27. Curry D.A. Unix System Security. Addison-Wesley, Reading, MA, 1992.296 р.

28. Робачевский A.M. Операционная система UNIX. СПб.: БХВ-Петербург, 2000. 528 с.

29. Керниган Б.В., Пайк P. UNIX — универсальная среда программирования. М.: Финансы и статистика, 1992. 304 с.

30. Хэвиленд К., Грэй Д., Салама Б. Системное программирование в UNIX. Руководство программиста по разработке ПО. М.: ДМК Пресс, 2000. 368 с.

31. Schultz Е.Е. Windows NT/2000 Network Security. Macmillan Technical Publishing, 2000. 437 p.

32. Брагг P. Система безопасности Windows 2000. M.: Изд. дом "Вильяме", 2001. 592 с.

33. Расторгуев С.П. Введение в теорию информационного противоборства. СПб.: Изд-во СПбГТУ, 2000. 74 с.

34. Грушо А.А., Тимонина Е.Е. Двойственность многоуровневой политики безопасности //Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2000. С. 40-41.

35. McLean J. The specification and modeling of computer security. IEEE Computer, 23(1), 1990. p. 9-16.

36. Haigh J. T. A Comparison of Formal Security Models. Proc. 7th National Computer Security Conference, Gaithersburg, MD, 1984. p. 88-111.

37. McLean J. A Formal Method for the Abstract Specification of Software. Journal of the ACM, 31(3), 1984. p. 600-627.

38. Hoagland J.A. Security Policy Specification Using a Graphical Approach. The University of California, Davis Department of Computer Science, Davis, CA, 1993. 2 p.

39. Hoagland J.A., Pandey R., Levitt K.N. Security Policy Specification Using a Graphical Approach. Technical Report CSE-98-3, The University of California, Davis Department of Computer Science, Davis, CA, 1998. 17 p.

40. Harel D. On Visual Formalisms. Comm. of the ACM, 31(5), 1988. P. 512-530.

41. Allan H., Maimone M.W., Tygar J.D, Wing J.M., Moormann Zaremski A. Miry: Visual Specification of Security. IEEE Transactions on Software Engineering (TSE), 16(1), 1990. P. 1185-1197

42. Калинин M.O. Применение метода графов при моделировании политик безопасности // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2001. С. 10-12.

43. Калинин М.О. Моделирование политик безопасности с применением метода графов // Межрегиональная конференция "Информационная безопасность регионов России" ("ИБРР-2001"): Материалы конференции. СПб: ООО "Политехника-сервис". 2001. Т. 1. С. 150.

44. Калинин М.О. Моделирование политик безопасности с применением метода графов // Российская научно-техническая конференция "Проблемы информационной безопасности в системе высшей школы": Тез. докл. М: МИФИ. 2002. С. 64.

45. Damianou N., Dulay N., Lupu E., Sloman M. The Ponder Policy Specification Language. Proc. Policy 2001: Workshop on Policies for Distributed Systems and Networks, Bristol, UK, 2001. P. 29-31.

46. McLean J. Proving noninterference and functional correctness using traces / Journal of Computer Security, 1(1), 1992. p. 37-57.

47. Cholvy L., Cuppens F. Analyzing Consistency of Security Policies. Proc. of the 1997 IEEE Symposium on Security and Privacy. Oakland, CA, USA: IEEE Press, 1997. P. 103-112.

48. Jajodia S., Samarati P., Subrahmanian V.S. A Logical Language for Expressing Authorizations. Proc. of the 1997 IEEE Symposium on Security and Privacy. Oakland, CA, USA, IEEE Press, 1997. P. 31-42.

49. Jajodia S., Samarati P., Subrahmanian V., Bertino E. A unified framework for enforcing multiple access control policies. In Proc. ACM SIGMOD International Conference on Management of Data, Tucson, AZ, 1997. P. 474-485.

50. Bertino E., Jajodia S., Samarati, P. A flexible authorization mechanism for relational data management systems. ACM Transactions on Information Systems 17 (2), 1999. P. 101-140.

51. Bertino E., Buccafurri F., Ferrari E., Rullo P. An authorizations model and its formal semantics. Proc. of the 5th European Symp. on Research in Computer

52. Security (ESORICS'98), number 1485 in LNCS,, Louvain-la-Neuve, Belgium, 1998. P. 127-142.

53. Miller D.V., Baldwin R.W. Access control by Boolean Expression Evaluation. Proc. 5th Annual Computer Security Applications Conference. Tucson, AZ, USA: IEEE Computer Society Press, 1990. P. 131-139.

54. Gray J. W., Ill, Syverson P. F. A Logical Approach to Multilevel Security of Probabilistic Systems /Proc. of the 1992 IEEE Symposium on Security and Privacy, Oakland, CA, 1992. P. 164-176.

55. Li N., Feigenbaum J., Grosof В. A logic-based knowledge representation for authorization with delegation. Proc. of the 12th IEEE Computer Security Foundations Workshop, Mordano, Italy, 1999. P. 162-174.

56. Tidswell J. E., Jaeger T. An Access Control Model for Simplifying Constraint Expression. Proc. of the 7th ACM conference on Computer and Communications Security, 2000. P. 154-163.

57. Калинин M.O. Язык описания политик безопасности информационных систем // Современное машиностроение: Сб. трудов молодых ученых. Вып. 1. СПб: Изд-во СПбИМаш. 1999. С. 69-74.

58. Зегжда Д.П., Калинин М.О. Реализация универсального языка описания политики безопасности // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 1998. С. 12-15.

59. Калинин М.О. Методы моделирования политик безопасности // Межрегиональная конференция "Информационная безопасность регионов России" ("ИБРР-2002"): Материалы конференции. СПб: ООО "Политехника-сервис". 2002. С. 144.

60. Калинин М.О. Классификация методов моделирования политик безопасности // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2002. С. 12-15.

61. Калинин М.О. Методы моделирования политик безопасности // Российская научно-техническая конференция "Проблемы информационной безопасности в системе высшей школы": Тез. докл. М: Изд-во МИФИ. 2003. С. 38.

62. Зегжда Д.П., Калинин М.О. Моделирование защищенности компьютерных систем, основанное на множестве правил // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2001. С. 5-9.

63. Зегжда Д.П., Калинин М.О. Оценка защищенности информационных систем // Проблемы информационной безопасности. Компьютерные системы. 2002. №3. С. 7-12.

64. Зегжда Д.П., Калинин М.О. Моделирование защищенности компьютерных систем // Межрегиональная конференция "Информационная безопасность регионов России" ("ИБРР-2001"): Материалы конференции. СПб: ООО "Политехника-сервис". 2001. Т. 1. С. 150.

65. Зегжда Д.П., Калинин М.О. Моделирование защищенности в компьютерных системах // Российская научно-техническая конференция "Проблемы информационной безопасности в системе высшей школы": Тез. докл. М: МИФИ. 2002. С. 52.

66. Калинин М.О. Структура и применение языка описания политик безопасности // Проблемы информационной безопасности. Компьютерные системы. 2002. №1. С. 18-26.

67. Bratko I. PROLOG Programming for Artificial Intelligence. Addison-Wesley Pub Co, 2000. 678 p.

68. Стобо Д.Ж. Язык программирования Пролог. М.: Радио и связь, 1993.368 с.

69. Малпас Дж. Реляционный язык Пролог и его применение. М.: Наука: Гл. ред. физ.-мат. лит., 1990. 464с.

70. Себеста Р.У. Основные концепции языков программирования. М.: Издат. дом "Вильяме", 2001. 672 с.

71. Тей А., Грибомон П., Луи Ж., Снийерс Д. и др. Логический подход к искусственному интеллекту: от классической логики к логическому программированию. М. Мир, 1990. 432 с.

72. Логическое программирование //Сборник. М. Мир, 1988. 368 с.

73. Руководство пользователя SWI-Prolog. ftp://swi.psy.uva.nl/pub/SWI-Prolog/refman/

74. Хопкрофт Д.Э., Мотвани Р., Ульман Д.Д. Введение в теорию автоматов, языков и вычислений. М.: Изд. дом "Вильяме", 2002. 528 с.

75. Зегжда Д.П., Калинин М.О. Моделирование политик безопасности для исследовательских и обучающих целей // Проблемы информационной безопасности. Компьютерные системы. 2000. №2. С. 105-111.

76. Калинин М.О. Лабораторное моделирование и исследование политик безопасности // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2000. С. 204-207.

77. Зегжда Д.П., Калинин М.О. Состав и комплекс лабораторных работ по дисциплине "Защищенные операционные системы" // Российская научно-техническая конференция "Проблемы информационной безопасности в системе высшей школы": Тез. докл. М: МИФИ. 2002. С. 51.

78. Зегжда Д.П., Калинин М.О. Универсальный механизм внедрения политик безопасности в защищенную информационную систему // Сборник "Проблемы управления информационной безопасностью". М: Институт системного анализа РАН. 2002. С. 31-35.

79. Зегжда Д.П., Калинин М.О. Формальный язык представления составных политик безопасности // Межрегиональная конференция "Информационная безопасность регионов России" ("ИБРР-2002"): Материалы конференции. СПб: ООО "Политехника-сервис". 2002. С. 143.

80. Зегжда Д.П., Калинин М.О. Формальный язык представления составных политик безопасности // Российская научно-техническая конференция "Проблемы информационной безопасности в системе высшей школы": Тез. докл. М: Изд-во МИФИ. 2003. С. 35.

81. Bonatti P., De Capitani Di Vimercati S., Samarati P. An Algebra for Composing Access Control Policies. ACM Transactions on Information and System Security (TISSEC), 5(1), 2002. p. 1-35.

82. Зегжда Д.П., Калинин М.О. Математические основы построения и моделирования комбинированных политик безопасности // Проблемы информационной безопасности. Компьютерные системы. 2002. №2. С. 7-13.

83. Зегжда Д.П., Калинин М.О. Алгебра составных политик безопасности // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2002. С. 6-8.

84. Зегжда Д.П., Калинин М.О. Тестирование дискреционного управления доступом в ОС Феникс // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2001. С. 172-175.

85. Зегжда Д.П., Калинин М.О. Организация управления дискреционным доступом в ОС "Феникс" // Межрегиональная конференция "Информационная безопасность регионов России" ("ИБРР-2001"): Материалы конференции. СПб: ООО "Политехника-сервис". 2001. Т. 1. С. 147.

86. Калинин М.О. Автоматическое доказательство защищенности систем дискреционного управления доступом // Методы и технические средства обеспечения безопасности информации: Тез. докл. СПб: Изд-во СПбГТУ. 2002. С. 9-11.

87. Калинин М.О. Автоматический анализ состояний операционной системы Windows 2000 // Проблемы информационной безопасности. Компьютерные системы. 2003. №1. С. 4-6.