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

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ИМЕНИ М. В. ЛОМОНОСОВА Механико-математический факультет

На правах рукописи

0034Э0Э50

Шапченко Кирилл Александрович

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

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

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

2 8 ЯНВ 291д

Москва - 2010

Работа выполнена на Механико-математическом факультете и в Институте

проблем информационной безопасности Московского государственного университета имени М. В. Ломоносова.

Научный руководитель: доктор физико-математических наук, профессор

Васенин Валерий Александрович.

Официальные оппоненты: доктор физико-математических наук, профессор

Галатенко Владимир Антонович;

доктор технических наук, доцент Девяти Петр Николаевич.

Ведущая организация: ФГУП «НИИ «Квант».

Защита диссертации состоится 17 февраля 2010 г. в 16 час. 45 мин. на заседании диссертационного совета Д 501.002.16 при Московском государственном университете имени М. В. Ломоносова по адресу: Российская Федерация, 119991, ГСП-1, Москва, Ленинские горы, д. 1, Московский государственный университет имени М. В. Ломоносова, Механико-математический факультет, ауд. 14-08.

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета Московского государственного университета имени М. В. Ломоносова (Главное здание МГУ, 14 этаж).

Автореферат разослан 15 января 2010 г.

Ученый секретарь диссертационного совета Д 501.002.16 при МГУ, доктор физико-математических наук

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

Актуальность работы. Механизмы логического разграничения доступа к информационным активам, коммуникационным и вычислительным ресурсам (далее для краткости изложения используются сочетание «логическое разграничения доступа» и сокращение «ЛРД») являются важной составляющей современных компьютерных систем, к защищенности которых предъявляются повышенные требования.1 С использованием механизмов логического разграничения доступа по заданному набору правил принимается решение о том, разрешено ли в автоматизированной системе некоторое действие, например, получение доступа к ее информационному ресурсу. Проблематике проектирования и разработки механизмов ЛРД, их интеграции в автоматизированные системы, информационные ресурсы которых подлежат защите, а также к построению математических моделей, описывающих процессы функционирования таких механизмов, уделяется повышенное внимание с конца 1960-х — начала 1970-х годов. К настоящему времени созданы многочисленные механизмы логического разграничения доступа, традиционным примером которых являются механизмы ЛРД в операционных системах (ОС), разработаны подходы к описанию математических моделей, составляющих основу функционирования подобных программных механизмов. К классическим формальным моделям логического разграничения доступа относятся модели дискреционного разграничения доступа, в том числе модель «take-grant», модели мандатного многоуровневого разграничения доступа, включая фундаментальные модели Белла-ЛаПадула и Биба. Получили широкое распространение модели ЛРД на основе ролей, ключевые положения которых начали формироваться в 1990-е годы. Активно ведутся исследования в рассматриваемой области отечественными учеными.2

Положения законов и подзаконных актов, нормативно-регламентирующих документов, стандартов и рекомендаций в области обеспечения безопасности информационных технологий определяют ряд требований к механизмам защиты в автоматизированных системах, в том числе — к механизмам логического разграничения доступа. Вместе с тем, практической реализации таких требований в современных системах препятствует то обстоятельство, что управление настройками подобных механизмов, как правило, осуществляется без должного анализа последствий. Изменения в настройки вносятся локально, модифицируются небольшие фрагменты правил логического разграничения доступа. При этом оценка влияния таких изменений на защищенность компьютерной системы в целом не производится. В результате уровень доверия к такой системе снижается. Отмеченная особенность характерна для механизмов ЛРД в современных Unix-подобных

1Н. А. Гайдамакнн. Разграничение доступа к информации в компьютерных системах. — Екатеринбург: Изд-во Уральского университета. — 2003. — 328 с.

В. А. Галатенко. Основы информационной безопасности. Курс лекций. 4-е изд. — М.: «Интуит», 2008. — 205 с.

А. А. Грушо, Э. А. Применко, Е. Е. Тимонина. Теоретические основы компьютерной безопасности. — М.: Academia. - 2009. - 272 с.

2П. Н. Девянин. Анализ безопасности управления доступом и информационными потоками в компьютерных системах. — М.: Радио и связь, 2006. — 176 с.

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

Формальной спецификации требований, которые предъявляются к механизмам и, как следствие, к моделям логического разграничения доступа, посвящено большое число работ. Значительное внимание уделяется задачам проверки выполнения ограничений на информационные потоки.2'3 Однако, результатов практического характера, целью которых является исследование моделей ЛРД, положенных в основу механизмов защиты современных Unix-подобных ОС, недостаточно для проведения анализа таких механизмов и их конфигурации на предмет выполнения требований по безопасности. Необходимость проведения такого анализа с учетом особенностей моделей и реализующих их механизмов ЛРД, которые используются в современных Unbc-подобных ОС, значительный, как правило, объем конфигурационных данных таких механизмов и потребности в их совместном использовании на практике определяют актуальность настоящей работы.

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

Научная новизна результатов диссертации состоит в создании новых доказательно обоснованных способов описания моделей логического разграничения доступа, корректного объединения таких моделей, в их анализе на предмет выполнения заданных требований по безопасности. Отличительной особенностью разработанных автором способов, формальных моделей и алгоритмов является возможность математически строго описывать и анализировать с их помощью конфигурацию механизмов логического разграничения доступа в современных компьютерных системах, которые используют Unix-подобные операционные системы, такие, как ОС на базе ядра Linux, имея в виду архитектурные и функциональные особенности механизмов ЛРД в таких системах.

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

3J. iYank, М. Bishop. Extending the Take-Grant Protection System. — Department of Computer Science. — University of California at Davi3. — 1996.

J. McLean. Security Models and Information Flow. // In Proc. IEEE Symposium on Security and Privacy. — IEEE Computer Society Press. — 1990. — pp. 180-187.

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

- разработаны и сформулированы способы формального описания моделей логического разграничения доступа для достаточно широкого класса компьютерных систем, в первую очередь — для систем на базе ядра ОС Linux;

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

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

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

Внедрение результатов работы. Результаты работы нашли применение в процессе выполнения проектов: «Методы и средства противодействия компьютерному терроризму: механизмы, сценарии, инструментальные средства и административно-правовые решения» (НИР 2005-БТ-22.2/001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям науки и техники»); «Разработка подходов к обеспечению информационной безопасности автоматизированных систем государственного управления на основе использования в их составе программного обеспечения с открытым кодом» (НИР 2007-4-1.4-15-04-001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2012 годы»). Получено свидетельство об официальной регистрации программы для ЭВМ «Набор специализированных дистрибутивов ОС Linux с повышенными требованиями к защищенности» (свидетельство № 2006613706).

Апробация работы.- Результаты работы докладывались на научных конференциях «Математика и безопасность информационных технологий» (2005-2008 гг.), «Ломоносовские чтения» (2006-200Э гг.), «Актуальные проблемы вычислительной математики» (2006 г.), «Третья международная конференция по проблемам управления» (2006 г.), на семинаре «Проблемы современных информационно-вычислительных систем» под руководством д.ф.-м.н., проф. В. А. Васенина (механико-математический факультет МГУ имени М. В. Ломоносова, 2005, 2007, 2009 гг.).

Публикации. По теме диссертации опубликовано 14 работ, из которых 3 статьи [1-3] — в журналах из перечня ведущих рецензируемых изданий, рекомендованных ВАК. Материалы работы вошли в главу 3 опубликованной в 2008 году коллективной монографии «Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия» под ред. В. А. Васенина [8].

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

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

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

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

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

Исходные посылки для проведения анализа моделей ЛРД на предмет выполнения требований безопасности формируются на основе положений политики информационной безопасности (ПИБ) исследуемой автоматизированной системы. Положениями такой политики в том числе определяется ряд требований к функциям по защите информации, которые в исследуемой компьютерной системе реализуются в используемых аппаратно-программных средствах, а также задаются высокоуровневые правила по использованию таких функций защиты. Объектом исследования в настоящей работе является программная реализация отдельного класса таких функций, а именно — функций логического разграничения доступа.

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

Результаты настоящей работы в первую очередь нацелены на их применение в процессе исследования настроек механизмов ЛРД в современных Unix-подобных операционных системах. Примером таких механизмов являются традиционные средства разграничения доступа в подобных ОС, а также механизмы системы защиты SELinux для ядра ОС Linux.

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

Определение 2. Моделью логического разграничения доступа называется четверка М = (Б, О, А, Д), где

• 5 — конечное и непустое множество субъектов доступа;

• О — конечное и непустое множество объектов доступа;

• А — конечное и непустое множество типов доступа;

