Содержание к диссертации
Введение
1 Логическое разграничение доступа 12
1.1 Терминология 13
1.2 Базовые модели 15
1.2.1 Многоуровневая модель 15
1.2.2 Дискреционная модель 17
1.2.3 Ролевая модель разграничения доступа 20
1.3 Современные языковые средства представления моделей логического разграничения доступа 23
1.4 Выводы 30
2 Язык описания моделей логического разграничения доступа 32
2.1 Основные положения разработанного языка 33
2.2 Синтаксис 39
2.3 Примеры использования разработанного языка 47
2.4 Описание формальной модели языка 49
2.5 Выводы 54
3 Анализ свойств моделей логического разграничения доступа, опи санных на разработанном языке 56
3.1 Традиционные способы анализа 57
3.2 Алгоритм проверки свойства включения моделей логического разграничения доступа 60
3.3 Выводы 68
4 Программная реализация механизмов разграничения доступа 70
4.1 Общие положения программных механизмов логического разграничения доступа 71
4.2 Механизмы разграничения доступа в ядре ОС Linux 72
4.3 Библиотека для разграничения доступа 76
4.4 Повышение производительности механизмов разграничения доступа 80
4.4.1 Эквивалентные преобразования моделей разграничения доступа 81
4.4.2 Кэширование разрешенных доступов 87
4.4.3 Преобразование в исполняемый код 90
4.5 Заключение 92
5 Тестовые испытания 93
5.1 Проверка выполнения функционального требования 93
5.2 Тестовые испытания методов повышения производительности механизмов логического разграничения доступа 95
5.2.1 Тестирование метода «эквивалентные преобразования моделей» 96
5.2.2 Тестирование метода «преобразование в исполняемый код» 97
5.3 Тестовые испытания механизмов логического разграничения доступа 98
5.4 Выводы 100
Заключение 101
- Современные языковые средства представления моделей логического разграничения доступа
- Примеры использования разработанного языка
- Алгоритм проверки свойства включения моделей логического разграничения доступа
- Повышение производительности механизмов разграничения доступа
Введение к работе
Актуальность работы. Б связи с активным использованием информационно-вычислительных комплексов для решения практически значимых задач все больший интерес в последнее время проявляется к средствам описания политик их информационной безопасности и, в частности, к моделям и механизмам логического разграничения доступа к ресурсам таких комплексов. Доступ к подобным ресурсам, к которым относятся информационные активы, средства вычислительной техники и коммуникаций, далее для краткости изложения будем именовать просто «доступом». Средства логического разграничения доступа (далее для краткости в тексте используется сочетание «разграничения доступа»), основанные на этих механизмах, занимают одно из центральных мест среди других компонентов, реализующих политику безопасности защищаемого объекта. К их числу относятся также средства идентификации/аутентификации пользователей и процессов, действующих от их имени, экранирования, шифрования и иные компоненты [4]. Механизмы разграничения доступа могут быть встроены как в операционные системы (ОС) и системные сервисы, так и в сервисы прикладного уровня [7].
Положения законов и подзаконных актов, нормативно-регламентирующих документов, стандартов и рекомендаций в области обеспечения безопасности информационных технологий [1,8-Ю, 17] определяют ряд требований к механизмам защиты в автоматизированных системах, в том числе — к программным механизмам логического разграничения доступа. К числу требований, предъявляемых к таким механизмам, используемым в автоматизированных системах с повышенными требованиями защищенности, относится требование существования формальных моделей, на основе которых они функционируют.
Формальное описание модели логического разграничения доступа сложно организованной компьютерной системы является крайне трудоемкой задачей
*>
в связи с гетерогенностью средств описания составляющих ее моделей в отдельных компонентах программной системы. В программных системах, работающих под управлением современных ОС, таких как Linux и Windows, используются программные реализации механизмов разграничения доступа, основанных на моделях, разработанных еще в 1970х годах, таких как дискреционная [47] или многоуровневая [22,24]. Дискреционная модель представляет собой достаточно вариативную в плане реализуемых на ее основе правил, простую для описания модель логического разграничения доступа. Вместе с тем политики безопасности на основе такой модели получаются громоздкими в их формальном и «машинном» представлении, сложно верифицируемыми и, как следствие, неудобными для управления. Мандатная модель разграничения доступа на основе упорядоченных меток безопасности является, наоборот, слишком «жесткой» с точки зрения условий и правил, которые она реализует. Она удобна в плане верификации, проста с позиции ее формального представления, управления и настройки, однако пригодна для реального применения при реализации политик безопасности относительно узкого класса информационных систем.
Перечисленные модели, а также ряд других [11, 29] определяют лишь базовые отношения, на основе которых формируются программные механизмы логического разграничения доступа к данным и ресурсам подлежащих защите практически значимых компьютерных систем. Реализация политик безопасности, использующих современные и более сложные модели разграничения доступа, такие как ролевая, сопряжена с большими трудностями внедрения дополнительных механизмов в ядра операционных систем и их практического использования в составе программных комплексов. Механизмы разграничения доступа, встроенные в различные компоненты, зачастую обладают собственным языком описания набора правил, в соответствии с которыми доступ разрешается или запрещается. Это обстоятельство затрудняет анализ со стороны пользователя или администратора, отвечающего за информационную безопасность системы, соответствия механизмов разграничения доступа, которые реализуются в отдельных компонентах сложной системы, политике безопасности системы в целом. Отмеченные выше и ряд других недостатков эксплуатирующихся в настоящее время систем стимулируют рабо-
ты по созданию новых логико-языковых средств описания моделей разграничения доступа, таких как extended Access Control Markup Language [54], Enterprise Privacy Authorisation Language [53]. Данные средства предоставляют администратору системы возможность самому определить модель разграничения доступа, в большей степени соответствующую потребностям защищаемого информационно-вычислительного комплекса, или выбрать необходимую по требованиям информационной безопасности модель среди предлагаемых другими разработчиками. Такие логико-языковые средства обладают широким кругом выразительных средств для описания условий, при которых разрешается или запрещается доступ. Отмеченное обстоятельство является важным преимуществом этих языков перед другими способами задания моделей логического разграничения доступа. Однако, и это следует отметить, перманентно выполняемые в течении всего времени функционирования информационной системы проверки на разрешение или запрещение доступа при использовании сложных моделей логического разграничения доступа, основанных на такого рода языковых средствах, становятся существенно более затратными в смысле потребляемых при их использовании вычислительных ресурсов, чем при применении более простых моделей. Последнее обстоятельство приводит к существенному замедлению работы информационной системы. Таким образом, одной из задач, важных для успешного внедрения и использования подобных средств в реальных информационно-вычислительных комплексах, является разработка, внедрение и оптимизация механизмов разграничения доступа, основанных на выразительных логико-языковых средствах.
В ходе жизненного цикла информационных систем происходят постоянные изменения, обновления, объединения и разделения, связанные с соответствующими процессами, происходящими в организациях, которые контролируют соблюдение требований безопасности ресурсов таких систем. Подобные модификации связаны с изменением структуры организаций, внутренних регламентов, стандартов и нормативно-правовых документов, регламентирующих их деятельность. Такие изменения должны отражаться в политиках информационной безопасности организаций и, в частности, в моделях логического разграничения доступа. Процесс создания и изменения моделей разграничения доступа и, в частности, их интеграции или разделения на несколько моделей является
?
крайне трудоемким и подверженным ошибкам.
Отмеченные выше обстоятельства определяют актуальность задачи автоматизированного анализа корректности моделей и механизмов логического разграничения доступа, которая, в свою очередь, во многом зависит от свойств языка их описания. Настоящая работа направлена на разработку нового, более удобного для использования на практике языка описания моделей логического разграничения доступа к ресурсам информационно-вычислительных (автоматизированных) систем и решение представленных выше задач применительно к такому языку.
Объектом исследования являются механизмы логического разграничения доступа в компьютерных системах, к защищенности которых предъявляются повышенные требования.
Предметом исследования являются формальные модели логического разграничения доступа в компьютерных системах, подходы к описанию и анализу таких моделей.
Цель диссертационной работы состоит в исследовании методов описания моделей логического разграничения доступа, в разработке и практической реализации на этой основе программных средств разграничения доступа пользователей к ресурсам компьютерных систем. Для достижения этой цели сформулированы и решаются следующие задачи:
создание формальной модели языка описания моделей логического разграничения доступа;
разработка на ее основе языка описания моделей логического разграничения доступа, эффективного с позиций предъявляемых к нему требований;
разработка алгоритмов анализа (проверки) свойств моделей, представленных на основе разработанного языка;
реализация программных средств разграничения доступа, основанных на разработанном языке и повышение их производительности;
проведение тестовых испытаний программных средств разграничения
доступа, і
Цель работы и перечисленные задачи соответствуют положениям паспорта специальности 05.13.19 — методы и системы защиты информации, информационная безопасность.
На защиту выносятся следующие основные результаты.
Формальное описание класса моделей логического разграничения доступа, которое включает в себя достаточное широкое с практической точки зрения множество моделей.
Логико-языковые средства (язык), позволяющие эффективно с позиции предъявляемых к ним требований описывать рассматриваемый класс моделей.
Алгоритм, позволяющий производить сравнения моделей, описанных с помощью разработанного языка, на предмет того, является ли одна из них «включенной» в другую.
Программные средств разграничения доступа, построенные на основе разработанного языка и предназначенные для их внедрения в ядро ОС Linux и в программы, написанные на языках С и Python.
Методы повышения эффективности программных механизмов логического разграничения доступа, позволяющие существенно ускорить принятие решения о предоставлении доступа к информационным активам, вычислительным и коммуникационным ресурсам защищаемых систем, а также результаты тестовых испытаний предложенных методов.
Методы исследования. Для формализации ряда используемых в настоящей работе понятий и проведения строгих доказательств используются следующие методы:
методы математической логики, включая исчисление предикатов;
методы дискретной математики, в том числе, теории графов, теории булевых функций;
методы программной инженерии.
Научная новизна результатов диссертации состоит:
в разработке новых подходов к описанию формальных моделей логического разграничения доступа на основе логико-языковых средств;
в создании способов сравнения описанных таким образом моделей;
в исследовании вопросов программной реализации механизмов разграничения доступа на основе разработанных логико-языковых средств.
Практическая значимость диссертационной работы заключается в разработанном автором языке описания моделей логического разграничения доступа, методах анализа моделей, описанных с помощью этого языка, а также в реализованных программных механизмах разграничения доступа, основанных на разработанном языке и предназначенных для внедрения в ядро Linux и прикладные программы.
Апробация работы. Результаты работы докладывались на научных конференциях «Математика и безопасность информационных технологий» (2005-2006 гг.), «Актуальные проблемы вычислительной математики» (2006 г.), на семинаре «Проблемы современных информационно-вычислительных систем» под руководством д. ф.-м. н., проф. В. А. Васенина (механико-математический факультет МГУ имени М. В. Ломоносова, 2005, 2009 гг.).
Внедрение результатов работы. Результаты работы нашли свое применение в процессе выполнения проектов: «Методы и средства противодействия компьютерному терроризму: механизмы, сценарии, инструментальные средства и административно-правовые решения» (НИР 2005-БТ-22.2/001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям науки и техники»). Получено свидетельство об официальной регистрации программы для ЭВМ «Набор специализированных дистрибутивов ОС Linux с повышенными требованиями к защищенности» (свидетельство № 2006613706).
Публикации. По результатам работы опубликовано 7 научных статей, из них — одна статья в журнале из перечня ведущих рецензируемых изданий, рекомендованных ВАК [2].
Материалы работы вошли в главу 3 опубликованной в 2008 году коллективной монографии «Критически важные объекты и кибертерроризм. Часть 2.
Аспекты программной реализации средств противодействия» (О. О. Андреев и др. под ред. В. А. Басенина) [15].
Личный вклад автора заключается в проведенном им анализе существующих логико-языковых средств описания моделей логического разграничения доступа, в разработке нового языка описания таких моделей, алгоритма анализа моделей, представленных на разработанном языке, а также в создании программных средств, реализующих разграничение доступа на основе нового языка.
Структура работы.
Первая глава диссертации посвящена результатам выполненных автором исследований, направленных на систематизацию и обобщение сведений об используемых в настоящее время на практике моделях логического разграничения доступа (ЛРД) и способах их описания. Рассмотрены преимущества и недостатки каждой из представленных моделей ЛРД и средств их описания. Выделяются ключевые задачи, решение которых представлено в работе.
Во второй главе рассматривается разработанный автором язык описания моделей логического разграничения доступа. Представлены базовые понятия, синтаксис и формальное математическое описание достаточно представительного класса моделей логического разграничения доступа, а также примеры использования разработанного диссертантом языка для их описания.
В третьей главе приводится исследование современных подходов к анализу моделей ЛРД, обосновывается необходимость разработки новых подходов и алгоритмов, которые могут быть применены в задаче изучения моделей ЛРД, описанных с помощью представленного в главе 2 языка.
Четвертая глава посвящена вопросам программной реализации механизмов разграничения доступа на основе разработанного языка. Рассматриваются основные принципы построения архитектуры средств разграничения доступа и их место в программных комплексах защиты информационной безопасности. Приводятся технические аспекты внедрения механизмов ЛРД в ядро Linux и в другие программные системы. Исследуются вопросы повышения производительности разработанных механизмов.
Пятая глава содержит описание методик проверки разработанных механизмов, а также результаты проведенных тестовых испытаний.
В заключении перечисляются основные результаты диссертационной работы.
\%
Современные языковые средства представления моделей логического разграничения доступа
С развитием, активным использованием во всех сферах человеческой деятельности, и усложнением автоматизированных систем изменяются и требования к информационной безопасности, в том числе, к правилам логического разграничения доступа к их ресурсам. Традиционно используемые базовые модели разграничения доступа, такие как дискреционная или ролевая, а также механизмы на их основе не всегда оказываются достаточно выразительными для описания всех требований по безопасности, которые предъявляются к подобным системам. По этой причине возникает необходимость в разработке моделей разграничения доступа ориентированных на конкретные информационные системы или требования по их безопасности, которые предъявляют использующие эти системы организации. Сама по себе разработка модели не является в большинстве случаев трудоемкой процедурой. Однако задача реализации программных механизмов разграничения доступа на ее основе и их корректное использование — достаточно сложный и подверженный ошибкам процесс.
Языковые средства описания моделей логического разграничения доступа для решения этих задач начали развиваться не так давно. В случае использования механизмов разграничения доступа, основанных на таких средствах, достаточно описать модель в терминах некоторого языка, после чего данные механизмы могут разграничивать доступ на основе этого описания. На настоящее время существует достаточно большое число языков описания моделей логического разграничения доступа, как общего назначения [26,53], подходящих для использования в любых информационных системах, к которым предъявляются требования по разграничению доступа, так и в специализированных, ориентированных на определенные сферы применения, которые включают языки описания правил фильтрации сетевых пакетов [28, 46] и другие. В настоящее время один из языков описания моделей логического разграничения доступа, называемый extended Access Control Markup Language (XACML) [54], принят в качестве стандарта. Далее на примере этого языка рассмотрим особенности языков описания моделей логического разграничения доступа общего назначения и реализующих их программных механизмов.
Язык XACML создан группой специалистов — экспертов, представляющих различные бизнес-компании и исследовательские учреждения, в рамках работы по созданию единого стандарта для описания средств и методов информационной безопасности. Первая версия стандарта языка вышла в 2003 году. В настоящее время организацией Oasis Open стандартизована вторая версия этого языка.
Язык XACML основывается на стандарте Internet Engineering Task Force, который именуется Framework for Policy-based Admission Control [45]. Этот стандарт описывает основные понятия и общие аспекты архитектуры некоторого абстрактного механизма разграничения доступа. Стандарт не описывает конкретные модели разграничения доступа, на основе которых такой механизм может производить разграничение доступа. Двумя главными компонентами описываемого абстрактного механизма разграничения доступа, в соответствии с этим стандартом, являются: точка разграничения доступа, в стандарте именуемая Policy Enforcement Point (далее — точка PEP); точка принятия решения, именуемая согласно стандарту Policy Decision Point (далее — точка PDP).
Точкой принятия решения называется компонент, в котором рассматриваются запросы на доступ, проверяется их соответствие принятой в информационной системе модели логического разграничения доступа и выдается решение о разрешении или запрете доступа. Точка разграничения доступа непосредственно связана с информационным ресурсом, который необходимо защищать. В этом компоненте реализуется модель разграничения доступа, принятая в информационной системе, на основе рассмотрения запроса на доступ, происходящего в точке принятия решения.
Указанные компоненты взаимодействуют между собой при попытке доступа. Точка принятия решения при этом может взаимодействовать с дополнитель ными компонентами, если в этом появляется необходимость для решения вопроса о предоставлении доступа. В ходе работы системы попытка доступа регистрируется в точке разграничения доступа, после чего такая точка формирует и направляет запрос на предоставление доступа в точку принятия решения. Точка принятия решения на основе поданных и, возможно, дополнительных данных выносит решение и направляет его в качестве ответа на запрос. На основании ответа точка разграничения доступа либо разрешает, либо запрещает доступ. В случае появления ошибки при рассмотрении запроса, точка решения вопроса о предоставлении доступа может посылать информацию об этой ошибке.
Разрешение или запрещение доступа принимается на основе некоторых так называемых политик, которые являются записью модели разграничения доступа на определенном языке, а также — данных о субъекте, объекте и типе доступа, которые содержатся в запросе или запрашиваются точкой принятия репіения у отдельных компонентов — хранилищ информации.
Указанные программные компоненты не обязательно должны быть реализованы в виде отдельных программных модулей. Данное разделение на два отдельных компонента является логическим. Вместе с тем, эти компоненты могут быть отделены друг от друга и, возможно, находиться на разных узлах компьютерной сети. Такая конфигурация информационной системы позволяет использовать одну точку принятия решений на несколько точек разграничения доступа, что упрощает контроль за соблюдением единой политики информационной безопасности.
Стандарт XACML задает язык описания моделей разграничения доступа, а также алгоритм функционирования точки принятия решения, которая использует этот язык. Описание функционирования механизма разграничения доступа на этом языке называется набором политик (policy set). Понятие набора политик в стандарте XACML соответствует общепринятому понятию модели разграничения доступа, поэтому при дальнейшем изложении будет использоваться термин «модель». Решение на запрос на доступа в соответствии с моделью может быть одним из трех: «разрешить» (Permit), «запретить» (Deny) и «не применимо» (NotApplicable). Последнее решение может выдаваться в том случае, если модель не применима к поданному запросу, описание способа определения применимости модели к запросу будет дано далее. Решение о доступе может сопровождаться набором обязательных действий (Obligations), которые должны быть выполнены точкой предоставления доступа перед его предоставлением. Получение решения о предоставлении доступа в соответствии с некоторой моделью разграничения доступа называется применением модели к запросу, а полученное решение — результатом применения.
Основным понятием, на основе которого формулируются модели в стандарте XACML, является понятие атрибута. Под атрибутом подразумевается свойство субъекта, объекта, типа доступа или окружения (environment), которое может влиять на решение о предоставлении доступа. Под окружением понимается среда выполнения, в которой происходит запрос на доступ. Каждый атрибут имеет имя и фиксированный тип данных, которые могут соответствовать данному атрибуту. Разграничение доступа производится на основе значений атрибутов субъекта, объекта, типа доступа и окружения, которые учитываются при принятии решения о доступе.
Стандарт XACML определяет набор типов данных, которым могут соответствовать атрибуты, а также набор атрибутов, которые обязан иметь каждый субъект, объект, тип доступа и окружение. К типам данных, в числе прочего, относятся: строковый; целочисленный; булев; вещественный. Обязательными атрибутами, в числе других, являются: идентификатор (для субъекта, объекта и типа доступа); текущее время (для окружения); время входа в систему (для субъекта). Существование у субъектов, объектов или окружения других атрибутов определяется спецификой информационной системы, в которой используется разграничение доступа на основе XACML. Так, например, при описании модели разграничения доступа, использующейся в информационной системе, к которой предъявляются требования по многоуровневому разграничению доступа, у субъектов может существовать атрибут «уровень допуска», а у объектов — «требуемый уровень допуска».
Примеры использования разработанного языка
Созданный в рамках настоящей работы язык, предоставляет достаточно широкие в плане функциональных возможностей средства для описания моделей логического разграничения доступа. В настоящем разделе в качестве примера будет представлено описание с его помощью языка детализированной модели логического разграничения доступа.
В качестве детализированной модели разграничения доступа была выбрана модель, которая является в некотором смысле развитием ролевого разграничения доступа. Более детально правила, по которым эта модель разграничивает доступ, формулируются следующим образом. В качестве предположения допустим, что информационная система, в которой используется модель, принадлежит некоторому учебному заведению, которое подразделяется на несколько факультетов. 1. В информационной системе существуют два допустимых вида доступа — «чтение» (read) и «запись» (write). 2. Каждый из пользователей информационной системы, в которой применяет данная модель, может принадлежать к одному из трех непересекающихся классов: «студент», «преподаватель» и «сотрудник деканата». 3. Каждый из пользователей информационной системы относится к одному и только одному факультету. 4. Объекты информационной системы, подлежащие защите, делятся по следующим классам: учебные материалы; расписание; результаты экзаменов. 5. Любой пользователь информационной системы может читать любые учебные материалы и расписание. 6. Студент может читать результаты экзаменов, которые он сдавал. 7. Преподаватель может читать и записывать результаты экзаменов, которые он принимал, а также изменять расписание его занятий и его учебные материалы. 8. Сотрудник деканата может читать и изменять расписание факультета, к которому он относится, а также читать результаты экзаменов студентов, которые относятся к тому же факультету, что и он.
В приложении Б представлено полное формальное описание перечисленных выше правил с помощью разработанного автором языка. Рассмотрим это описание более подробно. Первая часть описания (строки 2-9) посвящена указанию типов атрибутов, которые используются в модели. К атрибутам субъектов относятся атрибуты type и department (факультет), имеющие строковый тип. К атрибутам объектов относятся атрибуты type (класс объекта) lecturer (преподаватель), student (студент) и department (факультет), каждый из которых имеет строковый тип.
Первое правило модели (строки 11-16) соответствует неформальному правилу «любой пользователь информационной системы может читать любые учебные материалы и расписание». В том случае, если класс объекта — учебные материалы или расписание, а тип доступа — «чтение», доступ разрешается независимо от субъекта.
Второе правило модели (строки 28-24) соответствует неформальному правилу «студент может читать результаты экзаменов, которые он сдавал». В том случае, если класс субъекта — студент, класс объекта — результаты экзаменов, а идентификатор студента соответствует идентификатору, записанному в результатах, и тип доступа — «чтение», доступ разрешается.
Третье правило модели (строки 26-32) соответствует неформальному правилу «преподаватель может читать и записывать результаты экзаменов, которые он принимал, а также изменять расписание его занятий и его учебные материалы». В том случае, если класс субъекта — «преподаватель», доступ разрешается тогда, когда идентификатор преподавателя соответствует идентификатору, записанному в объекте.
Четвертое правило модели (строки 34-40) соответствует неформальному правилу «Сотрудник деканата может читать и изменять расписание факультета, к которому он относится». В том случае, если класс субъекта — «сотрудник», а класс объекта — «расписание», доступ разрешается тогда и только тогда, когда идентификатор факультета, к которому принадлежит сотрудник, соответствует идентификатору факультета, записанному в объекте.
Пятое правило модели (строки 42-49) соответствует неформальному правилу «Сотрудник деканата может читать результаты экзаменов студентов, которые относятся к тому же факультету, что и он». В том случае, если класс субъекта — «сотрудник», а класс объекта — «результаты экзаменов», доступ разрешается в том случае, если идентификатор факультета, к которому принадлежит сотрудник, соответствует идентификатору факультета, записанному в объекте, а доступ — чтение. Как легко заметить, рассмотренная запись модели логического разграничения доступа на разработанном автором языке полностью соответствует набору неформально описанных требований по разграничению доступа, правила реализации котрого перечислены в начале раздела.
Алгоритм проверки свойства включения моделей логического разграничения доступа
В процессе обновления политики информационной безопасности автоматизированной системы или объединения политик безопасности отдельных ее компонентов, ресурсы которых подлежат защите, возникает необходимость изменить или объединить в одну несколько моделей логического разграничения доступа. Например, когда первая модель ЛРД используется для анализа доступа к ресурсам одного компонента системы, а вторая — к ресурсам другой. При проведении такого объединения или изменения зачастую возникает необходимость проверить, является ли вновь полученная модель более «слабой», то есть, менее ограничивающей, чем предыдущие модели. Проведение такой проверки позволяет гарантировать, что у потенциальных злоумышленников не появилось новых возможностей доступа к защищаемым ресурсам информационной системы. В данном разделе будет описан способ анализа моделей логического разграничения доступа, основанных на предложенном языке, позволяющий проверять указанное свойство.
Будем считать, что одна модель слабее другой, если первая модель разрешает все доступы, которые разрешает вторая модель. Опишем этот факт с помощью формальных понятий, представленных в предыдущей главе.
Определение 3.1. Одна модель разграничения доступа с формулой разрешения доступа F, называется более слабой, чем другая, с формулой разрешения доступа 2 в том случае, когда истинно следствие F2 = F Одна модель разграничения доступа называется более сильной, чем вторая, если вторая является более ела бой, чем первая.
Разработанный автором и представленный в данной работе алгоритм позволяет проверять, является ли одна модель разграничения доступа более сильной, чем вторая, при определенных ограничениях на подаваемые ему на вход модели. Ограничение налагается на формулы разрешения доступа моделей и, как следствие, на формулы Target и Condition их правил. Оно состоит в том, что множество F функций, на основе которого строятся эти формулы, содержит только булевы связки л, V, -і, а также операции сравнения =, Ф, , . Необходимо заметить, что указанные функции, за исключением булевых связок, могут иметь лишь аргументы, не являющиеся булевыми, и при их вычислении получают булев результат.
Назовем множество формул разрешения доступа моделей, которые могут быть поданы на вход представляемому алгоритму, допустимым множеством. Справедливо следующее утверждение.
Доказательство. Доказательство будем проводить методом индукции по размеру формулы разрешения доступа, то есть, по количеству функций, используемых в ее описании.
Докажем базу индукции. В том случае, если размер формулы равен нулю, исходя из определения формулы разрешения доступа, она имеет одно из следующих представлений:
В первом случае формула разрешения доступа очевидно является булевой формулой. Во втором случае атрибут а должен быть булевым, так как формула f должна возвращать булево значение. По этой причине а является литералом и, как следствие, f является булевой формулой. База индукции доказана.
Рассмотрим формулу разрешения доступа, которая имеет представление вида f(Fb F2). Функция f может быть одной из следующих:
В первом случае применим предположение индукции. Каждая из формул FT И F2 по предположению индукции является булевой формулой. Исходя из этого факта и определения булевой формулы следует, что исходная формула разрешения доступа также является булевой формулой.
Во втором случае, исходя из ограничений на построение формул разрешения доступа, изложенных в разделе 2.4, формулы Fi и F2 могут быть либо атрибутами, либо константами. В этом случае, исходная формула разрешения доступа является литералом.
Исходя из сделанного в предыдущем абзаце замечания, можно заключить, что функции из разрешенного множества, за исключением логических связок, могут использоваться лишь в составе литералов. Таким образом, вся формула разграничения доступа может рассматриваться как булева формула относительно заданных литералов.
Повышение производительности механизмов разграничения доступа
Выразительная способность языков описания моделей логического разграничения доступа тесно связана с вопросами производительности механизмов обеспечения информационной безопасности. Использование языковых средств для формального описания сложных моделей, состоящих из десятков и сотен правил, может существенно замедлить работу информационной системы, особенно, если проверки на разрешение доступа должны производиться часто. В данном разделе описываются основные методы повышения эффективности вычисления ответа на запрос о доступе. Эти методы могут применяться в механизмах, основанных на разработанном автором языке. Все представленные в данной работе способы повышения производительности не зависят друг от друга и могут быть использованы как вместе, так и по отдельности.
Одним из практически значимых способов, позволяющих оптимизировать механизмы логического разграничения доступа является способ, который называется эквивалентным преобразованием моделей.
При использовании указанного класса методов повышения производительности, механизм разграничения доступа производит необходимые преобразования соответствующей ему модели разграничения доступа на этапе инициализации (загрузки) и в дальнейшем использует преобразованную модель для решения вопроса о предоставлении доступа.
Специфика механизмов логического разграничения доступа состоит в том, что типовая детализированная модель, которую эти механизмы реализуют, описанная с помощью предлагаемого языка, будет состоять из сотен или даже тысяч правил. Каждое из этих правил может быть применимо к запросу на предоставление доступа. При стандартной реализации механизмов безопасности большая часть времени на обработку запроса при использовании такой сложной модели уходит на поиск правил, которые могут быть к этому запросу применены. Принимая отмеченные выше обстоятельства, в целях повышения эффективности рассматриваемых механизмов представляется целесообразным рассмотреть такие способы эквивалентных преобразования моделей разграничения доступа, которые могут существенно сократить затраты на поиск правил, удовлетворяющих запросу.
Одним из классов эквивалентных преобразований, которые используются для повышения производительности поиска необходимых правил, являются преобразования, направленные на построение общей области применимости модели.
Определение 4.2. Построением общей области применимости модели называется построение новой модели логического разграничения доступа по существующей таким образом, чтобы полученная модель совпадала с исходной во всех компонентах, кроме области применимости модели. Пусть Target — условие на атрибуты, ограничивающее область применения модели, Target , ..., Targetn — условия на атрибуты, описывающие области применимости входящих в нее правил и моделей. Пусть Additional — условие на атрибуты, при этом при любых значениях атрибутов верны следствия Target1 = Additional, ..., Targetn = Additional. Тогда в качестве области применимости новой модели берется Target л Additional.
Утверждение 4.2. Представленный выше класс преобразований является эквивалентным. Доказательство. Справедливость этого утверждения следует из алгоритма применения модели к запросу. Действительно, любой запрос, к которому мог ла быть применима исходная модель, должен удовлетворять условию на ат рибуты Target л (Target! v ... v Targetn). Так как для любого значения истин ность условия Targetj при любых значениях атрибутов совпадает с истинностью Targetj л Additional для любого і, то этот же запрос удовлетворяет условию на атрибуты TargetA ((Target] л Additional) v... v (Targetn л Additional), которое эк вивалентно условию TargetA Additional л (Target t v... vTargetn). Таким образом, к запросу может быть применена преобразованная модель. Как легко заметить, верно и обратное утверждение — любой запрос, к которому может быть приме нена преобразованная модель, входит в область применимости модели исход ной. Решение о доступе и пост-действия, выполняемые при получении запро са, подходящего под область определения преобразованной модели, совпада ют. Данное утверждение обоснован тем, что алгоритм комбинирования правил и правила и модели, содержащиеся в исходной, не изменялись при преобра зовании. Это следует из определения способа вычисления решения о доступе, данного в разделе 2.4. Вторым классом эквивалентных преобразований является разделение моделей.
Определение 4.3. Разделением моделей называется такое преобразование, при котором одна модель разграничения доступа делится на две, области применимости которых в их объединении порождают область применимости изначальной модели. Общая модель содержит эти две модели, причем алгоритмы комбинирования правил у общей модели, двух содержащихся в ней моделей и исходной модели совпадают. В каждой из получившихся моделей оставляются лишь те правила, область применимости которых пересекается с областью применимости содержащей их модели. Пусть Target —условие на атрибуты, ограничивающее область применения модели, Target ..., Targetn, Targetn+1,..., Targetn+k —условия на атрибуты, ограничивающие область применимости входящих в нее правил и моделей. Пусть Additional! и Additional — условия на атрибуты такие, что при любых значениях атрибутов истинно следствие Additional! v Additional = Target. Кроме этого, пусть условие Additional л Additional = False справедливо при любых значениях атрибутов.
Рассмотрим две модели, алгоритм комбинирования и пост-действия каждой из которых совпадают с исходной моделью. При этом область применимости первой модели — Additional а второй — Additional. В первой модели содержатся правила, области применимости которых не противоречат Additional!, то есть, если область применимости правила Target то условие Targetj = --Additional! должно быть ложно хотя бы при каких-то значениях входящих в него атрибутов. Во второй модели содержатся правила, области применимости которых не противоречат Additional.
Преобразованной моделью называется такая модель, которая содержит указанные выше две модели и алгоритм комбинирования совпадает с аналогичным алгоритмом исходной модели. Утверждение 4.3. Представленный выше класс преобразований является эквивалентным. Доказательство. В том случае, если преобразованная модель применима к запросу, то должно быть истинно условие Target, которое равносильно условию Additional! v Additional2. Таким образом, к запросу применима и исходная модель. Обратное утверждение также верно. В том случае, если исходная модель применима к запросу на доступ, он удо влетворяет условию Additionalb либо условию Additional. Рассмотрим случай, когда запрос удовлетворяет условию Additional!. В этом случае, к нему будет применима первая из построенных подмоделей. Те правила исходной модели, которым удовлетворял запрос, будут присутствовать и в первой построенной подмодели. В противном случае их область применимости противоречила бы условию Additional!. Так как алгоритм комбинирования и пост-действия исход ной модели и первой построенной подмодели совпадают, то результат приме нения первой подмодели к запросу, также как и результат применения преоб разованной модели, совпадает с результатом применения исходной. Указанные эквивалентные преобразования могут применяться при решении задачи повышения производительности вычисления разрешенных запросов на доступ следующим образом. Специальным образом подобранная процедура сужения области применимости модели и разбиение на подмодели позволит сократить число проверок. Вместо последовательности проверок на применимость каждого отдельного правила должна производиться одна проверка на применимость модели и, в случае ее неудачи, все остальные проверки будут игнорироваться. В некотором смысле, при построении таких эквивалентных моделей происходит преобразование линейного списка правил в дерево, поиск по которому будет существенно быстрее, чем по списку. Далее рассмотрим сравнительно простой алгоритм эквивалентного преобразования моделей разграничения доступа, основанный на двух представленных выше классах преобразований. Этот алгоритм состоит из двух основных шагов
