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

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

Андреев Олег Олегович Логико-языковые средства описания моделей логического разграничения доступа Специальность 05.13.19 — методы и системы защиты информации, информационная безопасность

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

Москва 2010

Работа выполнена на кафедре вычислительной математики Механико-математического факультета и в Институте проблем информационной безопасности Московского государственного университета имени М. В. Ломоносова.

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

Официальные оппоненты: доктор физико-математических наук, профессор Грушо Александр Александрович доктор технических наук, профессор Заборовский Владимир Сергеевич

Ведущая организация: Научно-исследовательский институт системных исследований РАН

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

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

Автореферат разослан «27» марта 2010 г.

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

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

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

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

Механизмы ЛРД, встроенные в различные компоненты, зачастую обладают соб ственным языком описания набора правил, в соответствии с которыми доступ раз решается или запрещается. Это обстоятельство затрудняет анализ со стороны поль зователя или администратора соответствия механизмов ЛРД, которые реализуют ся в отдельных компонентах сложной системы, положениям безопасного исполь зования ресурсов системы в целом. Отмеченные выше и ряд других недостатков эксплуатирующихся в настоящее время систем стимулируют работы по созданию новых логико-языковых средств описания моделей ЛРД, таких как eXtended Access Control Markup Language. Данные средства предоставляют администратору системы возможность самому определить модель ЛРД, в большей степени соответствующую потребностям защищаемого информационно-вычислительного комплекса, или вы брать необходимую по требованиям информационной безопасности модель среди предлагаемых другими разработчиками. Однако, и это следует отметить, постоян но выполняемые на протяжении всего времени функционирования информацион ной системы проверки на разрешение или запрещение доступа при использовании сложных моделей ЛРД, основанных на такого рода языковых средствах, становятся существенно более затратными в смысле потребляемых при их использовании вы числительных ресурсов, чем при применении более простых моделей. Последнее обстоятельство приводит к замедлению работы информационной системы. Таким Васенин В. А. Проблемы математического, алгоритмического и программного обеспечения компьютерной безопас ности в Интернет. Материалы конференции МаБИТ-03. Москва, 2004. — С. 81–99.

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

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

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

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

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

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

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

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

• разработка алгоритмов анализа (проверки) свойств моделей, представленных на основе разработанного языка;

• реализация программных средств разграничения доступа, основанных на раз работанном языке и повышение их производительности;

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

Цель работы и перечисленные задачи соответствуют положениям паспорта спе циальности 05.13.19 — методы и системы защиты информации, информационная безопасность.

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

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

• Логико-языковые средства (язык), позволяющие эффективно с позиции предъ являемых к ним требований описывать рассматриваемый класс моделей.

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

• Программные средств разграничения доступа, построенные на основе разра ботанного языка и предназначенные для их внедрения в ядро ОС Linux и в программы, написанные на языках C и Python.

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

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

• методы математической логики, включая исчисление предикатов;

• методы дискретной математики, в том числе, теории графов, теории булевых функций;

• методы программной инженерии.

Научная новизна результатов диссертации состоит:

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

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

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

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

Внедрение результатов работы. Результаты работы нашли свое приме нение в процессе выполнения проектов: «Методы и средства противодействия компьютерному терроризму: механизмы, сценарии, инструментальные средства и административно-правовые решения» (НИР 2005-БТ-22.2/001 в рамках ФЦП «Исследования и разработки по приоритетным направлениям науки и техники»).

Получено свидетельство об официальной регистрации программы для ЭВМ «Набор специализированных дистрибутивов ОС Linux с повышенными требованиями к защищенности» (свидетельство № 2006613706).

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

Публикации. По результатам работы опубликовано 7 научных статей, из них — одна статья в журнале из перечня ведущих рецензируемых изданий, рекомендован ных ВАК [1].

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

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

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

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

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

Принятый в России международный стандарт ГОСТ Р ИСО/МЭК 15408 «Инфор мационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий» является одним из ключевых действующих нормативных документов в области обеспечения безопасности ин формационных технологий. В данном стандарте отмечается как необходимость ис пользования механизмов ЛРД (функциональное требование), так и важность управ ления и анализа конфигурации средств защиты в целом (одно из требований до верия). В Руководящих документах ФСТЭК России отмечаются требования по необ ходимости проведения формального доказательства корректности работы механиз мов защиты для подконтрольных объектов с высокими уровнями защищенности.

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

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

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

Bell D., LaPadula L. Secure Computer Systems: Mathematical Foundations, Tenical Report. Mitre Corporation, 1973.