• Д — предикат над множеством 5 х О х А, определяющий для тройки (в, о, а) е 5 X О х А, разрешен ли доступ типа о субъекта в к объекту о (предикат предоставления доступа).

Модели логического разграничения доступа, которые задаются представленным определением и исследуются в настоящей работе, описывают так называемую «статическую» часть правил ЛРД. Такие правила определяют действия субъектов доступа над объектами доступа, которые разрешены в автоматизированной системе. Множества субъектов, объектов и типов доступа в модели ЛРД, а также предикат предоставления доступа рассматриваются как неизменные. Такой способ описания моделей ЛРД позволяет исследовать настройки механизмов логического разграничения доступа в рамках тех процессов функционирования автоматизированной системы, в которых не производится действий по созданию или удалению субъектов и объектов доступа, по изменению атрибутов таких сущностей, по изменению правил доступа субъектов к объектам, либо такие действия не оказывают влияния на предикат предоставления доступа в модели. Указанные условия вносят некоторые ограничения в класс автоматизированных систем, способ анализа настроек механизмов защиты которых предлагается в настоящей работе. Однако, такой класс остается достаточно широким и значимым в практическом плане.

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

Рис. 1. Требования к механизмам и моделям логического разграничения доступа, (случай использования нескольких механизмов ЛРД).

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

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

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

• объединение и согласование моделей логического разграничения доступа отдельных компонентов системы («задача объединения»);

• спецификация и проверка свойств моделей логического разграничения доступа («задача верификации»);

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

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

• формального описания используемых моделей ЛРД;

• объединения моделей ЛРД отдельных компонентов в составе сложно орга-

низованной системы;

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

Автором проводится исследование современных методов и средств спецификации и проверки свойств в моделях логического разграничения доступа. Анализируются предпосылки к проведению такой проверки. Приводится краткий обзор методов спецификации и проверки свойств механизмов логического разграничения доступа с использованием аппарата математических моделей ЛРД. Исследованию таких моделей на направлении выполнения в них требований по безопасности посвящен ряд современных работ как зарубежных авторов,4 так и российских ученых.5 В главе рассматривается несколько классов задач проверки выполнения требований, предъявляемых к моделям ЛРД:

• поиск конфликтов Правил в моделях ЛРД;

• поиск конфликтов правил при объединении нескольких моделей ЛРД;

• сравнение двух моделей ЛРД;

• исследование свойств информационных потоков.

Особое внимание уделяется классу задач, связанных с так называемыми разрешенными (или допустимыми) составными информационными потоками (далее, для краткости, — информационными потоками). Понятие информационного потока определяется следующим образом для моделей ЛРД, в которых ряд типов доступа подразумевает передачу информации между сущностями в модели. Пусть в рассматриваемой модели ЛРД рассматривается субъект доступа С и объект доступа О. Будем считать, что элементарный информационный поток от С к О разрешен, если правилами ЛРД допускается доступ «на запись» от С к О. Аналогичным образом, элементарный информационный поток от О к С разрешен, если правилами допускается доступ «на чтение» от С к О. Под типами доступа «на чтение» и «на запись» в работе понимаются такие, что при реализации соответствующего доступа информация передается от объекта к субъекту (для типа доступа «на чтение») и от субъекта к объекту (для типа доступа «на запись»). Отметим, что типов доступа «на чтение» и «на запись» может быть несколько. Из набора элементарных информационных потоков складываются составные допустимые информационные потоки. Будем считать, что между сущностями Al и А2, каждая из которых может быть субъектом или объектом доступа в модели ЛРД, разрешен информационный поток, если существует конечная последователь-

4J. D. Guttman, A. L. Herzog, J. D. Ramsdell, С. W. Skorupka. Verifying information flow goals in security-enhanced Linux. // Journal of Computer Security, vol. 13, 2004.

D. P. Guelev, M. D. Ryan, P.-Y. Schobbens. Model-checking access control policies. // In Information Security Conference, number 3225 in Lecture Notes in Computer Science. Springer-Verlag, 2004.

G. Hughes, T. Bultarj. Automated verification of access control policies. // Technical Report 2004-22. — University of California, Santa Barbara, 2004.

5П. H. Девянин. Анализ безопасности управлеаия доступом и информагдюшшми потоками в компьютерных системах. — М.: Радио в связь, 2006. — 176 с.

Д. Н. Колегов. Применение ДП-моделей для анализа защищенности сетей. // Прикладная я дискретная математика. - 2008. — № 1. — 71-87.

ность элементарных информационных потоков такая, что

• первый элементарный поток начинается в AI;

• последний элементарный поток заканчивается в А2;

• конечная сущность каждого элементарного потока кроме последнего совпадает с началом следующего элементарного потока.

По причине важности ограничения составных информационных потоков в практически значимых механизмах логического разграничения доступа, ставятся задачи проверки свойств таких потоков в моделях ЛРД. Общий вид одного из типовых свойств информационных потоков формулируется следующим образом. Пусть задано ограничение на информационный поток, в частности, указаны требования к начальной и конечной сущностям в потоке, а также — к последовательности сущностей и типов доступа в потоке, например, что одна сущность А2 всегда идет после сущности AI и между ними всегда есть сущность A3. Необходимо проверить, выполняется ли это свойство для всех допустимых информационных потоков в заданной модели ЛРД. Отметим, что, как правило, кроме непосредственно проверки выполнения такого свойства появляется необходимость в построении контрпримера для случая, если оно не выполняется. Дополнительная информация, которая получается в процессе интерпретации подобного контрпримера, может упростить поиск некорректно заданных правил разграничения доступа. Отметим, что задание свойств, которыми должны обладать информационные потоки, зачастую составляют основу для формализации других задач проверки свойств моделей ЛРД. Например, ряд задач поиска конфликтов в модели ЛРД или в объединении таких моделей может быть сформулирован в терминах информационных потоков.

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

• поиск пути в графе и алгоритмы переписывания графов;

• методы «верификации на модели» («model checking»);

• методы автоматического доказательства теорем;

• исследование модели ЛРД как вычислительного алгоритма или программы на некотором императивном языке программирования.

Выявленные особенности методов проверки требований безопасности в моделях ЛРД являются одними из отправных положений, в соответствии с которыми автором разрабатывается новый метод проверки свойств моделей ЛРД. Такой метод проектируется с целью его дальнейшего использования на практике для исследования свойств моделей ЛРД в современных автоматизированных системах, использующих Unix-подобные операционные системы, в том числе — ОС на основе ядра Linux. Новый метод позволит отразить в математической модели ЛРД ряд типовых функциональных особенностей механизмов защиты таких систем, уменьшить объем исследуемых моделей с помощью отождествления «похожих» правил доступа, эффективно проверить свойства из некоторого класса требований, которые являются распространенными для целевых систем.

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

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

Автором предлагается унифицированный способ описания статической части моделей ЛРД, позволяющий в единообразной форме записывать модели логического разграничения доступа, которые относятся к рассмотренным ранее в главе традиционно используемым классам таких моделей. В основу предлагаемого способа описания положено расширение понятия «контекст безопасности» из модели ЛРД Type Enforcement. Ключевой особенностью этого понятия является то обстоятельство, что аргументами предиката предоставления доступа в модели ЛРД являются два контекста безопасности и тип производимого доступа. Таким образом, использование контекстов безопасности позволяет в рамках унифицированного описания абстрагироваться от особенностей субъектов и объектов доступа за счет инкапсуляции таких особенностей в понятие контекста безопасности.

Предлагаемый унифицированный способ описания моделей ЛРД не изменяет свойств (семантики) моделей ЛРД, а лишь позволяет записать их правила в унифицированном виде. В рамках этого способа описание модели ЛРД строится следующим образом. В модели определяются базовые множества SC = {scj, SC2, •..} — конечное и непустое множество контекстов безопасности, А = {г, w,...} — конечное и непустое множество типов доступа, а также определяется предикат предоставления доступа Ди над множеством SC х SC х А.

Определение 3. Тройку Мд = (SC, А, Ац) назовем унифицированной моделью ЛРД на основе контекстов безопасности.

Для того, чтобы записать некоторую другую модель ЛРД М в рамках такого способа необходимо определить два отображения:

^м '• Sm SC — отображение субъектов доступа из М на контексты безопасности в унифицированном описании;

rffl : Ом —> SC — отображение объектов доступа из М на контексты безопасности в унифицированном описании.

Множество типов доступа остается неизменным: А = Аи-Такие отношения должны удовлетворять следующему свойству: предикат предоставления доступа должен сохраняться, то есть

Ve 6 Vo € Ow УаеЛ: Ам(е,о,а) = Аи(т$(з),т(°\о),а). (1)

