2.3. Формальные модели управления доступом

Разработанная в 1971 г. модель Харрисона-Руззо-Ульмана [16] формализует упоминавшееся ранее понятие матрицы доступа – таблицы, описывающей права доступа субъектов к объектам (рис. 2.3.1.1).

Строки матрицы доступа соответствуют субъектам, существующим в системе, а столбцы – объектам. На пересечении строки и столбца указаны права доступа соответствующего субъекта к данному объекту: например, на рис. 2.3.1.1 субъект subj 3 обладает правами чтения и записи по отношению к объекту obj 3.

Введём следующие обозначения:

S – множество возможных субъектов,
O – множество возможных объектов (напомним, что S ⊂ O);
R= – конечное множество прав доступа
O×S × R - пространство состояний системы;
M – матрица прав доступа, описывающая текущие права доступа субъектов к объектам;
Q=(S, O, M) – текущее состояние системы;
M[s,o] - ячейка матрицы, содержащая набор прав доступа субъекта s ⊂ S к объекту о ⊂ О

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

Здесь α - имя команды; xt - параметры команды, представляющие собой идентификаторы субъектов и объектов, орi,— элементарные операции.

Элементарные операции op1. opn будут выполнены в том случае, если выполняются все без исключения условия из блока if … then.

При описании элементарных операций мы будем полагать, что в результате выполнения операции система переходит из состояния Q=(S, О, М) в состояние Q’=(S’,0’,M’).

<Модель предусматривает наличие шести элементарных операций:

enter r into M[s,o]

Приведём несколько примеров команд:

Создание файлаПользователь p создаёт файл f и получает на него права владения, чтения и записи. command create_file (p, f)create object f,enter own into M[p, f],enter r into M[p, f],enter w into M[p, f], end
Создание процесса.Процесс p создаёт процесс q и получает на него право чтения, записи и владения, передавая процессу q права записи и чтения по отношению к самому себе. command exec_process(p, q)create subject q,enter own into M[p, q],enter r into M[p, q],enter w into M[p, q],enter r into M[q, p], enter w into M[q, p],end
Передача права чтения по отношению к файлуПраво чтения на файл f передаётся владельцем p субъекту q. command grant_read(p, q, f)if own in M[p, f]then enter r into M[q, f],end

Формальное описание системы в модели Харрисона-Руззо-Ульмана выглядит следующим образом. Система ∑ = (Q,R,C) состоит из следующих элементов:

Конечный набор прав доступа R=.
Конечный набор исходных субъектов S0=.
Конечный набор исходных объектов О0=.
Исходная матрица доступа М0.
Конечный набор команд С = .

Поведение системы во времени рассматривается как последовательность состояний , каждое последующее состояние является результатом применения некоторой команды к предыдущему: Qn+i=Cn(Qn).

Для заданной системы начальное состояние Q0= называется безопасным относительно права r, если не существует применимой к Q0 последовательности команд, в результате выполнения которой право r будет занесено в ячейку матрицы М, в которой оно отсутствовало в состоянии Qo.

Другими словами это означает, что субъект никогда не получит право доступа г к объекту, если он не имел его изначально.

Если же право г оказалось в ячейке матрицы М, в которой оно изначально отсутствовало, то говорят, что произошла утечка права r.

Рассмотрим пример [17]. Пусть система допускает использование двух прав доступа: R=, где г - чтение, а w - запись, и пусть система описывается следующими командами:

Создание субъектаcommand create (s, о)create subject о,enter r into M[s, о],enter w into M[s, o],endКоманда разрешает создание нового субъекта с одновременным получением по отношению к нему прав доступа на чтение и на запись.
Получение прав доступаcommand takex(s, о, р)if r in M[s, о] andх in М[о, р]

Как видим, в результате выполнения шагов 1-5 субъект s обходным путём получает право доступа а по отношению к субъекту о - т.е. происходит утечка права а - а это значит, что исходное состояние не является безопасным.

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

истема ∑ = (Q,R,C) называется монооперационной, если каждая команда at е С выполняет один примитивный оператор.

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

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

Заметим, что команды delete и destroy можно не рассматривать, поскольку нас интересует наличие права а, а не его отсутствие. Аналогично, нет необходимости рассматривать более одного оператора create: система является монооперационной, и одна команда не может одновременно создать объект или субъект и модифицировать его права доступа, поскольку путём замены параметров можно ограничиться работой с последовательностями команд, которые оперируют над существующими субъектами и объектами. Единственная команда create будет необходима на случай, если в начальном состоянии в системе не было ни одного субъекта.

Итак, пусть с1, с2, . сn — последовательность команд, в результате выполнения которой происходит утечка права а. Упростим эту последовательность команд следующим образом:

Удалим все команды delete и destroy.
Добавим в начало последовательности С1, C2 . Cn, —, с„ команду Sinit вида create subject.
Проходя последовательность команд справа налево, последовательно удалим все команды вида create subject и заменим все ссылки на создаваемые с помощью этих команд субъекты ссылкой на Sinit.
Аналогично удалим все команды вида create object, заменяя ссылки на создаваемые с помощью этих команд объекты ссылками на Sinit.
Удалим все команды вида enter, вносящие право а в ячейку, которая уже содержит это право.

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

Команды вида create object, destroy subject, destroy object и delete в последовательности отсутствуют. Команда create subject присутствует в единственном числе. Максимальное число команд вида enter равно |R|(|S0+1)(|О0|+1). Тем самым, общее число возможных команд равно R(S0 +1)(O0 +1) + 1 – а значит, количество последовательностей команд ограничено

К сожалению, расширить полученный результат на произвольные системы невозможно.

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

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

Классическая модель Харриона-Руззо-Ульмана до сих пор широко используется при проведении формальной верификации корректности построения систем разграничения доступа в высоко защищённых автоматизированных системах. Развитие моделей дискреционного управления доступом [18, 19] заключается преимущественно в построении всевозможных модификаций модели Харрисона-Руззо-Ульмана, а также в поиске минимально возможных ограничений, которые можно наложить на описание системы, чтобы вопрос её безопасности был вычислительно разрешимым.

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

Данная модель была предложена в 1975 году [20] для формализации механизмов мандатного управления доступом. Мандатный принцип разграничения доступа, в свою очередь, ставил своей целью перенести на автоматизированные системы практику секретного документооборота, принятую в правительственных и военных структурах, когда все документы и допущенные к ним лица ассоциируются с иерархическими уровнями секретности.

В модели Белла-ЛаПадулы по грифам секретности распределяются субъекты и объекты, действующие в системе, и при этом выполняются следующие правила:

Простое правило безопасности (Simple Security, SS).Субъект с уровнем секретности x5 может читать информацию из объекта с уровнем секретности xo тогда и только тогда, когда x5 преобладает над xo.
*-свойство (*-property).Субъект с уровнем секретности x5 может писать информацию в объект с уровнем секретности xo в том и только в том случае, когда xo преобладает над x5.

Для первого правила существует мнемоническое обозначение No Read Up, а для второго – No Write Down.

Диаграмма информационных потоков, соответствующая реализации модели Белла-ЛаПадулы в системе с двумя уровнями секретности, приведена на рис. 2.3.2.1.

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

S - множество субъектов;
О - множество объектов, S с О;
R= - множество прав доступа, г - доступ на чтение, w - доступ на запись;
L= - множество уровней секретности, U- Unclassified, SU -Sensitive but unclassified, S - Secret, TS - Top secret;
Λ = (L, ≤,•, Θ ) - решётка уровней секретности;
V - множество состояний системы, представляемое в виде набора упорядоченных пар (F, М), где:
- F :S U O -> L - функция уровней секретности, ставящая в соответствие каждому объекту и субъекту в системе определённый уровень секретности;
- М- матрица текущих прав доступа.
становимся более подробно на решётке уровней секретности. Напомним, что решёткой Λ называется алгебраическая система вида (L, ≤,•, Θ ) , где:
- ≤ - оператор, определяющий частичное нестрогое отношение порядка для уровней секретности;
- • - оператор наименьшей верхней границы;
- Θ - оператор набольшей нижней границы.
Отношение ≤ обладает следующими свойствами:
1. Рефлексивность: V a ∈ L : а ≤ а . С точки зрения уровней безопасности это означает, что разрешена передача информации между субъектами и объектами одного уровня безопасности.
2. Антисимметричность: V а1,а2 ∈ L: ((a1 ≤ а2) & (а2 ≤ a1))—>а2 =а1. Антисимметричность в нашем случае означает, что если информация может передаваться как от субъектов и объектов уровня А к субъектам и объектам уровня В, так и от субъектов и объектов уровня В к субъектам и объектам уровня А, то эти уровни эквивалентны.
3. Транзитивность: V а 1 ,а 2,a3 ∈ L : ( (a 1 ≤ а 2 ) & (а 2 ≤ a3 ) ) -> а1 ≤ а3. Транзитивность означает, что если информации может передаваться от субъектов и объектов уровня А к субъектам и объектам уровня В, и от субъектов и объектов уровня В к субъектам и объектам уровня С, то она может передаваться от субъектов и объектов уровня A к субъектам и объектам уровня С.
Операторы наименьшей верхней границы • и наибольшей нижней границы Θ определяются следующим образом:

Нетрудно показать, что для каждой пары V а 1 ,а 2 ∈ L существует единственный элемент наименьшей верхней границы и единственный элемент наибольшей нижней границы.