A Guide to Understanding Discretionary Access Control in Trusted Systems, NCSC-TG-003. National Computer Security Center, 1987.

Ferrariolo D., Kuhn R. Role-Based Access Control, // Proceedings of 15th National Computer Security Conference, 1992.

Основы модели Белла-ЛаПадулы формулируются следующим образом:

• субъект не имеет права читать данные из объектов с уровнем секретности вы ше, чем у него;

• субъект не имеет права писать в объекты с уровнем секретности ниже, чем у него.

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

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

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

• невозможно ограничить субъектов-владельцев объектов в предоставлении ими доступа другим субъектам;

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

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

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

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

Во втором разделе первой главы описывается один из представительных языков описания моделей ЛРД общего назначения, которым в настоящее время является eXtended Access Control Markup Language (XACML), принятый в качестве стандарта комитетом Oasis Open. Одним из ключевых понятий, на основе которого формули руются модели в стандарте XACML, является понятие атрибута. Атрибутом являет ся свойство субъекта, объекта, типа доступа или окружения. Каждый атрибут имеет имя и фиксированный тип данных, которые могут в нем содержаться. Разграниче ние доступа производится на основе значений атрибутов субъекта, объекта, типа доступа и среды окружения, которые учитываются при принятии решения о досту пе.

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

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

eXtensible Access Control Markup Language (XACML) Commitee Specication. OASIS Open, 2003. Электронная версия печатной публикации. http://www.oasis-open.org/committees/xacml/ В первом разделе второй главы описываются понятия, на которых основывается предлагаемый автором язык. Основным понятием, на котором базируются модели ЛРД, описывающиеся с использованием этого языка, кроме понятий субъекта, объ екта и типа доступа, является понятие атрибута безопасности, в дальнейшем для краткости именуемого просто атрибутом. Каждый объект, субъект, тип доступа, а также окружение может иметь некоторые задаваемые пользователем или механиз мом ЛРД атрибуты. Под окружением имеется в виду часть информационной систе мы, общая для всех субъектов и объектов, не зависящая от них.

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

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

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

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

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

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

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

• Строится направленный граф, называемый графом зависимостей, вершинами которого являются отдельные модели.

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

• Проверяется существование в графе направленных циклов.

• В том случае, если циклы существует, проверка завершается с ошибкой.

• В противном случае, описания моделей не являются взаимно исключающими.

В работе доказано следующее утверждение.

Утверждение 1.1. Алгоритм проверки наличия взаимных включений корректен, а именно — завершает свою работу за конечное время.

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

• S, множество имен атрибутов субъектов;

• O, множество имен атрибутов объектов;

• E, множество имен атрибутов окружения;

• A, множество имен атрибутов типов доступа;

• V = Boolean Integer Float String Sets Maps, множество значений атри бутов, где Boolean обозначает предопределенный булевый тип, Integer — це лочисленный, Float — вещественный, String — строковый, Sets — объединение типов «множество фиксированного типа» и Maps — объединение множеств типа «ассоциативный массив фиксированного типа»;

• Type S O E A 2V, функция, устанавливающие каждому имени атрибута множество значений, которые этот атрибут может принимать;

• F VV VVV...VV...V..., множество частичных функций с различным ко личеством аргументов, определенных на подмножествах V и возвращающих значения из V.

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

1. Выражениями являются элементы множества S O E A — все возможные имена атрибутов, а также элементы множества V — константы.

2. В том случае, если v1,..., vn — выражения, а f — функция из множества F с количеством аргументов n, то f(v1,..., vn ) является выражением.

Типом выражения v называется множество возможных значений выражения.

Оно определяется следующим образом:

1. Type(v) в том случае, если v принадлежит S O E A;

2. Boolean в том случае, если v является константой из множества Boolean;

3. аналогично определяется тип выражения для остальных констант;

4. множество возвращаемых значений функции f в том случае, если выражение имеет вид f(v1,..., vn ).

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

1. элементы множеств S O E A и V являются правильно типизированными выражениями;

2. в том случае, если v1, …, vn — правильно типизированные выражения, имеющие типы T1, …, Tn, и f — функция из множества F с количеством аргументов n, определенная в том числе на множестве T1... Tn, то f(v1,..., vn ) является правильно типизированным выражением.

В дальнейшем в работе рассматриваются лишь правильно типизированные вы ражения.

Определение 1.2. Условием на атрибуты в указанных выше обозначениях назы вается такое правильно типизированное выражение v, типом которого является Boolean.

На основе данных выше определений правильно типизированного выражения и условия на атрибуты строится определение правила и модели ЛРД.