Определение 4. Пусть задана модель логического разграничения доступа М = {Sm,Om>Am,Am) и определены множество SC и отображения : Sm -> SC и : Ом —> SC. Пусть выполнено условие (1). В таком случае будем считать, что модель логического разграничения доступа М может быть записана в унифицированном виде.

Для ряда традиционно используемых и современных моделей ЛРД, а именно — моделей ЛРД с использованием матрицы доступа и списков доступа, базовых многоуровневых - и базовых ролевых моделей ЛРД, моделей Туре Enforcement, Role Compatibility и grsecurity/RBAC, автором представлены

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

Как отмечалось ранее, основными моделями ЛРД, для анализа которых автором разрабатывается способ проверки требований по безопасности, являются те модели, которые реализуются механизмами защиты в современных Unix-подоб-ных ОС. Как правило, с помощью подобных механизмов ограничивается доступ к объектам (например, к объектам файловых систем), на множестве которых задана некоторая иерархическая структура. Особенности подобной структуры необходимо принимать во внимание при формировании подлежащей анализу модели ЛРД. По этой причине автором предложен способ формального описания моделей ЛРД, позволяющих учитывать древовидную иерархию, заданную на множестве объектов доступа. Он не является единственно возможным способом задания древовидной иерархии объектов доступа в модели ЛРД, однако позволяет учесть особенности правил ЛРД к объектам файловых систем в современных Unix-подобных ОС. Пусть задана модель ЛРД M = (S, О, А, А). Зададим отношение иерархии на множестве О и продемонстрируем, как построить такую модель ЛРД М', для которой будут выполнены следующие свойства:

• доступ к каждому объекту о € О в рамках ее правил будет разрешен только в том случае, если р'азрешен доступ к каждому из объектов, которые стоят выше в иерархии, чем объект о;

• если предыдущее условие выполнено, то доступ к объекту будет разрешен или запрещен по тем же правилам, что и в модели ЛРД М.

Определим функцию parent : О —>• О U {None}, которая будет сопоставлять каждому объекту о € О другой объект р 6 О, который является контейнером, содержащим объект о, либо выделенную константу None в случае, если о является корневым элементом в древовидной иерархии.

Определение 5. Пусть задано конечное и непустое множество О, а также функция parent : О -> О U {None}. Путем в множестве О по отношению к функции parent назовем конечную последовательность тт = ooOj... оп такую, что о,- 6 О, i = 0,..., п и parent(o{) = o;+i, г = 0,..., п — 1. Функция parent задает, древовидную иерархию на множестве О, если выполнены следующие условия:

• существует единственный элемент orooi € О (называемый корневым элементом в иерархии), такой что parent(oroot) — None;

• для любого о £ О существует единственный путь 7r = o0oi... о„, такой что

OQ = О И Оп = Oroot.

Автором предложен способ, как с помощью заданной в соответствии с определением 5 функции parerit по модели ЛРД M = {S, О, А, Д) построить модель M ¡¡иг = {S, О, Ля.еп Ащег, parent), которая будет учитывать древовидную иерархию на множестве объектов доступа О описанным ранее способом.

Определение 6. Пусть задана модель ЛРД M = (S, О, А, Д), а также определена функция parent, задающая древовидную иерархию на О. Пусть Amer = Ли{аг}, где дополнительный тип доступа ах содержательно означает возможность проведения операций над элементами контейнера в заданной древовидной иерар-

хии, а модель ЛРД М расширена до модели М' = (S, 0,Ащег, А'). При этом A'(s, о, а) = A(s, о, а) для всех s G S, о е О и а в А. Определим предикаты Aparent и А'Шег на множествах S х О X Ащег и 5 х (О Li {None}) х Атег соответственно:

Определим предикат Ащег на множестве 5 х О х Ащег как совпадающий с предикатом А'Шег. Тогда модель ЛРД Мщег = (S, О, Анч'еп Д//1ег, parent) назовем расширением модели ЛРД M = (S, О, А, А), учитывающим древовидную иерархию, заданную функцией parent.

Определение 6 корректно, то есть предикат предоставления доступа в расширенной модели ЛРД может быть вычислен, причем однозначным образом. Такое свойство гарантируется единственностью пути от объекта доступа к корневому элементу древовидной иерархии (определение 5).

Автором предложены формальные описания моделей ЛРД, которые используются в современных Unix-подобных операционных системах, а именно — традиционная модель прав доступа «Unix permissions», модель Type Enforcement для механизмов Security-Enhanced Linux (SELinux), модель Role Compatibility для механизмов Rule-Set Based Access Control (RSBAC), ролевая модель для набора механизмов grsecurity. Для двух моделей ЛРД, которые реализуются механизмами защиты grsecurity и RSBAC в ядре ОС Linux, а именно — моделей grsecurty/RBAC и Role Compatibility, автором доказаны утверждения об их представлении с помощью логико-языковых средств модели ЛРД Type Enforcement, используемой в системе SELinux.

Глава 3 посвящена новому, разработанному автором, методу объединения формальных моделей логического разграничения доступа. Отмечается актуальность задачи согласования моделей при анализе компьютерных систем, отдельные компоненты которых используют различные механизмы логического разграничения доступа. В первую очередь разработанный метод ориентирован на объединение моделей ЛРД, используемых в Unix-подобных ОС, в том числе — традиционной модели Unix Permissions и модели Type Enforcement. Необходимость объединения таких моделей в процессе их исследования на предмет выполнения требований по безопасности диктуется потребностями в их совместном использовании в современных сложно организованных компьютерных системах, включая одновременное использование нескольких механизмов ЛРД в операционных системах и в сервисах прикладного уровня. Однако, указанной областью применения использование предлагаемого способа не ограничивается. Например, в процессе функционирования больших распределенных информационно-вычислительных систем, состоящих из нескольких отдельных, возможно, автономно эксплуатируемых подсистем, возникает потребность в совместном использовании информационных ресур-

если pareui(o) = None;

(2)

если о = None; иначе,

(3)

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

При согласовании моделей ЛРД необходимо принимать во внимание следующие аспекты:

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

• комбинирование правил доступа в том случае, если некоторый субъект или объект доступа одновременно используется в нескольких моделях ЛРД (например, принадлежит нескольким подсистемам);

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

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

Определение 7. Пусть заданы модели ЛРД М{ — (5С;,Л;,Д;), г = 1,...,к согласно определению 3. Модель ЛРД М = (£С, А, Д) назовем объединенной моделью ЛРД для М\,..., Мк, если для этого набора моделей заданы следующие множества, отображения и предикаты:

• & : Б С, ->• БС^ = С БС, г — 1 взаимно однозначные отображения контекстов безопасности;

• ¿,5 = г ф ] — множество типов доступа от субъектов в модели М{ к объектам в модели Му,

• г,з = 1,..., к, з — предикаты над множествами БС^ х БС^ х задающие правила, по которым определяется возможность доступа

от контекстов безопасности в модели М; к контекстам безопасности в модели Му

• Д?, I £ г^1'"'^, |/| ^ 2 — предикаты над множествами (П.е/^^) х (Гке/5^0) х (и.е/^«)' задающие правила предоставления доступа на множествах контекстов безопасности, принадлежащих нескольким объединяемым моделям ЛРД,

а также выполняются условия

5С= IJ у A; U (J ) ; (4)

¡=1 ,...,* . \i=l,...,fc / \ij=l,...,Jt; /

A(scj, sc2, a) = Ai 1(sc1), ^ 1(sc2), a) A a e Д- для всех scb sc2 S SC» \ (u;=1.....se«>) , i =

(5)

(6) (7)

A(scj, sc2, a) = Д?(sci, sc2, а), если sci, sc2 € (П;е/ SC^),

«б(Ц61 Ai), где/ег^-Л, |/|>2;

A(sci, sc2, a) = A;-»j, для всех scj € SC^, sc2 € SC^, a Ç Ai_>j, где i,j e {1, - -.,Л},» 7й J-

Рассмотрим ряд предлагаемых автором операций (действий) по согласованию моделей логического разграничения доступа. Каждая такая операция проводится над несколькими моделями ЛРД. Ее результатом является новая модель ЛРД. К предлагаемым операциям по согласованию моделей ЛРД относятся:

• выражение одной модели ЛРД через другую;

• объединение моделей ЛРД без внесения дополнительных доступов («слияние» моделей ЛРД);

• объединение моделей ЛРД над совпадающими множествами субъектов и объектов доступа с помощью комбинирования предикатов предоставления доступа;

• согласование моделей ЛРД с помощью операции «обобщенного слияния», объединяющей операции «слияния» моделей и комбинирования предикатов предоставления доступа;