Заметим, что в качестве уровней безопасности совершенно не обязательно выбирать целые числа, в ряде случаев удобнее использовать более сложные структуры. За счёт этого, например, в пределах каждого уровня секретности можно реализовать категории секретности (см. рис. 2.3.2.2). В этом случае наличие допуска к той или иной категории информации может служить дополнительным механизмом безопасности, ограничивающим доступ к защищаемым субъектам или объектам.
- Система I = ( ν 0,R,T)в модели Белла-ЛаПадулы состоит из следующих элементов:
- ν 0 - начальное состояние системы; R - множество прав доступа;
- Т : V х R —> V - функция перехода, которая в ходе выполнения запросов переводит систему из одного состояния в другое.
Изменение состояний системы во времени происходит следующим образом: система, находящаяся в состоянии v е V, получает запрос на доступ гей и переходит в состояние ν* = Т( ν , r).

Состояние νn называется достижимым в системе ∑ = ( ν 0 ,R,T), если существует последовательность :T(ri, νi )= νi+1 V i=0,n-1 Начальное состояние ν 0 является достижимым по определению.

Состояние системы (F, М) называется безопасным по чтению (или simple-безопасным), если для каждого субъекта, осуществляющего в этом состоянии доступ по чтению к объекту, уровень безопасности субъекта доминирует над уровнем безопасности объекта:

V s ∈ S, V o ∈ О, r ∈ M[s, о] -> F(o) ≤ F(s).

Состояние (F, М) называется безопасным по записи (или * - безопасным) в случае, если для каждого субъекта, осуществляющего в этом состоянии доступ по записи к объекту, уровень безопасности объекта доминирует над уровнем безопасности субъекта:

V s ∈ S, V o ∈ О : w ∈ M[s,o] -> F(s) ≤ F(o).

Состояние (F, М) называется безопасным, если оно безопасно по чтению и по записи.

Наконец, система ∑ = ( ν 0 ,R,T) называется безопасной, если её начальное состояние ν 0 безопасно, и все состояния, достижимые из v0 путём применения конечной последовательности запросов из R, безопасны.

Теорема (Основная теорема безопасности Белла-ЛаПадулы). Система ∑ = ( ν 0 ,R,T) безопасна тогда и только тогда, когда выполнены следующие условия:
1. Начальное состояние ν 0 безопасно.
2. Для любого состояния ν , достижимого из ν 0 путём применения конечной последовательности запросов из R, таких, что T( ν ,r) = ν* , ν =(F, М) и ν* =(F*, М*) , для V s ∈ S, V o ∈ О выполнены условия:
  1. Если r ∈ M*[s,o] и r ∉ M[s,o], то F*(o) ≤ F*(s).
  2. Если r ∈ M*[s,o] и F*(s)<F*(o), то r ∈ M*[s,o]
  3. Если w ∈ M*[s,o] и w ∉ M[s,o], то F*(o) ≤ F*(s).
  4. Если w ∈ M*[s,o] и F*(s)<F*(o), то w ∈ M*[s,o]
  Доказательство: Пусть система ∑ = ( ν 0 ,R,T) безопасна. В этом случае начальное состояние Vo безопасно по определению. Предположим, что существует безопасное состояние ν *, достижимое из состояния ν : T( ν ,r) = ν* , и для данного перехода нарушено одно из условий 1-4. Легко заметить, что в случае, если нарушены условия 1 или 2, то состояние ν * будет небезопасным по чтению, а если нарушены условия 3 или 4 - небезопасным по записи. В обоих случаях мы получаем противоречие с тем, что состояние ν * является безопасным.
  
  Докажем достаточность утверждения. Система ∑ = ( ν 0 ,R,T) может быть небезопасной в двух случаях:
  1. В случае если начальное состояние ν 0 небезопасно. Однако данное утверждение противоречит условию теоремы.
  2. Если существует небезопасное состояние ν *, достижимое из безопасного состояния ν 0 путём применения конечного числа запросов из R. Это означает, что на каком-то промежуточном этапе произошёл переход Т( ν , r) = ν *, где ν - безопасное состояние, а ν * - небезопасное. Однако условия 1-4 делают данный переход невозможным.
  Отметим, что изложенная модель в силу своей простоты имеет целый ряд серьёзных недостатков. Например, никак не ограничивается вид функции перехода T – а это означает, что можно построить функцию, которая при попытке запроса на чтения к объекту более высокого уровня секретности до проверки всех правил будет понижать уровень секретности объекта. Другим принципиальным недостатком модели Белла-ЛаПадулы является потенциальная возможность организации скрытых каналов передачи информации. Тем самым, дальнейшее развитие моделей мандатного управления доступом было связано с поиском условий и ограничений, повышающих её безопасность.
  
  В настоящее время модель Белла-ЛаПадулы и другие модели мандатного управления доступом [18, 19] широко используются при построении и верификации автоматизированных систем, преимущественно предназначенных для работы с информацией, составляющей государственную тайну.
  📎📎📎📎📎📎📎📎📎📎