Содержание к диссертации
Введение
Глава 1. Исследование моделей логического разграничения доступа . 9
1.1. Актуальность проведения исследований в области разработки и практического использования моделей логического разграничения доступа . 10
1.2. Термины и определения 13
1.3. Задачи разработки и использования математических моделей логического разграничения доступа 18
1.4. Задачи, исследуемые в настоящей работе 22
1.5. Типовые требодания к моделям логического разграничения доступа и способы их проверки 23
1.6. Выводы 34
Глава 2. Описание моделей логического разграничения доступа . 36
2.1. Основные положения разработки и формального описания моделей логического разграничения доступа (ЛРД) 37
2.2. Унифицированный способ описания статической части правил ЛРД в моделях логического разграничения доступа 42
2.3. Учет древовидной иерархии на объектах доступа в модели ЛРД 48
2.4. Формальное описание моделей ЛРД, положенных в основу механизмов защиты в ядре ОС Linux 51
2.5. Выводы .' 61
Глава 3. Метод согласования моделей логического разграничения доступа 63
3.1. Постановка задачи согласования моделей разграничения доступа . 64
3.2. Операции согласования моделей логического разграничения доступа . 67
3.3. Метод согласования моделей логического разграничения доступа . 75
3.4. Выводы 76
Глава 4. Спецификация и проверка свойств безопасности в моделях логического разграничения доступа 77
4.1. Предпосылки для создания метода исследования моделей логического разграничения Доступа на предмет выполнения требований по безопас ности 78
4.2. Постановка задачи проверки свойств моделей логического разграничения доступа и типовые классы проверяемых свойств 79
4.3. Метод спецификации и проверки свойств моделей логического разграничения доступа на предмет выполнения требований безопасности 82
4.4. Специализированный алгоритм проверки свойств прохождения информационного потока 90
4.5. Замечания о практическом применении разработанного метода проверки свойств моделей 92
4.6. Выводы 93
Глава 5. Программная реализация комплекса средств для анализа моделей логического разграничения доступа на предмет выполнения требований по безопасности 94
5.1. Функциональные возможности программного комплекса для исследования моделей логического разграничения доступа на предмет выполнения требований по безопасности 95
5.2. Программная архитектура создаваемого набора инструментальных средств 97
5.3. Компоненты программного комплекса для исследования свойств безопасности в моделях ЛРД 99
5.4. Тестовые испытания: применение к разработке и использованию дистрибутивов операционных систем 103
5.5. Выводы . 119
Заключение 120
Список литературы 121
- Задачи разработки и использования математических моделей логического разграничения доступа
- Унифицированный способ описания статической части правил ЛРД в моделях логического разграничения доступа
- Операции согласования моделей логического разграничения доступа
- Постановка задачи проверки свойств моделей логического разграничения доступа и типовые классы проверяемых свойств
Введение к работе
Актуальность работы. Механизмы логического разграничения доступа к информационным активам, коммуникационным и вычислительным ресурсам (далее для краткости изложения используются сочетание «логическое разграничения доступа» и сокращение «ЛРД») являются важной составляющей современных компьютерных систем, к защищенности которых предъявляются повышенные требования [9,10,12,33]. С использованием механизмов логического разграничения доступа по заданному набору правил принимается решение о том, разрешено ли в автоматизированной системе некоторое действие, например, получение доступа к ее информационному ресурсу. Проблематике проектирования и разработки механизмов ЛРД, их интеграции в автоматизированные системы, информационные ресурсы которых подлежат защите, а также к построению математических моделей, описывающих процессы функционирования таких механизмов, уделяется повышенное внимание с конца 1960-х — начала 1970-х годов. К настоящему времени созданы многочисленные механизмы логического разграничения доступа, традиционным примером которых являются механизмы ЛРД в операционных системах (ОС), разработаны подходы к описанию математических моделей, составляющих основу функционирования подобных программных механизмов. К классическим формальным моделям логического разграничения доступа относятся модели дискреционного разграничения доступа, в том числе модель «take-grant», модели мандатного многоуровневого разграничения доступа, включая фундаментальные модели Белла-ЛаПадула и Биба. Получили широкое распространение модели ЛРД на основе ролей, ключевые положения которых начали формироваться в 1990-е годы. Активно ведутся исследования в рассматриваемой области отечественными учеными [13].
Положения законов и подзаконных актов, нормативно-регламентирующих документов, стандартов и рекомендаций в области обеспечения безопасности информационных технологий определяют ряд требований к механизмам защиты в автоматизированных системах, в том числе — к механизмам логического разграничения доступа. Вместе с тем, практической реализации таких требований в современных системах препятствует то обстоятельство, что управление настройками подобных механизмов, как правило, осуществляется без должного анализа последствий. Изменения в настройки вносятся локально, модифицируются небольшие фрагменты правил логического разграничения доступа. При этом оценка влияния таких изменений на защищенность компьютерной системы в целом не производится. В результате уровень доверия к такой системе снижается. Отмеченная особенность характерна для механизмов ЛРД в современных Unix-подобных операционных системах, например, в ОС на базе ядра ОС Linux, которые в настоящее время часто используются в автоматизированных системах с повышенным
уровнем защищенности.
Формальной спецификации требований, которые предъявляются к механизмам и, как следствие, к моделям логического разграничения доступа, посвящено большое число работ. Значительное внимание уделяется задачам проверки выполнения ограничений на информационные потоки [13,58]. Однако, результатов практического характера, целью которых является исследование моделей ЛРД, положенных в основу механизмов защиты современных Unix-подобных ОС, недостаточно для проведения анализа таких механизмов и их конфигурации на предмет выполнения требований по безопасности. Необходимость проведения такого анализа с учетом особенностей моделей и реализующих их механизмов ЛРД, которые используются в современных Unix-подобных ОС, значительный, как правило, объем конфигурационных данных таких механизмов и потребности в их совместном использовании на практике определяют актуальность настоящей работы.
Объектом исследования являются механизмы логического разграничения доступа в компьютерных системах, к защищенности которых предъявляются повышенные требования.
Предметом исследования являются формальные модели логического разграничения доступа в компьютерных системах, подходы (методы и средства) к спецификации и проверке свойств реализующих их программных средств.
Цель диссертационной работы состоит в исследовании и разработке математических моделей, алгоритмов и программных средств, поддерживающих процессы спецификации и анализа свойств моделей логического разграничения доступа, ориентированных на применение в инструментальных средствах автоматизации управления настройками механизмов логического разграничения доступа в компьютерных системах, в составе которых используются Unix-подобные операционные системы.
На защиту выносятся следующие основные результаты:
разработаны и сформулированы способы формального описания моделей логического разграничения доступа для достаточно широкого класса компьютерных систем, в первую очередь — для систем на базе ядра ОС Linux;
сформулированы и строго обоснованы положения нового способа объединения и согласования математических моделей логического разграничения доступа, с помощью которого предоставляется возможность исследовать совместно используемые механизмы ЛРД в компьютерных системах, разрабатываемых на основе Unix-подобных операционных систем;
разработан доказательно корректный способ спецификации и анализа свойств моделей логического разграничения доступа, с помощью которого может быть проверено выполнение ограничений на информационные потоки в компьютер-
ной системе; - предложен и апробирован в процессе тестовых испытаний программный комплекс для анализа моделей логического разграничения доступа, которые реализуются с помощью механизмов ЛРД в Unix-подобных ОС, на предмет выполнения ими требований по безопасности.
Методы исследования. Результаты диссертационной работы получены с использованием математического моделирования механизмов логического разграничения доступа в компьютерных системах, аппарата теории графов, методов «верификации на модели» (model checking), логического программирования, а также — положений программной инженерии.
Научная новизна результатов диссертации состоит в создании новых доказательно обоснованных способов описания моделей логического разграничения доступа, корректного объединения таких моделей, в их анализе на предмет выполнения заданных требований по безопасности. Отличительной особенностью разработанных автором способов, формальных моделей и алгоритмов является возможность математически строго описывать и анализировать с их помощью конфигурацию механизмов логического разграничения доступа в современных компьютерных системах, которые используют Unix-подобные операционные системы, такие, как ОС на базе ядра Linux, имея в виду архитектурные и функциональные особенности механизмов ЛРД в таких системах.
Практическая значимость диссертации заключается в применении созданного автором программного комплекса в процессе анализа моделей логического разграничения доступа на предмет выполнения требований по безопасности. Потенциальные возможности комплекса продемонстрированы на дистрибутивах операционных систем на базе ядра ОС Linux и программного обеспечения с открытым исходным кодом. В процессе тестовых испытаний показаны функциональные возможности разработанного программного комплекса по анализу настроек механизмов логического разграничения доступа при создании специализированных дистрибутивов ОС.
Внедрение результатов работы. Результаты работы нашли применение в процессе выполнения проектов: «Методы и средства противодействия компьютерному терроризму: механизмы, сценарии, инструментальные средства и административно-правовые решения» (НИР'2005-БТ-22.2/001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям науки и техники»); «Разработка подходов к обеспечению информационной безопасности автоматизированных систем государственного управления на основе использования в их составе программного обеспечения с открытым кодом» (НИР 2007-4-1.4-15-04-001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2012 годы»). Получено свидетельство об официальной регистрации программы
для ЭВМ «Набор специализированных дистрибутивов ОС Linux с повышенными требованиями к защищенности» (свидетельство № 2006613706).
Апробация работы. Результаты работы докладывались на научных конференциях «Математика и безопасность информационных технологий» (2005-2008 гг.), «Ломоносовские чтения» (2006-2009 гг.), «Актуальные проблемы вычислительной математики» (2006 г.), «Третья1 международная конференция по проблемам управления» (2006 г.), на семинаре «Проблемы современных информационно-вычислительных систем» под руководством д.ф.-м.н., проф. В. А. Васенина (механико-математический факультет МГУ имени М. В. Ломоносова, 2005, 2007, 2009 гг.).
Публикации. По теме диссертации опубликовано 14 работ, из которых 3 статьи [7,19,31] — в журналах из перечня ведущих рецензируемых изданий, рекомендованных ВАК. Материалы работы вошли в главу 3 опубликованной в 2008 году коллективной монографии «Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия» под ред. В. А. Васенина [28].
Личный вклад автора заключается в проведенном им анализе современного состояния в области формального описания моделей логического разграничения доступа, в способе, предложенном для объединения таких моделей, а также в разработанных автором и апробированных на практике методах, математических моделях, алгоритмах и программных средствах для анализа свойств механизмов логического разграничения доступа.
Структура и объем диссертации. Глава 1 посвящена результатам выполненных автором исследований, направленных на систематизацию и обобщение сведений о направлениях использования математических моделей ЛРД при проектировании и разработке автоматизированных систем с повышенным уровнем защищенности, а также — отдельных механизмов в составе таких систем. Выделены ключевые задачи, решение которых представлено в настоящей работе. Проводится исследование современных подходов к спецификации и проверке свойств в моделях логического разграничения доступа. Представлены результаты анализа особенностей таких подходов и оценка возможности их применения на практике в процессе проверки выполнения требований по безопасности, которые предъявляются к современным автоматизированным системам с повышенным уровнем их защищенности.
В главе 2 рассматриваются методы формального описания моделей логического разграничения доступа. Автором предлагается способ формального описания моделей ЛРД, позволяющий учитывать древовидную иерархию на множестве объектов доступа в модели, а также — унифицированный подход к описанию ряда традиционно используемых моделей ЛРД. Представлено формальное описание исследуемых далее в работе моделей, а именно — моделей ЛРД, которые реализуются механизмами защиты в ядре
ОС Linux.
Задачи разработки и использования математических моделей логического разграничения доступа
Целесообразно выделить следующий набор общих по постановке задач, связанных с исследованием, разработкой и использованием моделей логического разграничения доступа в современных компьютерных системах: построение моделей логического разграничения доступа по данным о конфигурации механизмов разграничения доступа в компьютерной системе («задача преобразования настроек в модель»); задание конфигурации механизмов логического разграничения доступа на основе формальной модели («задача преобразования модели в настройки»); объединение и согласование моделей логического разграничения доступа отдельных компонентов системы («задача объединения»); спецификация и проверка свойств моделей логического разграничения доступа («задача верификации»); проверка соответствия модели логического разграничения доступа механизму обеспечения безопасности компьютерной системы, функциональные возможно сти которого она моделирует («задача валидации»).
Первая и вторая задачи заключаются в проведении преобразования между математической моделью разграничения доступа и конфигурацией программного механизма, реализующего такую модель или некоторый класс моделей разграничения доступа, к которому она принадлежит. С практической точки зрения решение таких задач востребовано на направлении проведения (выполнения) автоматических изменений в настройках механизмов защиты в компьютерных системах. Их решение представляет практический интерес на этапе исследования корректности функционирования таких механизмов, включая их тестирование и проверку на соответствие высокоуровневым требованиям, которые задаются в принятой политике информационной безопасности.
Задача объединения и согласования моделей ЛРД является актуальной по целому ряду причин. В первую очередь следует отметить, что многие автоматизированные системы на настоящее время являются распределенными территориально, использующими, например, разветвленную сетевую инфраструктуру, в том числе — сети связи общего пользования. Более того, в силу организационной децентрализации на отдельных сегментах автоматизированной системы могут действовать различные правила обеспечения информационной безопасности. Для того, чтобы убедиться в корректности функционирования механизмов безопасности в распределенной системе в целом необходимо получить объединенное представление, например, в виде математической модели для дальнейшего исследования, о действующих правилах обеспечения безопасности, включая правила ЛРД. Второй причиной, по которой задача объединения и согласования моделей ЛРД заслуживает отдельного рассмотрения, является то обстоятельство, что многие из типовых компьютерных систем обладают некоторыми свойствами «распределенности» в структуре своей внутренней организации (обычно именуемой программной архитектурой). Отдельные компоненты программных комплексов зачастую обладают собственными механизмами разграничения доступа, действующими над множествами своих субъектов и объектов доступа. Так, например, в серверной операционной системе могут присутствовать несколько отдельных механизмов ЛРД в ядре ОС, в веб-сервере и серверах обмена файлами, в СУБД, в размещенных на сервере веб-приложениях. Наборы объектов доступа и правила, по которым разграничивается доступ к таким объектам посредством указанных механизмов, как правило, задаются для каждого из механизмов изолированно по отношению к другим. Тем не менее, имея в виду, что эти наборы объектов доступа находятся в одной автоматизированной системе, их совместное функционирование может привести к нарушениям правил разграничения доступа. Такие нарушения, например, могут оказаться возможными по причине наличия связей между объектами доступа из разных наборов. В этом случае, даже если над множествами своих объектов доступа каждый из механизмов ЛРД работает корректно, то о кор ректности их совместного функционирования определенных выводов сделать нельзя. Причиной является тот факт, что дополнительные, неучтенные связи между объектами доступа (а также, возможно, между субъектами доступа или другими сущностями моделей ЛРД) могут привести к несанкционированному доступу. В целях учета таких особенностей совместного функционирования нескольких механизмов разграничения доступа в автоматизированной системе при проверке корректности их функционирования возникает необходимость в разработке методов объединения моделей ЛРД, в том числе — построению единой модели ЛРД по нескольким заданным комбинируемым моделям.
Спецификация и проверка свойств в моделях ЛРД является главным направлением исследования, результаты которого представлены в настоящей работе. Назначение методов спецификации и проверки свойств в моделях ЛРД состоит: в формулировке на некотором формальном языке условий (свойств), выполнение которых необходимо для заданного набора настроек механизмов разграничения доступа; в автоматизированном доказательстве выполнения или невыполнения этих сформулированных условий в модели ЛРД, которая строится по настройкам исследуемых механизмов ЛРД.
Проведение подобной проверки, как отмечалось ранее, является актуальной задачей при проектировании, разработке и эксплуатации автоматизированных систем, к защищенности которых предъявляются повышенные требования. Отметим тот факт, что для выполнения спецификации и проверки выполнения свойств в моделях ЛРД появляется необходимость в выполнении ряда действий по подготовке формального описания исследуемой модели ЛРД и проверяемых свойств. Методы выполнения таких действий являются результатом решения задач о формальном описании и объединении моделей ЛРД, которые обсуждались выше.
Задача валидации представляет собой частный случай общей задачи верификации и тестирования, компьютерных программ. В результате решения такой задачи устанавливаются гарантированные свойства механизма ЛРД, но не заданной для него конфигурации. Роль модели ЛРД в такой задаче заключается в том, что она (или некоторый класс таких моделей) является одной из целевых спецификаций для общей задачи верификации исходного кода программных механизмов обеспечения безопасности, а также для задачи тестирования такого программного обеспечения. В силу отмеченных особенностей указанная задача выходит за рамки исследования, результаты которого представлены в настоящей работе.
Унифицированный способ описания статической части правил ЛРД в моделях логического разграничения доступа
При рассмотрении способов описания правил выполнения административных действий для механизмов ЛРД, следует отметить необходимость описания как самих правил, так и математической модели, согласно которой выполняются административные действия. Поясним указанное обстоятельство на следующем далее примере.
Пусть дана модель ЛРД, статическая часть правил в которой описывается отмеченным ранее упрощенным способом с использованием матрицы доступа. В качестве административных могут рассматриваться действия по изменению матрицы доступа. Правила, по которым определяется допустимость таких действий, могут быть описаны с помощью дополнительной матрицы доступа. В ней типам доступа соответствуют возможности по изменению правил доступа к некоторому объекту, то есть на изменение элементов основной матрицы доступа, описывающих доступ каждого из субъектов к заданному объекту. Для интерпретации таких правил динамического изменения статической конфигурации может быть использована система переходов, состояниями которой являются описания статической части правил (основная матрица доступа), а переходы между ними определяются дополнительной матрицей доступа. Таким же образом, как и в случае описания статической части правил, может быть применен способ группирования сущностей в модели для уменьшения размера матрицы доступа.
Схема динамического изменения модели в рассматриваемом примере может быть усложнена с помощью введения действий не только по изменению основной матрицы доступа, но и по изменению дополнительной матрицы доступа. Такие изменения содержательно соответствуют передаче прав на управление доступом к заданным объектам. В рассматриваемой упрощенной модели этот факт означает передачу права «владения» объектом по аналогии с дискреционным разграничением доступа к объектам файловых систем, которые используются в традиционно используемых операционных системах. Обычно подобные изменения рассматриваются как операции над некоторым математическим объектом, например, графом, представляющим доступы в модели ЛРД, разрешенные в рамках принятого набора правил разграничения доступа [66].
Следует отметить развитие подходов к описанию действий по изменению в ролевых моделях ЛРД. Например, для ряда ролевых моделей разработаны расширения, позволяющие описывать допустимые административные действия и правила по управлению ими [86]. Традиционный способ описания таких правил, которые регламентируют изменения в правилах ЛРД, аналогичен классическим способам описания статической части правил ЛРД и основан на теоретико-множественном описании. Как правило, определяются две составляющие динамической части модели ЛРД: правила, регламентирующие возможность и рамки изменения правил ЛРД (например, по отношению к отдельному объекту доступа или к классу таких объектов); правила, по которым производится изменение модели ЛРД, например, заданных в ней множеств и отношений.
Первая составляющая может быть рассмотрена как расширение предиката доступа, в котором появляется новый набор типов доступа, а именно — доступы на изменение правил ЛРД по отношению к объекту. Примером подобного формального описания правил являются отношение «субъект-владелец — объект» в моделях дискреционного разграничения доступа [87}, а также ограничения на изменение правил доступа в моделях ролевого ЛРД с административными привилегиями [86].
Вторая составляющая модели, как правило, описывается как система переходов между состояниями модели ЛРД. Такие системы переходов формально определяются, например, для моделей «take-grant» [12,69,70] и для моделей «доступы — потоки» [13].
Отметим, что в ряде случаев в рамках некоторых подходов к организации изменения правил ЛРД удается имитировать поведение, которое достигается с помощью других способов описания. Так, например, модели ролевого разграничения доступа с административными привилегиями позволяют имитировать ряд аспектов поведения моделей ЛРД, основанных на дискреционном принципе разграничению доступа [94].
Принимая во внимание возможность изменения правил разграничения доступа, следует исследовать воцрос, какая сущность в автоматизированной системе может производить такие изменения. В традиционных механизмах ЛРД, включая те, которые используются в ядрах операционных систем, могут быть выделены следующие распространенные способы организации изменения правил ЛРД. Правила ЛРД заданы изначально и не могут изменяться субъектами доступа в процессе функционирования автоматизированной системы. Примером использования такого способа являются модели мандатного многоуровневого доступа [47,49,53]. Правила ЛРД к каждому объекту могут быть изменены некоторыми выделенными субъектами в модели ЛРД. Среди распространенных способов выделения таких субъектов следует отметить следующие: правила доступа к объекту могут быть изменены субъектом-владельцем, определяемым для этого объекта в модели ЛРД (примером являются моде ли дискреционного разграничения доступа [87], в том числе применяемые в современных ОС (в таком случае, как правило, отношение «субъект является владельцем объекта» может передаваться другим субъектами, а также используется при описании статической части модели ЛРД); — в модели ЛРД для каждого объекта определяются множество выделенных субъектов, которым разрешено изменять правила доступа к этому объекту (примерами использования такого способа являются ролевые модели ЛРД с административными привилегиями [86]).
В настоящем разделе автором предлагается унифицированный способ описания статической части моделей ЛРД, позволяющий в единообразной форме записывать модели логического разграничения доступа, которые относятся к рассмотренным выше, традиционно используемым классам таких моделей. Основной предпосылкой для создания такого способа описания является то обстоятельство, что, как правило, с использованием предиката предоставления доступа (определение 1.5) решение о доступе вычисляется на основании атрибутов субъектов и объектов доступа. Множества таких атрибутов могут быть объединены (унифицированы), что приводит к некоторому упрощению записи правил разграничения доступа. Однако отметим, что предлагаемый способ описания моделей ЛРД предназначен для использования при решении задач анализа свойств таких моделей. При первоначальном задании правил ЛРД представляется целесообразным использовать способы описания моделей ЛРД, разделяющие субъекты и объекты доступа, в первую очередь — с целью выделения активной роли субъекта в выполнении операции доступа.
Результатом использования предлагаемого способа является представление нескольких разных моделей ЛРД в единой форме записи. Подобное единообразное представление позволяет упростить согласование нескольких моделей ЛРД. Кроме того, предлагаемый унифицированный способ описания моделей ЛРД в дальнейшем изложении (глава 4) служит основой для создания формальной модели — системы переходов, в которой будет производиться проверка свойств исследуемых моделей ЛРД.
В основу предлагаемого способа описания положено расширение понятия «контекст безопасности» из модели ЛРД Type Enforcement, которая реализована механизмами системы Security-Enhanced Linux. Ключевой особенностью этого понятия является тот факт, что аргументами предиката предоставления доступа в модели ЛРД являются два контекста безопасности и тип производимого доступа. Таким образом, использование контекстов безопасности позволяет в рамках унифицированного способа описания абстрагироваться от особенностей субъектов и объектов доступа за счет инкапсуляции таких особенностей в понятие контекста безопасности.
Операции согласования моделей логического разграничения доступа
Одним из способов преобразования моделей ЛРД в целях их согласования является выражение одной такой модели (будем называть ее исходной) с помощью логико-языковых средств другой модели (целевой) с сохранением семантики правил предоставления доступа исходной модели. В результате этого преобразования задача согласования двух моделей ЛРД, для задания которых используются различающиеся языки спецификации, сводится к задаче согласования моделей ЛРД в едином представлении.
При проведении преобразования такого вида целесообразно наложить ряд ограничений на соответствие элементов моделей ЛРД. К типовым ограничениям подобного рода следует отнести: отображения субъектов исходной модели в субъекты целевой модели и объектов исходной модели в объекты целевой модели должны быть инъективными; отображение типов доступа исходной модели в типы доступа целевой модели должно быть инъективным; сохранение дополнительно задаваемых отношений на множествах субъектов и объектов.
Отметим, что, зачастую, вместо инъективности вложения оказывается возможным добиться того, чтобы существовало взаимно однозначное соответствие между множествами элементов приводимых моделей ЛРД.
По причине накладываемых ограничений, а также ввиду отличий в схемах задания предикатов предоставления доступа в исходной и в целевой моделях ЛРД преобразование между этими моделями не всегда удается осуществить. Тем не менее, для некоторых пар исходных и целевых моделей такое преобразование возможно. Для ряда традиционно используемых дискреционных, многоуровневых и ролевых моделей ЛРД следует отметить результаты решения задач выражения одной из таких моделей через другую [1,73,75,94]. Результаты представления одной модели ЛРД с помощью логико-языковых средств другой такой модели, полученные автором для ряда моделей ЛРД, которые реализуются в некоторых современных механизмах защиты в ядре ОС Linux, представлены ранее в главе 2 (леммы 2.7 и 2.9).
Операция «слияния» моделей ЛРД представляет собой построение общей модели логического разграничения доступа, содержащей интегрируемые модели ЛРД как подмодели, без внесения дополнительных доступов. Принимая во внимание тот факт, что сущности подлежащих согласованию моделей ЛРД (далее, для краткости будем использовать термин «согласуемых моделей») могут отождествляться, в рамках выполнения операции их объединения моделей правила доступа между отождествляемыми сущностями не должны противоречить друг другу. Такое отождествление необходимо учитывать, например, в том случае, если рассматриваемые модели ЛРД описывают правила разграничения доступа к одним и тем же объектам.
Такую операцию, как правило, удобно применять к моделям логического разграничения доступа, которые основываются на иерархических и решеточных структурах. При слиянии таких моделей результат имеет упорядоченную структуру, такую же или подобного вида, как и у согласуемых моделей. В качестве примера реализации операции слияния для моделей RBACi, являющихся расширенными вариантами моделей RBACQ с использованием иерархий ролей, следует отметить результаты, использующие объединение графов ролевых иерархий [76].
Предложим формальное описание операции слияния моделей ЛРД. В целях сокращения изложения будем считать, что согласуемые модели ЛРД уже представлены с использованием унифицированного описания таких моделей с помощью контекстов безопасности (определение 2.3).
Определение 3.3. Пусть заданы модели ЛРД М\ = (SCi,Ai,Ai) и М2 = (502, 2 2)- Назовем модель ЛРД М — (SC,A,A) результатом слияния моделей ЛРД Mi и М2 (введем обозначение: М = SimpleMerge(Mi,M2)), если выполняются
При объединении нескольких моделей ЛРД, действующих над одними и теми же множествами субъектов и объектов доступа, целесообразно применить комбинирование предикатов предоставления доступа с помощью логических связок. Такой способ согласования зачастую неявно используется в механизмах операционных систем при определении возможности доступа.
Типовыми вариантами для комбинирования предикатов предоставления доступа являются использование логических связок «И» и «ИЛИ»:
Предложим формальное определение результата согласования моделей ЛРД, для которых задано унифицированное описание на основе контекстов безопасности.
Определение 3.4. Пусть заданы модели ЛРД Mi — (SC, А, Ді) и М2 = (SC,A,A2), у которых совпадают множества контекстов безопасности и множества типов доступа. Назовем модель ЛРД М = (SC, А, А) результатом согласования моделей ЛРД с использованием комбинирования предикатов предоставления доступа М\ и М2 (введем обозначение: М = РСотЪ(М\, М2, ор)), если задана бинарная операция ор над булевыми аргументами и выполняется следующее условие:
Отметим тот факт, что это определение может быть легко продолжено на случай объединения более чем двух моделей ЛРД, если операция ор будет коммутативной и ассоциативной.
Рассмотренные в предыдущих подразделах операции согласования моделей ЛРД обладают ограничениями. Согласование с помощью слияния моделей ЛРД нельзя произвести, если не выполнено условие, заданное формулой (3.18). Процедура согласования моделей ЛРД с использованием комбинирования предикатов предоставления доступа требует совпадения множеств контекстов безопасности и множеств типов доступа. Однако, после объединения этих двух операций согласования моделей логического разграничения доступа, появляется возможность представить более универсальную операцию согласования таких моделей.
Постановка задачи проверки свойств моделей логического разграничения доступа и типовые классы проверяемых свойств
Основной областью применения предлагаемого автором метода спецификации и проверки свойств в моделях ЛРД на практике является исследование свойств безопас ности таких моделей, которые используются в современных Unix-подобных операционных системах. Применение разрабатываемого метода не ограничивается указанной областью и расширяется на задачи проверки других моделей логического разграничения доступа. Такое расширение может быть произведено с учетом результатов, изложенных в главах 2 и 3. Ключевой особенностью нового способа проверки, отличающего его от других решений в этой области, является возможность учета иерархической структуры на множестве объектов доступа при автоматизированной проверке свойств. Общая задача проверки свойств моделей ЛРД в рамках создаваемого метода ставится следующим образом. В качестве входных данных предоставляются: модель ЛРД, правила которой сформулированы с помощью унифицированного описания, предложенного в разделе 2.2; подлежащее проверке свойство или набор свойств, которые заданы на языке спецификации свойств информационных потоков.
В результате проверки необходимо: доказать выполнение или невыполнение подлежащих проверке свойств; в случае невыполнения какого-либо из свойств предоставить описание контрпримера — последовательности действий, с помощью которой это свойство может быть нарушено.
В предлагаемом методе процедура доказательства и построение контрпримеров ориентированы на их выполнение в автоматизированном режиме.
Основной алгоритм проверки свойств безопасности, используемый в предлагаемом методе, является специализированным вариантом общего алгоритма верификации на модели [14].
Укажем ряд классов актуальных свойств безопасности, проверка которых реализуется предлагаемым методом. В основу всех рассматриваемых далее классов свойств положена спецификация ограничений на информационные потоки, разрешенные согласно исследуемой модели. Понятие информационного потока для моделей ЛРД, в которых ряд типов доступа подразумевает передачу информации между сущностями в модели (например, посредством операций чтения и записи), определяется следующим образом. В первую очередь определяется понятие элементарного информационного потока, а на его основе строится определение для общего вида информационного потока. Пусть в подлежащей анализу (проверке свойств) модели ЛРД рассматривается субъект доступа s и объект доступа о. Будем считать, что элементарный информационный поток от s к о разрешен, если правилами ЛРД допускается доступ «на запись» от s к о. Аналогичным образом, элементарный информационный поток от о к s разрешен, если правилами допускается доступ «на чтение» от s к о. Под типами доступа «на чтение» и «на запись» в контексте данной работы понимаются такие, что при реализации соответству ющего доступа информация передается от объекта к субъекту (для типа доступа «на чтение») и от субъекта к объекту (для типа доступа «на запись»). Отметим, что таких типов доступа каждого из видов может быть несколько. Рассматриваемые типы доступа реализуются во многих компонентах современных автоматизированных систем, включая рассматриваемые в настоящей работе механизмы операционных систем для логического разграничения доступа к объектам файловых систем. В подобном случае типы доступа «на чтение» и «на запись» реализуются в функциях чтения и записи (в том числе — продолжающей записи) файлов, чтения и изменения каталогов, чтения метаданных объектов файловой системы. В рассматриваемом примере, в соответствии с обсуждаемым определением, разрешены элементарные информационные потоки между процессами в ОС (субъектами доступа) и объектами файловых систем (объектами доступа). Из нескольких таких элементарных информационных потоков складываются составные допустимые информационные потоки. Будем считать, что между сущностями е\ и е2, каждая из которых может быть субъектом или объектом доступа в модели ЛРД, разрешен информационный поток, если существует конечная последовательность элементарных информационных потоков такая, что первый элементарный поток начинается в е\\ последний элементарный поток заканчивается в е ±\ конец каждого элементарного потока кроме последнего совпадает с началом следующего элементарного потока.
Интерпретировать такую конструкцию на примере операционной системы и доступа к объектам файловых систем можно следующим образом. Пусть процессу S\ в ОС не разрешен доступ на чтение файла о\, однако разрешен доступ на чтение файла о2. Одновременно, пусть процессу s2 в ОС разрешены доступы на чтение ох и на запись 02- Следовательно, согласно приведенным определениям, разрешен информационный поток oi —У S2 — 02 — si. Такое следствие указывает на тот факт, что при определенной координации действий процессов si и s2 в операционной системе процесс Si может получить информацию из файла о\, доступ на чтение к которому запрещен для Si в соответствии с заданными правилами разграничения доступа. Подобное взаимодействие может противоречить общим принципам правил ЛРД, которые устанавливаются для автоматизированной системы. Это свидетельствует о некорректной настройке используемых механизмов логического разграничения доступа. Например, в том случае, если процессы, аналогичные Si, могут создаваться только пользователем с низким уровнем привилегий, а файл 0\ содержит данные, которые предназначены для пользователей с высоким уровнем привилегий.
Общий вид одного из типовых свойств информационных потоков формулируется следующим образом. Пусть задано ограничение на информационный поток, в частно сти — указаны требования к начальной и конечной сущностям в потоке, а также к последовательности сущностей и типов доступа в потоке, например, что одна сущность Єї всегда идет после сущности е% и между ними всегда есть сущность ез. Необходимо проверить, выполняется ли это свойство для всех допустимых информационных потоков в заданной модели ЛРД. Отметим, что, как правило, кроме непосредственно проверки выполнения такого свойства появляется необходимость в построении контрпримера для случая, если оно не выполняется. Дополнительная информация, которая получается в процессе интерпретации подобного контрпримера, может упростить поиск некорректно заданных правил разграничешія доступа.
В качестве базового свойства, на котором демонстрируется применение методов верификации, выберем следующее: при заданных классах сущностей модели Е\, 5 и Ез любой информационный поток от сущности из Е\ к сущности из Ei проходит через одну из сущностей Е%.
Задание свойств, которыми должны обладать информационные потоки, составляют основу для формализации ряда других задач проверки свойств моделей ЛРД. К таким задачам относится, например, поиск конфликтов в модели ЛРД или в объединении таких моделей. Задача поиска конфликта может быть сформулирована в терминах информационных потоков. Примером ограничения на поток в таком случаем может являться спецификация его длины или требование «локальности» по отношению к одной из объединяемых моделей ЛРД. Проверка подобных свойств позволит определить ряд дополнительных потоков и доступов, ставших допустимыми вследствие объединения моделей.