• объединение моделей ЛРД с использованием дополнительных доступов между субъектами и объектами доступа в разных, подлежащих объединению моделях (операция «связывания» моделей ЛРД).

В первую очередь такие операции ориентированы на применение к тем моделям ЛРД, которые реализуются механизмами защиты в Unix-подобных ОС. Операции комбинирования предикатов и «обобщенного слияния» используются для объединения моделей ЛРД, заданных над пересекающимися множествами субъектов и объектов доступа. Примером таких моделей являются совместно используемые модели Unix Permissions и Type Enforcement. Операция «связывания» применяется для согласования тех моделей ЛРД, множества субъектов и объектов доступа в которых не пересекаются. В качестве примера пары таких совместно используемых моделей ЛРД следует отметить модель ЛРД, действующую в ядре ОС, и модель ЛРД для информационных ресурсов в некотором приложении, функционирующем под управлением ОС. Остановимся более подробно на двух операциях согласования, играющих ключевую роль в предлагаемом автором методе, а именно — на операциях «обобщенного слияния» и «связывания» моделей ЛРД. Представим формальные определения этих операций и ряд доказанных автором утверждений об их свойствах.

Определение 8. Пусть заданы модели ЛРД Мх = (SC\, Ai, Д5) и М2 = (SC2, А2, Д2), а также заданы две одноместные операции opl, ор2 и одна двухместная операция ор над булевыми аргументами. Назовем модель ЛРД М = (SG, А, Д) результатом обобщенного слияния моделей ЛРД Mi и М2 (введем обозначение: М. — Merge(Mi, М2, ор, opi, ор2)), если выполняются следующие условия:

SC = SCt U SC2 = (,SCi \ SC2) ü (SCi П SC2) ü (SC2 \ SC\); А = АгИ Az; (8)

A(sci, SC2, a) = A¡(sci, sc2, a) A o G A¡ для всех (sci, sc2) G (SCt x SCt) \ ((SCX П SC2) x (SCj П SC2)), i = 1,2;

A(sci,sc2,a) = op(A](sci,sC2,a), A2(sci,sc2,a)) для всех (sci, sc2) G ((SCi П SC2) x (5Ci П SC2)), аеА1Г\А2-, A(scj, sc2, o) = opi (A¡(sci, sc2, a)) для всех (scb sc2) G ((SCi П SC2) x (SCi П SC2)), a G A¡ \ i = 1,2¡

a(5ci, sc2, a) = ложь для всех (sci, sc2) G (SCi x SC2) \ ((5C¡ П SC2) x (5C: n SC2)), a $É Л и (sci,sc2) G (SC2 x.5Ci) \ ((SCi П SC2) x (SCi П SC2)), a $É A2.

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

Лемма 1. (О коммутативности операции обобщенного слияния моделей ЛРД.) Пусть модели ЛРД Mi = (SCi, Ai, Д1) и М2 = (SC2,A2, Д2) дают при выполнении операции обобщенного слияния модель ЛРД М = (SG, А, Д) = GMerge(M\, M2,op,opi,op2) для некоторых операций ор, opi, ор2. Тогда, если ор — коммутативная бинарная операция над булевыми аргументами, a opi = ор2, то М — GMerge(M¡, Mi, ор, ор2, opj).

Лемма 2. (Об ассоциативности операции обобщенного слияния моделей ЛРД.) Пусть заданы модели ЛРД M¡ — (SC¡, A¡, A¡), i = 1,2,3, причем A\ = A2 = Л3 = А, Пусть при выполнении операции обобщенного слияния результатом являются додели Mi¡2 = (SCi$,Ait2, ai,2) = GMerge(M\, М2, ор, opi, ор2) и М2)з = (SC2,3, Л2)з, Д2,з) = GMerge(M2, М3, ор, ор\,ор2) для некоторых булевых операций ор, opi и ор2. Пусть ор — логическое <tИ» или логическое «ИЛИ». Тогда Мц2,з) — GMerge(Mj, Мг,з, ор, opj, op¿) = GMerge(Mii2, Mi, ор, орьорг) = М(1; 2),3.

С использованием результатов лемм 1 и 2 автором доказана теорема о порядке выполнения операций обобщенного слияния.

(9) (10)

(11)

Теорема 1. (О порядке применения операции обобщенного слияния моделей ЛРД.) Пусть заданы модели ЛРД = (£>С,-, Д-, Д,), i = 1,..., к, причем Ах — ... = Аь — А. Пусть ор — логическое «И» или логическое *ИЛШ. Тогда при выполнении операций обобщенного слияния над моделями М{ попарно, вплоть до получения одной итоговой модели ЛРД, результат не зависит от порядка выполнения таких операций.

Другой операцией объединения моделей ЛРД, определяемой автором в главе 3, является операция «связывания» таких моделей.

Определение 9. Пусть заданы модели ЛРД М\ = (БС1}А1, Д2) и М2 = (БС$,А2, Дг), а также заданы следующие множества и предикаты:

• = г ~ 1, ■ ■ ■, П1_»о| — множество типов доступа от сущностей

модели Мг к сущностям модели Л/г;

д

■2-Я

{4

(2-+1)

¿ = 1.

..., — множество типов доступа от сущностей

модели А/г к сущностям модели Мц

• Д'1^2 ~~ предикат над множеством БСх X БС2 х А'х^2> задающий правила разграничения доступа от сущностей модели М\ к сущностям модели М2\

• Д^! — предикат над множеством 5Сг х 5С] х Азадающий правила разграничения доступа от сущностей модели М2 к сущностям модели М\.