Определение 1.3. Правилом называется пара (Target, Condition), где Target и Condition — условия на атрибуты. КомпонентаTarget соответствует цели прави ла, Condition — условию правила.

Моделью называется четверка (Target, Models, Alg, Obligations). При этом:

• Target — условие на атрибуты, соответствующее цели модели;

• Models — последовательность правил или моделей, используемых в основной модели;

• Alg — алгоритм комбинирования, один из множества {deny overrides, permit overrides, first applicable};

• Obligations — последовательность пост-действий, представляемых кортежа ми вида (name, attr1,..., attrn ), где name String — вид обязательного действия, attr1,..., attrn S O E A — имена атрибутов, значения которых будут переданы.

Автором показывается, если не рассматривать пост-действия, то приведенная в предыдущем определении тройка (Target;

Models;

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

Теорема 1.1. Для любой модели, задаваемой с помощью языка описания моделей ЛРД, существует условие на используемые в ней атрибуты, которое истинно тогда и только тогда, когда модель разрешает доступ.

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

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

Другим распространенным способом проверки свойств механизма ЛРД является «верификации на модели». Такой класс методов носит название «model eing», в русскоязычных источниках используются наименования «методы верификации моделей» или «методы верификации на модели». Подобные методы основаны на задании модели как системы переходов между состояниями («машины состояний»), для каждого из которых задан набор истинных в нем атомарных высказываний про позициональной логики. Проверяемое свойство специфицируется в виде формулы временной логики, накладывающей ограничения на состояния в форме путей в за данной системе переходов. В зависимости от используемого языка временной ло гики некоторым образом ограничивается последовательность состояний, содержа щихся в допустимых путях системы переходов Существующие методы анализа моделей ЛРД по сути не подходят для моде лей, описанных на разработанном автором языке. Причиной такого несоответствия Ko M., Mancini L.V., Parisi-Presicce F. Decidability of safety in graph-based models for access control. // In European Symposium on Resear in Computer Security, pp. 299–243, 2002.

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

Guelev D., Ryan M.D. и Zhang N. Evaluating access control policies through model eing. Proceedings of Eighth Information Security Conference (ISC05), 2005.

Morisset C., Santana de Oliveira A. Automated Detection of Information Leakage in Access Control. Universite Paris, Vandoeuvre les Nancy, 2007.

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

// Проблемы информатики. — No3, 2009. — 124 Новосибирск: НГТУ, 2009. — С. 22–32.

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

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

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

Определение 1.4. Одна модель ЛРД с формулой разрешения доступа F1 называется более слабой, чем другая, с формулой разрешения доступа F2 в том случае, когда истинно следствие F2 F1. Одна модель ЛРД называется более сильной, чем вторая, если вторая является более слабой, чем первая.

Разработанный автором и представленный в данной работе алгоритм позволяет проверять, является ли одна модель ЛРД более сильной, чем вторая, при опреде ленных ограничениях на подаваемые ему на вход модели. Ограничение налагается на формулы разрешения доступа моделей и, как следствие, на формулы Target и Condition их правил. Оно состоит в том, что множество F функций, на основе кото рого строятся эти формулы, содержит только булевы связки,, ¬, а также операции сравнения =,,,.

Определение 1.5. Назовем литералом одно из следующих выражений:

• булева константа;

• булев атрибут или отрицание булевого атрибута;

• выражение вида (a op b), где a и b — атрибуты или константы, а op — опе рация из множества {=,,, } (то есть, множество разрешенных функций за исключением логических связок).

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

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

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

Дополнительный алгоритм получает на вход конечный набор отношений вида {ai opi bi }, где ai и bi — атрибуты или константы, а opi — одна из функций =,,,.

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

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

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

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

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

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

2. Вершины, которые в соответствии с условиями группы находятся в отноше нии равенства, «склеиваются». В том случае, если «склеиваются» вершины, находящиеся в отношении «не равны», либо вершины, соответствующие раз личным константам, группа является противоречивой.

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

4. В том случае, если в графе существуют направленные циклы, группа является противоречивой.

5. В том случае, если в графе существуют направленные пути, ведущие от мень ше константы к большей или равной, группа противоречива.

6. В противном случае группа является непротиворечивой.

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

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

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

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

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

После рассмотрения дополнительного алгоритма в работе описываются шаги ос новного алгоритма. Его суть заключается в проверке того факта, является ли первая модель более сильной, чем вторая, в предположении что на вход поданы две моде ли ЛРД, удовлетворяющие указанному ограничению. Формула разрешения доступа первой модели будет обозначаться как F1, формула разрешения доступа второй — как F2. Алгоритм в соответствии с определением должен выполнять проверку ис тинности формулы F1 F2, на всех возможных значениях аргументов, которая эк вивалентна проверке тождественной ложности формулы F1 ¬F2, обозначаемой в дальнейшем F. Необходимо отметить, что формула F удовлетворяет тому же огра ничению, что и формулы F1 и F2.

Представленный в работе алгоритм состоит из следующих шагов.

1. Формула F рассматривается как булева формула относительно введенного определения литерала и приводится к виду дизъюнктивной нормальной фор мы с помощью эффективного алгоритма.

2. Каждый из дизъюнктов, полученный на первом шаге, должен быть ложен при любых значениях атрибутов, ложность которого необходимо проверить, вы глядит в общем виде как a1... an (an+1 op1 bn+1 )... (an+k opk bn+k ), где a1,..., an+k, b1, …, bn+k — атрибуты, отрицания атрибутов или константы, а op1, …, opk — операции из разрешенного множества.

Набор отношений (an+1 op1 bn+1 ), … (an+k opk bn+k ) проверяется на противоре чивость представленным выше алгоритмом проверки набора отношений на противоречивость. Если набор противоречив, дизъюнкт всегда ложен, иначе существуют значения атрибутов, при которых дизъюнкт истинен.

Автором доказывается утверждение о корректности разработанного им алгорит ма проверки тождественной ложности формулы.

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

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

Разработанные в рамках диссертации механизмы безопасности в первую оче редь предназначаются для внедрения в специализированные программные дистри бутивы с повышенным уровнем защищенности на базе ядра ОС Linux. В контексте требований существующих нормативно-правовых документов следует отметить, что задача построения таких дистрибутивов непосредственно связана с управле нием функциями безопасности, отдельные требования к которому представлены в ГОСТ Р ИСО/МЭК 15408 «Общие критерии», а именно — в описании класса требова ний FMT («Управление безопасностью»). Создание таких дистрибутивов позволит не только более эффективно проводить изменения настроек механизмов безопасно сти (включая «атрибуты безопасности» в терминологии стандарта), но и предоста вит возможность организовать проверку выполнения ряда требований по безопас ности состояния защищаемой системы до и после таких изменений.

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

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

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

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

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

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

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

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

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

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

Утверждение 1.5. Пусть Target — условие на атрибуты, ограничивающее область применения модели, Target1, …, Targetn — условия на атрибуты, описывающие об ласти применимости входящих в нее правил и моделей. Пусть Additional — усло вие на атрибуты, при этом при любых значениях атрибутов верны следствия Target1 Additional, …, Targetn Additional.

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

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

В работе в виде утверждения представляется формальное определение данного пре образования.

Утверждение 1.6. Пусть Target — условие на атрибуты, ограничивающее область применения модели, Target1, …, Targetn, Targetn+1, …, Targetn+k — условия на атрибу ты, ограничивающие область определения входящих в нее правил и моделей. Пусть Additional1 и Additional2 — условия на атрибуты такие, что при любых значениях атрибутов истинно следствие Additional1 Additional2 = Target. Кроме этого, пусть условие Additional1 Additional2 = False справедливо при любых значениях атрибу тов.

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

Автором приведен сравнительно простой алгоритм эквивалентного преобразо вания моделей ЛРД, основанный на двух представленных выше классах преобразо ваний. Этот алгоритм состоит из двух основных шагов:

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

• разделение на подмодели по принципу принадлежности атрибута диапазону значений.

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

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

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

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

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

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

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

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

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

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

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

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

Всего было сгенерировано три модели с количеством правил — 100, 1000 и 10000, соответственно. В качестве алгоритма комбинирования правил был выбран «прио ритет запрещения», пост-действия отсутствовали.

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

Low Level Virtual Maine, 2009. Электронная версия печатного документа. http://www.llvm.org В следующей таблице представлены результаты применения базовой и опти мизированной версии механизма ЛРД в случае применения метода повышения производительности «эквивалентные преобразования моделей».

Количество правил в Время на разрешение Время на разрешение модели ЛРД запроса на доступ, ба- запроса на доступ, зовая реализация, мс оптимизированная реализация, мс 100 534 1000 5249 10000 52983 Легко заметить, что производительность оптимизированной реализации на по рядки выше базовой, причем причем это различие возрастает при увеличении раз мера модели ЛРД.

В следующей таблице представлены результаты сравнения производительно сти базовой и оптимизированной версии механизма ЛРД в случае использования метода «преобразование в исполняемый код».

Количество правил в Время на разреше- Время на разре модели ЛРД ние запроса на до- шение запроса ступ, базовая реали- на доступ, оп зация, мс тимизированная реализация, мс 100 550 1000 5293 10000 51004 Следует отметить, что производительность оптимизированной реализации в несколько раз выше базовой, хотя и не достигает таких показателей ускорения, как метод повышения производительности, указанная выше.

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

В качестве модели ЛРД для тестирования выбрана модель Белла-ЛаПадулы, опи сание которой на представленном языке приведено в работе. В тестовую систему были предварительно добавлены 99 пользователей. Каждому из этих пользовате лей был задан атрибут level с произвольным значением. Кроме этого, в тестовую систему был добавлен один пользователь, который был владельцем процессов, за пускавшихся во время тестирования. Ему были установлен самый низкий уровень секретности в модели Белла-ЛаПадулы.

В качестве тестовых примеров были выбраны:

• компиляция ядра linux-2.6.28;

• копирование каталога с большим количеством вложенных подкаталогов и файлов (100 подкаталогов, в каждом из них еще 10 подкаталогов, в каждом из которых 100 файлов);

• копирование большого файла (100 Мб) блоками различных размеров.

Тестовый пример Время выполне- Время выполне ния с отключен- ния с включенным ным модулем модулем разгра разграничения ничения доступа, доступа, с с Компиляция ядра 215 Копирование каталога с 11.5 12. большим числом вложен ных файлов Копирование большого 0.83 0. файла блоками по 4 кб Копирование большого 0.68 0. файла блоками по 1024 кб Как следует из представленных результатов, время выполнения задач с включен ным в состав ядра ОС модулем разграниченяи доступа незначительно отличается от аналогичного времени в отсутствии такого модуля. В некоторых случаях эти за медления находятся в пределах погрешности измерения. Исходя из приведенных выше экспериментальных данных можно сделать вывод, что предложенные в дис сертации методы оптимизации механизмов ЛРД, основанных на разработанном ав тором языке, позволяют достаточно эффективно использовать такие механизмы в современных программных системах.

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

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

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

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

• Реализованы программные механизмы логического разграничения доступа, построенные на основе разработанного языка и предназначенные для их внед рения в ядро ОС Linux и в программы, написанные на языках C и Python.

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

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

оценки эффективности методов повышения производительности об работки запросов на предмет разрешения доступа;

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

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

Публикации по теме диссертации 1. О. О. Андреев. Интеграция моделей логического разграничения досту па, описанных на специализированном языке. // Информационные тех нологии. — М.: Новые технологии. — 2009. — № 12. — С. 29–33.

2. О. О. Андреев. О методах оптимизации механизмов разграничения доступа, основанных на логико-языковых средствах. // Проблемы информатики. — Но восибирск: НГТУ. — 2009. — № 2.

3. В. А. Васенин, К. А. Шапченко, О. О. Андреев. Математические модели и ме ханизмы логического разграничения доступа в операционной системе Linux:

текущее состояние и перспективы развития. // Математика и безопасность информационных технологий. Материалы конференции в МГУ 25–28 октября 2006 г.. — М.: МЦНМО, 2007. С. 159–171. (О. О. Андрееву принадлежат результа ты по исследованию способов описания моделей логического разграничения доступа в защищенных операционных системах).

4. О. О. Андреев. Язык описания моделей разграничения доступа и его реали зация в ядре операционной системы Linux. // Математика и безопасность ин формационных технологий. Материалы конференции в МГУ 2–3 ноября г. — М.: МЦНМО, 2006, С. 305–-322.

5. Набор специализированных дистрибутивов ОС Linux с повышенными требо ваниями к защищенности. / В. А. Васенин, К. А. Шапченко, А. Н. Водомеров, А. В. Инюхин, О. О. Андреев, В. Б. Савкин. // Свидетельство о государственной регистрации программы для ЭВМ № 2006613706. — 2006. (О. О. Андрееву при надлежат результаты по разработке механизмов логического разграничения доступа на основе логико-языковых способов описания моделей).

6. К. А. Шапченко, О. О. Андреев, В. Б. Савкин, А. А. Иткес. Специализированные дистрибутивы операционной системы Linux с повышенным уровнем защи щенности. // Критически важные объекты и кибертерроризм. Часть 2. Аспек ты программной реализации средств противодействия. / О. О. Андреев и др.

Под ред. В. А. Васенина. — М.: МЦНМО, 2008. — 607 с. — С. 168–216. (О. О. Ан дрееву принадлежат результаты по разработке механизма разграничения до ступа, включенного в ядро ОС Linux).

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