Назовем модель ЛРД М\<*2 = (5С1<-у2> А1++21Д1++2) результатом связывания моделей ЛРД Мх и М2 (введем обозначение: — Ыпк(М\, АЛ^, Д'цг! Д^)), если выполняются следующие условия:

SCiH2 = SGx LI SC2\ = Ax<JA2U A[_+2 U

(12)

Ai++2(sci,sc2,a) = Д1(5Сь sc2,a), ложь,

A2{sc1,sc2,a), ложь,

если scj £ SCi, SC2 £ SC\,a £ Ai, если sex 6 SCx,sc2 £ SCx,a £ Ax»2 \ если sei £ SC2,sc2 £ SC2,a £ A2, если sei € SC2, sc2 £ SC2, а £ \ A2, (13)

^1->2(SC1> sc2i a)> если sci € SCx, sc2 £ SC2, я 6 A'x^2, ложь, если sei £ SCi, sc2 £ SC2, а £ Axu2 \ А'х_>2,

^2->i(scii sc2> о), если sej £ SC2, sc2 £ SCx, о £ An-»i> ложь, , если sex € SC2, SC2 £ SCx,a € Ax+>2 \ ^2-n-

Автором сформулированы в виде вспомогательных лемм и доказаны два свойства операции связывания моделей ЛРД.

Лемма 3. (О коммутативности операции связывания моделей ЛРД,.) Пусть модели ЛРД Мх = (SCx, -^l, Ai) и М2 — (SC2, А2, А2) при выполнении операции связывания позволяют получить модель ЛРД Мх+>2 = (5CiU2! Д102) = Link(Mx, М2, A'x^2i А'2_>Х1 Д1-+21 множества

A'2^i и предикаты Д1_»2> удовлетворяют определению 9. Тогда

М1«42 = Ыпк(М2, Ми А'^2, Д^!, А'{_,2), где А'!_ц(зс2, яси а) -

(г,Я е {(1,2), (2,1)}.

Лемма 4. (Об ассоциативности операции связывания моделей ЛРД.) Пусть модели ЛРД М{ — (5С;,Л<, Д;), г = 1,2,3 при выполнении операции связывания приводят к модели ЛРД = Ыпк(М\, М2, А\А'2_>1, Д'1_»2> Д'г-я) = Ам2, Дюг) « = ЫпЦМ2, М3, Д'^,

дз-+г) = (5С2(->з, Дг«з)- Тогда, если М1++(2„з)___= Ыпк{М(2„3), Мь

А(1«2)«з) = Ыпк(М(1^1), М3, А'(Ш2)-»3> Д3-»(1«2))>

причем предикаты Д(1++2)-+3' ^з-+(1н2) определяются однозна.чным образом.

На основе результатов лемм 3 и 4 автором доказана теорема о порядке выполнения операций связывания моделей ЛРД.

Теорема 2. (О порядке применения операции связывания моделей ЛРД.) Пусть заданы модели ЛРД А/; = (¿'Сч, Д, Д<), г = 1, ...,к. Тогда при выполнении операций связывания над моделями М{ попарно, вплоть до получения одной итоговой модели ЛРД, результат не зависит от порядка выполнения таких операций.

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

Теорема 3. Пусть задано множество моделей ЛРДМо — {М, = (5С1, Л, Д,)}, г = 1,..., А; с одинаковыми множествами типов доступа. Пусть множество строится по множеству М{, г ^ 0 следующим образом: (1) производится выбор множества из т ^ 2 моделей М[ — ....

¿4,} с М;

к множеству применяется операция обобщенного слияния с использованием бинарной булевой операции «И» или «ИЛИ», либо операция связывания, в результате получается модель ЛРД М[; (3) строится искомое множество Мц.\ = (М{ \ М.[) и {М-}. Тогда для некоторого го, 1 ^ ¿о < к множество моделей ЛРД М^ будем содержать ровно одну модель ЛРД.

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

• модели ЛРД из М.\ действуют над пересекающимися (например, полностью совпадающими) множествами субъектов и объектов доступа;

• модели ЛРД из М.\ полностью независимы по субъектам и объектам доступа.

Первый случай характерен для объединения результатов одновременного использования нескольких механизмов ЛРД над одними и теми же множествами субъектов и объектов доступа. В качестве примера такого случая следует отметить совместное использование модели Type Enforcement и традиционной модели прав доступа Unix-подобных ОС в механизмах защиты SELinux. В этом случае производится операция обобщенного слияния. Второй случай возникает при одновременном использовании не связанных явным образом моделей ЛРД, например, в операционной системе и в программном сервисе, работающем под управлением этой ОС. В таком случае представляется целесообразным использование операции связывания.

Разработанный автором метод согласования моделей ЛРД используется как необходимый подготовительный шаг при исследовании свойств таких моделей, которые реализуются с использованием механизмов ядра ОС Linux, а также — механизмов ЛРД в прикладных программах. Использование предложенного метода согласования позволяет корректным образом объединить используемые разнородные модели и, тем самым, расширить класс проверяемых свойств безопасности.

В главе 4 рассматривается оригинальный метод спецификации и проверки свойств моделей логического разграничения доступа. Метод основан на использовании алгоритмов теории графов и технологии «верификации на модели» («model checking»). Отмечаются особенности его применения на практике.

Основной областью применения предлагаемого автором метода к спецификации и проверке свойств в моделях ЛРД является исследование свойств безопасности таких моделей, которые используются в современных Unix-подобных операционных системах. Применение разрабатываемого метода не ограничивается указанной областью и расширяется на задачи проверки других моделей логического разграничения доступа. Такое расширение может быть произведено с учетом результатов, изложенных в главах 2 и 4. Ключевой особенностью нового метода, отличающего его от других решений в этой области, является возможность учета иерархической структуры на множестве объектов доступа при автоматизированной проверке свойств. Общая задача проверки свойств моделей ЛРД в рамках создаваемого метода ставится следующим образом. В качестве входных данных предоставляются:

• модель ЛРД, правила которой сформулированы с помощью способа унифицированного описания, который предложен автором в главе 2;

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

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

процедура доказательства и построение контрпримеров ориентированы на выполнение в автоматизированном режиме.

В качестве базового свойства, на котором демонстрируется применение методов верификации, выбрано следующее требование: при заданных классах сущностей модели Ei, £2 и Е3 любой информационный поток от сущности из Е\ к сущности из Е2 проходит через одну из сущностей £73.

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

• сбор данных о конфигурации механизмов ЛРД;

• представление полученных данных в виде формальной модели;

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

• проведение проверки выполнения свойств в модели;

• интерпретация результатов с позиции настроек механизмов ЛРД.

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

Автором разработаны и представлены в работе:

• способ построения основной модели для проверки, а именно — модели Крипке, состояния которой соответствуют производимым доступам;

• способ спецификации типовых требований безопасности, предъявляемых к моделям ЛРД, на основе линейной временнбй логики;

• два метода проверки выполнения таких требований с использованием специализированных алгоритмов верификации на модели («model checking») и интерпретации полученных результатов.

Автором предложены два метода проверки выполнения заданных требования по безопасности. Первый го них использует в своей основе универсальные средства верификации на модели, такие как NuSMV2. Второй — основан на предлагаемом автором специализированном алгоритме проверки, который использует методы теории графов. Применение универсальных средств верификации на модели, как правило, является вычислительно трудоемким процессом по причине того, что класс свойств, которые могут быть проверены с помощью таких средств, достаточно широк. В таком контексте целесообразной представляется разработка специализированных алгоритмов, предоставляющих возможность проверить в исследуемой модели ЛРД более узкий класс свойств, вместе с тем позволяющих сделать процесс такой проверки более эффективным. Опишем предлагаемый автором алгоритм проверки свойств о прохождении информационного потока. Отметим, что проверка такого свойства может быть осуществлена с использованием алгоритмов на графе доступов, включая традиционные алгоритмы вычисления возможности доступа в классической модели «take-grant» и ее расширенном ва-

рианте,6 а также с использованием современных методов исследования графа доступов.7 Предлагаемый автором алгоритм формулируется в рамках способа унифицированного описания моделей ЛРД и ориентирован на проверку требований безопасности к тем моделям ЛРД, которые используются в Unix-подобных ОС.

Определение 10. Пусть задана модель ЛРД М — (SC, А, А). Назовем состоянием системы переходов тройку sei, sc2, а, где sei, sc2 € SC, а € А. Корректным состоянием системы переходов назовем такое состояние, для которого истинен предикат Д(вС2, SC2, а), если а является доступом на запись, либо истинен предикат Д(вС2, sei, а), если а является доступом на чтение.

Пусть на множестве всех корректных состояний (обозначим его через S) задано отношение R такое, что

(sa = (sca, 1, SCa:2, йа), Sb — (sCßti, SCßfi, aß)) & R <==> 3Ca 2 = SCf3,1.

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

(0) 7 := {(s, None) : s = (sei, sc2, a) e S, sci € ¿?i};

(1) V:=0;

(2) пока |.F| ф 0, выполнять шаги (3)-(7):

(3) выбрать / e 7, f= (si, s0), si = (scx^.a), 7 := 7\ {/};

(4) если SC2 £ Ез, то перейти к шагу (2);

(5) если {(sa, ар) 6 V : sa = sj = 0, то V := V U {(sb s0)}i

(6) если sc2 € E2, то выйти с возвращаемым значением (V,/);

(7) 7 \= 7 U {(sca, seß) : (scy,sca) £ Я};

(8) выйти из алгоритма с возвращаемым значением (V, None).

Такой алгоритм является модификацией алгоритма поиска «в глубину» в графе, который задается множеством вершин S и отношением инцидентности R. По причине конечности множеств 5 и R алгоритм всегда завершает свою работу. Возвращаемое значение алгоритма, а именно — пара (V,/), содержит последовательность состояний системы переходов, на которой не выполняется проверяемое свойство прохождения информационных потоков. В случае, если рассматриваемое свойство выполняется в исследуемой модели ЛРД, / = None. Если / ф None,

6М. Harrison, W. Ruzzo, J. Ullman. Protection in Operating Systems. // Communications of the ACM. — 1976. - № 19(8). - pp. 461-171.

A. Jones, R. Lipton, L. Snyder. A Linear Time Algorithm for Deciding Security. // Proc. I7th Annual Symp. on the Foundations of Computer Science. — 1976. — pp. 33—41.

J. Franb, M. Bishop. Extending the Take-Grant Protection System. — Department of Computer Science. — University of California at Davis. — 199S.

7П. H. Девянин. Анализ безопасности управления доступом и информационными потоками в компьютерных системах. — М.: Радио и связь, 2006. — 176 с.

Д. Н. Колегов. Применение ДП-моделей для анализа защищенности сетей. // Прикладная и дискретная математика. — 2008. — № 1. — 71-87.

то / содержит состояние системы переходов, в котором реализуется последний элементарный информационный поток. Множество V содержит пары (si,so), для которых выполняется свойство (so, sj) € R. Таким образом, по значению / и парам (sj, sq) £ V может быть восстановлена последовательность операций, приводящих в исследуемой модели ЛРД нарушения подлежащего проверке свойства.

В главе 5 излагаются предложенный автором способ реализации программного комплекса средств для исследования моделей логического разграничения доступа на предмет выполнения требований по безопасности. Назначением разрабатываемого программного комплекса является анализ выполнения требований безопасности (свойств), которые формулируются в виде ограничений на информационные потоки в моделях логического разграничения доступа. Комплекс предназначен для определения того факта, выполняется ли заданное свойство из указанного класса в модели ЛРД, построенной на основе сбора данных о конфигурации механизмов ЛРД. Комплекс ориентирован на исследование конфигурации таких механизмов в Unix-подобных операционных системах на основе ядра ОС Linux.

Программный комплекс состоит из следующих компонентов (рис. 2):

• средства сбора данных о настройках механизмов ЛРД и преобразования таких настроек механизмов ЛРД во внутреннее представление моделей ЛРД;

• генераторы внутреннего представления моделей ЛРД;

• средство согласования моделей ЛРД;

• средства проверки свойств в моделях ЛРД;

• средства интерпретации результатов проверки.

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

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

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

разграничения доступа в Unbc-подобных ОС и механизмы SELinux, реализующие модель Type Enforcement. Дистрибутив ОС обладает программными средствами и библиотеками, необходимыми для сбора данных о настройках механизмов ЛРД, а в процессе сбора данных о настройках механизмов ЛРД, их изменение не производится. Состав такого дистрибутива расширяется за счет добавления веб-сервера и работающей поверх него веб-системы управления контентом. Механизмы защиты веб-системы реализуют отдельную модель ЛРД, не связанную с моделями ЛРД, которые выполняются непосредственно механизмами операционной системы. В качестве такой модели выбрана модель ЛРД класса RBACq.

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

• проверка выполнения требования изоляции пользователей при использова-

.нии традиционных средств разграничения доступа в Unix-подобных ОС;

• проверка выполнения требования изоляции сервисов в комбинированной модели ЛРД;

• проверка выполнения требования ограничения доступа к средствам управления настройками механизмов ЛРД при использовании комбинированной модели ЛРД;

• проверка выполнения требования изоляции пользователей веб-системы управления контентом.

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

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

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

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

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

• Предложено и прошло тестовые испытания математическое и программное обеспечение, составляющее основу комплекса средств для анализа моделей логического разграничения доступа, которые реализуются механизмами ЛРД в Unix-подобных ОС, на предмет выполнения ими требований по безопасности, а именно — ограничений на допустимые информационные потоки.

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

Публикации по теме диссертации

[1] К. А. Шапченко. Способ проверю! свойств безопасности в моделях логического разграничения доступа с древовидной иерархией объектов доступа. // Информационные технологии. — М.: Новые технологии. — 2009. — №10. — С. 13-17.

[2] В. А. Васенин, К. А. Шапченко. Проблемы управления персональными данными. // Открытые системы. — М.: «Открытые системы».

— 2009. — № 9. — С/ 42-45. (К. А. Шапченко принадлежат результаты по систематизации подходов к использованию программно-технических средств защиты).

[3] Ф. М. Пучков, К. А. Шапченко. Статический метод анализа программного обеспечения на наличие угроз переполнения буферов. // Программирование. — М.: «Pleiades Publishing» — 2005.— № 4.

— С. 19-34. (К. А. Шапченко принадлежат результаты по подготовке программ к исследованию на предмет наличия ошибок вида «переполнение буфера»).

[4] К. А. Шапченко. К вопросу о средствах ОС Linux для управления доступом при использовании ролевых политик безопасности. // Математика и безопасность информационных технологий. Материалы конференции в МГУ 2-3 ноября 2005 г., - М.: МЦНМО. - 2006. - С. 257-281.

[5] Набор специализированных дистрибутивов ОС Linux с повышенными требованиями к защищенности. / В. А. Васенин, К. А. Шапченко, А. Н. Водомеров,

A. В. Инюхин, О. О. Андреев, В. Б. Савкин. // Свидетельство о государственной регистрации программы для ЭВМ № 2006613706. — 2006.

[6] В. А. Васенин, К. А. Шапченко, О. О. Андреев. Математические модели и механизмы логического разграничения доступа в операционной системе Linux: текущее состояние и перспективы развития. // Материалы Второй международной научной конференции по проблемам безопасности и противодействия терроризму. Пятая общероссийская научная конференция «Математи-каи безопасность информационных технологий» (МаБИТ-06). МГУ имени М.

B. Ломоносова, 25-26 октября 2006 г. - М.: МЦНМО. - 2007. - С. 159-171. (К. А. Шапченко принадлежат результаты по исследованию и разработке методов проверки выполнения требований по безопасности в настройках механизмов логического'разграничения доступа).

[7] Ф. М. Пучков, К. А. Шапченко, О. О. Андреев. К созданию автоматизированных средств верификации программного кода. // Материалы Второй международной научной конференции по проблемам безопасности и противодействия терроризму. Пятая общероссийская научная конференция «Математика и безопасность информационных технологий» (МаБИТ-06). МГУ

имени М. В. Ломоносова, 25-26 октября 2006 г. - М.: МЦНМО. - 2007. - С. 401-439. (К. А. Шапченко принадлежат результаты по подготовке программ к исследованию на предмет наличия ошибок вида «переполнение буфера»).

[8] К. А. Шапченко, О. О. Андреев, В. Б. Савкин, А. А. Иткес. Специализированные дистрибутивы операционной системы Linux с повышенным уровнем защищенности. // Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия. / О. О. Андреев и др. Под ред. В. А. Васенина. - М.: МЦНМО. - 2008. - 607 с. - С. 168-216. (К. А. Шапченко принадлежат доказательства теорем о представлении одной модели ЛРД через другую, а также результаты по исследованию и разработке методов проверки выполнения требований по безопасности в настройках механизмов логического разграничения доступа).

[9] К. А. Шапченко, О. О. Андреев. Подход к управлению настройками механизмов безопасности в дистрибутивах ОС Linux. // Материалы Четвертой международной научной конференции по проблемам безопасности и противодействия терроризму. Московский государственный университет им. М. В. Ломоносова. 30-31 октября 2008 г. Том 2. Материалы Седьмой общероссийской научной конференции «Математика и безопасность информационных технологий » (МаБИТ-2008). - М.: МЦНМО. - 2009. - С. 153-160. (К. А. Шапченко принадлежит подход к интеграции методов проверки выполнения требований по безопасности в настройках механизмов ЛРД в процессы проектирования и эксплуатации дистрибутивов операционных систем).

[10] К. А. Шапченко. Современные методы проверки свойств безопасности в моделях логического разграничения доступа. // Проблемы информатики, — Новосибирск: НГТУ. - 2009. - № 3. - С. 22-32.

[11] Способ генерации баз данных для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Ф. М. .Пучков, К. А. Шапченко. // Патент на изобретение № 2364929. - 2009.

[12] Способ генерации баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Ф. М. Пучков, К. А, Шапченко. // Патент на изобретение № 2364930. - 2009.

[13] Способ генерации баз данных и баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Ф. М. Пучков, К. А. Шапченко. // Патент на изобретение № 2373569. - 2009.

[14] Способ верификации программного обеспечения распределенных вычислительных комплексов и система для его реализации. / Ф. М. Пучков, К. А. Шапченко. // Патент на изобретение № 2373570. — 2009.

Подписано в печать ¡0

Формат 60x90 1/16. Усл. печ. л. 15 Тираж /¿/¿7экз. Заказ 02

Отпечатано с оригинал-макета на типографском оборудовании механико-математического факультета МГУ имениМ. В. Ломоносова

Введение.

Глава 1. Исследование моделей логического разграничения доступа

1.1. Актуальность проведения исследований в области разработки и практического использования моделей логического разграничения доступа

1.2. Термины и определения

1.3. Задачи разработки и использования математических моделей логического разграничения доступа.

1.4. Задачи, исследуемые в настоящей работе

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

1.6. Выводы.

Глава 2. Описание моделей логического разграничения доступа

2.1. Основные положения разработки и формального описания моделей логического разграцичения доступа (ЛРД).

2.2. Унифицированный способ описания статической части правил ЛРД в моделях логического разграничения доступа.

2.3. Учет древовидной иерархии на объектах доступа в модели ЛРД.

2.4. Формальное описание моделей ЛРД, положенных в основу механизмов защиты в ядре ОС Linux.

2.5. Выводы . . . /.

Глава 3. Метод согласования моделей логического разграничения доступа

3.1. Постановка задачи согласования моделей разграничения доступа

3.2. Операции согласования моделей логического разграничения доступа

3.3. Метод согласования моделей логического разграничения доступа

3.4. Выводы.

Глава 4. Спецификация и проверка свойств безопасности в моделях логического разграничения доступа

4.1. Предпосылки для создания метода исследования моделей логического разграничения Доступа на предмет выполнения требований по безопасности

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

4.3. Метод спецификации и проверки свойств моделей логического разграничения доступа на предмет выполнения требований безопасности.

4.4. Специализированный алгоритм проверки свойств прохождения информационного потока.

4.5. Замечания о практическом применении разработанного метода проверки свойств моделей.

4.6. Выводы.

Глава 5. Программная реализация комплекса средств для анализа моделей логического разграничения доступа на предмет выполнения требований по безопасности

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

5.2. Программная архитектура создаваемого набора инструментальных средств

5.3. Компоненты программного комплекса для исследования свойств безопасности в моделях ЛРД.

5.4. Тестовые испытания: применение к разработке и использованию дистрибутивов операционных систем.

5.5. Выводы

Актуальность работы. Механизмы логического разграничения доступа к информационным активам, коммуникационным и вычислительным ресурсам (далее для краткости изложения используются сочетание «логическое разграничения доступа» и сокращение «ЛРД») являются важной составляющей современных компьютерных систем, к защищенности которых предъявляются повышенные требования [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 и программного обеспечения с открытым исходным кодом. В процессе тестовых испытаний показаны функциональные возможности разработанного программного комплекса по анализу настроек механизмов логического разграничения доступа при создании специализированных дистрибутивов ОС.

Внедрение результатов работы. Результаты работы нашли применение в процессе выполнения проектов: «Методы и средства противодействия компьютерному терроризму: механизмы, сценарии, инструментальные средства и административно-правовые решения» (НИР12005-БТ-22.2/001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям науки и техники»); «Разработка подходов к обеспечению информационной безопасности автоматизированных систем государственного управления на основе использования в их составе программного обеспечения с открытым кодом» (НИР 2007-4-1.4-15-04-001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2012 годы»). Получено свидетельство об официальной регистрации программы для ЭВМ «Набор специализированных дистрибутивов ОС Linux с повышенными требованиями к защищенности» (свидетельство № 2006613706).

Апробация работы. Результаты работы докладывались на научных конференциях «Математика и безопасность информационных технологий» (2005-2008 гг.), «Ломоносовские чтения» (2006-2009 гг.), «Актуальные проблемы вычислительной математики» (2006 г.), «Третья'международная конференция по проблемам управления» (2006 г.), на семинаре «Проблемы современных информационно-вычислительных систем» под руководством д.ф.-м.н., проф. В. А. Васенина (механико-математический факультет МГУ имени М. В. Ломоносова, 2005, 2007, 2009 гг.).

Публикации. По теме диссертации опубликовано 14 работ, из которых 3 статьи [7,19,31] — в журналах из перечня ведущих рецензируемых изданий, рекомендованных ВАК. Материалы работы вошли в главу 3 опубликованной в 2008 году коллективной монографии «Критически важные объекты и кибертерроризм. Часть 2. Аспекты программной реализации средств противодействия» под ред. В. А. Васенина [28].

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

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

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

ОС Linux.

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

В главе 4 рассматривается оригинальный подход к спецификации и проверке свойств моделей логического разграничения доступа. Такой подход основан на использовании методов теории графов, технологии «верификации на модели» («model checking») и элементов логического программирования. Отмечаются особенности его применения на практике.

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

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

5.5. Выводы

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

Целевой областью применения созданного комплекса является организация аудита свойств безопасности в дистрибутивах Unix-подобных операционных систем с повышенным уровнем защищенности. Созданная первая версия программного комплекса демонстрирует возможность применения предлагаемых алгоритмов проверки свойств в моделях ЛРД на практике.

Представленный набор примеров составляет программу тестовых испытаний для созданных программных средств анализа программной реализации механизмов ЛРД и заданной для таких механизмов конфигурации на предмет выполнения требований безопасности. Результаты тестовых испытаний демонстрируют возможность применения разработанного метода проверки выполнения свойств безопасности в моделях ЛРД на практике. Тестовые примеры позволяют оценить возможности масштабирования, в том числе — в целях оценки эффективности алгоритмов и средств проверки выполнения требований безопасности в автоматизированных системах с большим числом субъектов и объектов доступа.

Заключение

В рамках диссертационной работы получены следующие результаты.

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

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

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

• Предложено и прошло тестовые испытания математическое и программное обеспечение, составляющее основу комплекса средств для анализа моделей логического разграничения доступа, которые реализуются механизмами ЛРД в Unix-подобных ОС, на предмет выполнения ими требований по безопасности, а именно — ограничений на допустимые информационные потоки.

1. О. О. Андреев. Сравнение ролевой и дискреционной модели разграничения доступа // Материалы конференции МаБИТ-04, Москва, 2005 г. — М.: МЦНМО, 2006. — С. 284-291.

2. О. О. Андреев. Язык описания моделей разграничения доступа и его реализация в ядре операционной системы Linux. // Материалы конференции МаБИТ-05, Москва, 2006 г. М.: МЦНМО, 2007. - С. 305-321.

3. В. А. Васенин. Проблемы математического, алгоритмического и программного обеспечения компьютерной безопасности в Интернет // Материалы конференции Ма-БИТ-03, Москва, 2003 г. М.: МЦНМО, 2004. - С. 111-143.

4. В. А. Васенин. Информационная безопасность критических объектов: управление, технологии, кадры. // Открытые системы, № 5, 2009. — М.: «Открытые системы», 2009.

5. В. А. Васенин, К. А. Шапченко. Проблемы управления персональными данными. // Открытые системы, № 9, 2009. — М.: «Открытые системы», 2009. — С. 42-45.

6. Ф. С. Воройский. Информатика. Новый систематизированный толковый словарь-справочник (Введение в современные информационные и телекоммуникационные технологии в терминах и фактах). — 3-е изд., перераб. и доп. — М.: ФИЗМАТЛИТ, 2003. 760 с.

7. В. А. Галатенко. Основы информационной безопасности. Курс лекций. / Под редакцией академика РАН В. Б. Бетелина. — 4-е изд. — М.: Интернет-Университет Информационных Технологий; БИНОМ. Лаборатория знаний. — 2008. — 205 с.

8. Н. А. Гайдамакин. Разграничение доступа к информации в компьютерных системах. — Екатеринбург: Изд-во Уральского университета. — 2003. — 328 с.

9. В. А. Герасименко, А. А. Малюк. Основы защиты информации. — М.: ООО «Ин-комбук». — 1997.

10. А. А. Грушо, Э. А. Применко, Е. Е. Тимонина. Теоретические основы компьютерной безопасности. — М.: Academia. — 2009. — 272 с.

11. П. Н. Девянин. Анализ безопасности управления доступом и информационными потоками в компьютерных системах. — М.: Радио и связь, 2006. — 176 с.

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

13. Д. Н. Колегов. Применение ДП-моделей для анализа защищенности сетей. // Прикладная и дискретная математика. — 2008. — № 1. — 71-87.

14. Т. Кормен, Ч. Лейзерсон, Р. Ривест, К. Штайн. Алгоритмы: построение и анализ. / Под ред. И. В. Красикова. — 2-е изд. — М.: Вильяме, 2005. — 1296 с.

15. Ф. М. Пучков, К. А. Шапченко. К вопросу о выявлении возможных переполнений буферов посредством статического анализа исходного кода программ. // Материалы конференции МаВИТ-04. М.: МЦНМО, 2005. - С. 347-359.

16. Ф. М. Пучков, К. А. Шапченко. Статический метод анализа программного обеспечения на наличие угроз переполнения буферов. // Программирование. — 2005.— №4. С. 19-34.

17. Способ генерации баз данных для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Ф. М. Пучков, К. А. Шапченко. // Патент на изобретение № 2364929. — 2009.

18. Способ генерации баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Ф. М. Пучков, К. А. Шапченко. // Патент на изобретение № 2364930. — 2009.

19. Способ генерации баз данных и баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации. / Ф. М: Пучков, К. А. Шапченко. // Патент на изобретение № 2373569. 2009.

20. Способ верификации программного обеспечения распределенных вычислительных комплексов и система для его реализации. / Ф. М. Пучков, К. А. Шапченко. // Патент на изобретение № 2373570. — 2009.

21. Ф. Харари. Теория графов. — М.: Издательство «Мир», 1973.

22. К. А. Шапченко. Способ проверки свойств безопасности в моделях логического разграничения доступа с древовидной иерархией объектов доступа. // Информационные технологии. №10, 2009. — М.: Новые технологии, 2009. — С. 13-17.

23. К. А. Шапченко. Современные методы проверки свойств безопасности в моделях логического разграничения доступа. // Проблемы информатики. — №3, 2009. —

24. Новосибирск: НГТУ, 2009. — С. 22-32.

25. А. Ю. Щербаков. Современная компьютерная безопасность. Теоретические основы. Практические аспекты. — М.: Книжный мир. — 2009. — 352 с.

26. ГОСТ Р ИСО/МЭК 13335-1-2006. Информационная технология. Методы и средства обеспечения безопасности. Часть 1. Концепция и модели менеджмента безопасности информационных и телекоммуникационных технологий. — М.: ИПК Издательство стандартов, 2006.

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

28. ГОСТ Р ИСО/МЭК 15408-2-2002. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 2. Функциональные требования безопасности. — М.: ИПК Издательство стандартов, 2002.

29. ГОСТ Р ИСО/МЭК 15408-3-2002. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Требования доверия к безопасности. — М.: ИПК Издательство стандартов, 2002.

30. ГОСТ Р ИСО/МЭК 17799-2005. Информационная технология. Практические правила управления информационной безопасностью. — М.: ИПК Издательство стандартов, 2005.

31. ГОСТ 34.003-90. Информационная технология. Комплекс стандартов на автоматизированные системы. Термины и определения. — М.: ИПК Издательство стандартов, 2005.

32. Защита от несанкционированного доступа к информации. Термины и определения. Руководящий документ ФСТЭК от 30 марта 1992 года / ФСТЭК. — 1992.

33. Автоматизированные системы. Защита от несанкционированного доступа к информации. Классификация автоматизированных систем и требования по защите информации. Руководящий документ ФСТЭК от 30 марта 1992 года / ФСТЭК. — 1992.

34. Средства вычислительной техники. Защита от несанкционированного доступа к информации. Показатели защищенности от несанкционированного доступа к информации. Руководящий документ ФСТЭК от 30 марта 1992 года / ФСТЭК. — 1992.

35. Постановление Правительства Российской Федерации от 17 ноября 2007 г. № 781 «Об утверждении положения об обеспечении безопасности персональных данных при их обработке в информационных системах персональных данных».

36. S. Barker, М. Fernandez. Term rewriting for access control. // In Proc. DBSec2006, volume 4127 in LNOS. Springer-Verlag, 2006. — pp. 179-193.

37. S. Barker, P. J. Stuckey. Flexible access control policy specification with constraint logic programming. // ACM Trans. Inf. Syst. Secur., vol. 6, 2003.

38. D. Bell and L. J. LaPadula. Secure computer systems: Mathematical foundations and model. // Technical Report M74-244. — The Mitre Corporation, 1976.

39. E. Bertino, B. Catania, E. Ferrari, P. Perlasca. A logical framework for reasoning about access control models. // ACM Trans. Inf. Syst. Secur., vol. 6, 2003. — pp. 71-127.

40. K. J. Biba. Integrity Considerations for Secure Computer Systems. — MTR-3153, The Mitre Corporation, April 1977.

41. R. Chandramouli, R. Sandhu. Role Based Access Control Features in Commercial Database Management Systems. // Proceedings of 21st National Information Systems Security Conference,' October 6-9, 1998, Crystal City, Virginia.

42. A. Cimatti, E. Clarke, E. Giunchiglia, et al. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. // Proc. International Conference on Computer-Aided Verification (CAV 2002), July, 2002, vol. 2404, ser. LNCS.

43. E. M. Clarke, O. Grumberg, D. E. Long. Model Checking and Abstraction. // ACM Transactions on Programming Languages and Systems. Vol. 16, N. 5. — ACM Press, 1994. pp. 1512-1542.

44. DoD 5200.28-STD. Department of Defense Standard. Department of Defense Trusted Computer System Evaluation Criteria. — 1983. Электронный ресурс]. URL: http: //www.fas.org/irp/nsa/rainbow/stdOOl.htm.

45. D. J. Dougherty, K. Fisler, S. Krishnamurthi. Specifying and reasoning about dynamic access control policies. // Lecture Notes in Computer Science. — Springer-Verlag, 2006. pp. 632- 646.

46. K. Fisler, S. Krishnamurthi, L. A. Meyerovich, M. C. Tschantz. Verification and change-impact analysis of access-control policies. //In International Conference on Software Engineering, pp. 196-205, May 2005.

47. I. Foster, C. Kesselman, S. Tuecke. The Anatomy of the Grid: Enabling Scalable Virtual Organizations. // International Journal of High Performance Computing Application. —15(3). 2001.

48. Foster, Y. Zhao, I. Raicu, S. Lu. Cloud Computing and Grid Computing 360-Degree Compared. // Proceedings of Grid Computing Environments Workshop GCE'08. — 2008. pp. 1-10.

49. J. Frank, M. Bishop. Extending the Take-Grant Protection System. — Department of Computer Science. — University of California at Davis. — 1996.

50. D. P. Guelev, М. D'. Ryan, P.-Y. Schobbens. Mo del-checking access control policies. //In Information Security Conference, number 3225 in Lecture Notes in Computer Science. Springer-Verlag, 2004.

51. M. Koch, F. Parisi-Presicce. Describing Policies with Graph Constraints and Rules. // In Proc. ICGT02. Springer-Verlag, 2002. - pp. 223-238.

52. N. Li, M. Tripunitara. On Safety in Discretionary Access Control. //In Proceedings of IEEE Symposium on Security and Privacy, May 2005.

53. Т. Moses, extensible Access Control Markup Language (XACML) version 1.0. // Technical report. — OASIS, 2003.

54. M. Nyanchama, S.' Osborn. Access Rights Administration in Role-Based Security Systems. // Database Security VIII: Status and Prospects. — North-Holland, 1994.pp. 37-56.

55. OASIS Security Services (SAML) TC Public Documents, http://www.oasis-open, org/committees/documents.php?wgabbrev=security

56. S. L. Osborn, R. S. Sandhu, Q. Munawer. Configuring role-based access control to enforce mandatory and discretionary access control policies. // Proceedings of ACM Trans. Inf. Syst. Secur. №3(2), 2000. — pp. 85-106.

57. S. L. Osborn. Integrating role graphs: a tool for security integration. // Data Knowl. Eng. №43(3), 2002. pp. 317-333.

58. A. Ott. Mandatory Rule Set Based Access Control in Linux. A Multi-Policy Security Framework and Rol6 Model Solution for Access Control in Networked Linux Systems.1. Shaker Publishing, 2007.

59. A. Ott. The Role Compatibility Security Model. // Nordic Workshop on Secure IT Systems (NordSec), 2002.

60. R. Peri. Specification and Verification of Security Policies. / Dissertation. — The Faculty of the School of Engineering and Applied Science, University of Virginia. — 1996. — 179 P

61. Puchkov, F.; Shapchenko, K. Static Analysis Method for Detecting Buffer Overflow Vulnerabilities // Programming and Computer Software, Volume 31, Number 4, July 2005, pp. 179-189(11).

62. G. Rozenberg, editor. Handbook of Graph Grammar and Computing by Graph Transformation. Vol: 1: Foundations. — World Scientific, 1997.

63. Rule-Set Based Access Control. Электронный ресурс]. Режим доступа: http://www. rsbac. org, свободный. — Электрон, текст, док.

64. В. Sarna-Starosta, S. D. Stoller. Policy analysis for security-enhanced Linux. //In Proceedings of the 2004 Workshop on Issues in the Theory of Security, pages 1-12, April 2004.

65. R. Sandhu. Role-Based Access Control. // Advances in Computers, Vol.46. — Academic Press 1998.

66. R. Sandhu. Lattice-Based Access Models. // IEEE Computer, Vol. 26, N. 11, November 1993, pp. 9-19.

67. R. Sandhu, V. Bhamidipati, Q. Munawer. The ARBAC97 Model for Role-Based Administration of Roles. // ACM Transactions on Information and Systems Security

68. TISSEC), Vol. 2, February 1999.

69. R. Sandhu, P. Samarati. Access Control: Principles and Practice. // IEEE Communications, Vol. 32, N. 9, September 1994.

70. R. Sandhu, E. J. Coyne, H. L. Feinstein, С. E. Youman. Role-based access control models. // IEEE Computer, 29(2):38-47, 1996.

71. M. Schumaher, E. Fernandez-Buglioni, D. Hybertson, F. Buschmann, P. Sommerlad. Security patterns: integrating security and systems engineering. — John Wiley & Sons, 2006.

72. D. Solomon, M. Russinovich. Microsoft Windows Internals, 4th Ed. — Microsoft Press, 2005. 922 p.

73. Spengler В., Increasing Performance and Granularity in Role-Based Access Control Systems: A Case Stiidy in Grsecurity. Электронный ресурс]. Режим доступа: http: //www.grsecurity.net/researchpaper.pdf, свободный. — Электрон, текст, док.

74. G. Holzmann. The,SPIN Model Checker: Primer and Reference Manual. — Addison-Wesley Professional, 2003. — 608 p.

75. Sun Microsystems. RBAC in the Solaris Operating Environment White Paper. Электронный ресурс]. Режим доступа: http://www.sun.com/software/whitepapers/ wp-rbac/wp-rbac.pdf, свободный. — Электрон, текст, док.

76. Н. Wang, S. L. Osborn. Discretionary access control with the administrative role graph model. // SACMAT 2007 Proceedings. pp. 151-156.