take(α, x, y, z)
|
x ∈ S, (x, y, t)∈ E,
(y, z, β )1∈ E x≠ z, α ⊆ β
|
S'=S, O'=O,
E= E' ∪{(x, z, α)}
|
grant(α,x,y, z)
|
x ∈ S, (x, y, g)∈E,
(y, z, β )∈ E x≠ z, α ⊆ β
|
S'=S, O'=O,
E= E' ∪{(y, z, α)}
|
create(β, x, y)
|
x ∈ S, y∉ O
|
O'=O ∪{y},
S'=S ∪{y}, если y – субъект E= E' ∪{(y, z, β )}
|
remove(α,x,y)
|
x ∈ S, y∈ O,
(x, y, β)∈ E, α ⊆ β
|
S'=S, O'=O,
E= E' \ {(x,y,α)}∪{(x, y, β )}
|
Санкционированное получение прав доступа Вводятся следующие определения1.
Определение 2.1.6. Для исходного состояния системы Γ0 (O0, S0, E0) и прав доступа α ⊆ R предикат "возможен доступ(α, x, y, Γ0)" является истинным тогда и только тогда, когда существуют графы доступов системы Γ1 (O1, S1, E1), Γ2 (O2, S2, E2), …, ΓN (ON, SN, EN), такие, что:
Γ0(O0,S0,E0)├с1 Γ1(O1,S1,E1)├с2…├сN ΓN(ON,SN,EN) и (x, y,α)∈ EN
где c1, c2, …, cN – команды вида 2.1, 2.2, 2.3 и 2.4.
Говоря иначе, доступ субъекта x к объекту y с правом α ⊆ R, отсутствующий в начальном состоянии системы (x, y, α) ∉ E0, возможен тогда и только тогда, когда существует последовательность перехода системы из состояния в состояние (Γ0, Γ1,…, ΓN) под воздействием команд 2.1, 2.2, 2.3 и 2.4.
Определение 2.1.7. Вершины графа доступов являются tg-связными (соединены tg-путем), если в графе между ними существует такой путь, что каждая дуга этого пути выражает право t или g (без учета направления дуг).
Вершины непосредственно tg-связаны, если tg-путь между ними состоит из единственной дуги.
Справедлива следующая теорема.
Теорема 2.1.3. В графе доступов Γ0 (S0,O0, E0), содержащем только вершины-субъекты, предикат "возможен доступ(α, x, y, Γ0)" истинен тогда и только тогда, когда выполняются следующие условия:
Условие 2.1.3.1. Существуют субъекты s1,…,sm такие, что (si, y, γi)∈E0 для i=1, …, m и α =γ1 ∪…∪γm.
Условие 2.1.3.2. Субъект х соединен в графе Γ0 tg-путем с каждым субъектом si для i=1, …, m.
Доказательство. Доказательство теоремы проводится для m=1, так как схема доказательства для этого случая легко обобщается на случай m>1.
При m=1 условия 2.1.3.1 и 2.1.3.2 формулируются следующим образом:
Условие 2.1.3.1. Существует субъект s такой, что справедливо (s, y, α) ∈ E0.
Условие 2.1.3.2. Субъекты x и s соединены tg-путем в графе Γ0.
Необходимость. Пусть истинен предикат "возможен дос-
туп(α, x, y, Γ0)". Тогда по определению 2.6 существует последовательность графов доступов Γ1 (O1, S1, E1), Γ2 (O2, S2, E2),…, ΓN (ON, SN, EN) такая, что: Γ0├с1 Γ1├с2…├сN ΓN и (x, y, α) ∈ EN, при этом N является минимальным, т. е. (x, y, α) ∉ EN -1. Необходимость условий 2.1.3.1 и 2.1.3.2 можно доказать индукцией по N.
При N=0 очевидно (x, y, α) ∈ E0. Следовательно, условия 2.1.3.1,
2.1.3.2 выполнены.
Пусть N>0, и утверждение теоремы истинно для ∀ k < N. Тогда (x, y, α) ∉E 0 и дуга (x, y, α) появляется в графе доступов ΓN в результате применения к графу ΓN -1 некоторой команды сN. Очевидно, это не команда "Создать" или "Удалить". Если сN является командой "Брать" (или "Давать"), то по его определению ∃ s′∈ SN -1: (x, s′, t) ∈ EN -1 (или (s′, x, g) ∈ EN -1), (s′, y, α) ∈ EN -1 и сN = take(α, x, s′, y) (или сN = grant (α, s′, x, y)).
Возможны два случая: s′∈ S0 и s′∉ S0.
s′∈ S0. Тогда истинен предикат "возможен доступ (α, s′, y, Γ0)", при
этом число преобразований графов меньше N. Следовательно, по предположению индукции ∃ s∈ S0: (s, y, α) ∈ E0 и s′ соединен с s tg-путем в графе Γ0. Кроме этого, истинен предикат "возможен доступ (t, x, s′, Γ0)" (или "возможен доступ(g, s′, x, Γ0)"), при этом число преобразований графов меньше N. Следовательно, по предложению индукции
∃ s′′∈S0: (s′′, s′, t)∈E0 и s′′ соединен с x tg-путем в графе Γ0(или (s′′, x, g) ∈ E0 и s′′ соединен с s′ tg-путем в графе Γ0). Таким образом, ∃ s∈ S0: (s, y, α) ∈ E0 и субъекты x, s соединены tg–путем в графе Γ0. Выполнение условий 2.1.3.1 и 2.1.3.2 для случая s′∈ S0 доказано.
s′∉ S0. Число N преобразований графов минимально, поэтому новые
субъекты создаются только в тех случаях, когда без этого невозможна передача прав доступа. Следовательно, преобразования графов отвечают следующим требованиям:
субъект-создатель берет на созданный субъект максимально необходимый набор прав{t, g};
каждый имеющийся в графе Γ0 субъект не создает более одного субъекта;
созданный субъект не создает новых субъектов;
созданный субъект не использует правило "Брать" для получения прав доступа на другие субъекты.
Из перечисленных требований следует, что ∃ М< N –1,
∃ s′′∈ S0: cМ = create({g, t}, s′′, s′), cN = take(α, x, s′, y) и истинен предикат "возможен доступ (α, s′′, y, Γ0)". Отсюда следует, что истинен предикат "возможен доступ (t, x, s', ΓM)" , а так как s'' – единственный субъект в графе ΓM, имеющий права на субъект s', то по предположению индукции s'' соединен с x tg-путем в графе Γ0. Из истинности предиката "возможен доступ (α, s′′, y, Γ0)" и по предположению индукции следует, что s и s'' соединены tg–путем в графеΓ0. Следовательно, ∃ s∈S0: (s, y, α) ∈ E0 и x, s соединены tg–путем в графе Γ0. Выполнение условий 2.1.3.1 и 2.1.3.2 для случая s′∉ S0 доказано. Индуктивный шаг доказан.
Достаточность. Пусть выполнены условия 2.1.3.1 и 2.1.3.2 Доказательство проведем индукцией по длине tg–пути, соединяющего субъекты x и s.
Пусть N = 0. Следовательно, x = s, (x, y, α) ∈E0 и предикат "возможен доступ(α, x, y, Γ0)" истинен.
Пусть N = 1, т. е. ∃ s∈S0: (s, y, α) ∈E0 и субъекты x, s непосредственно tg-связаны. Тогда возможны четыре случая такого соединения x и s, для каждого из которых нетрудно указать последовательность преобразований графа, требуемую для передачи прав доступа (см. рис. 2.7).
Рис. 2.7. Возможные случаи непосредственной tg-связности x и s, а также последовательность преобразований графаΓ0 до получения доступа (x, y, α) ∈ EN
Таким образом, при N =1 предикат "возможен доступ(α, x, y, Γ0)" истинен.
Пусть N >1. Рассмотрим вершину z, находящуюся на tg–пути между x и s, и являющуюся смежной с s в графе Γ0. Тогда по доказанному для случая N =1 существует последовательность преобразований графов доступов Γ0├с1 Γ1├с2…├сK ΓK : (z, y, α) ∈ EK и длина tg–пути между z и x равна N –1, что позволяет применить предположение индукции.
Теорема доказана. ■
Несмотря на кажущуюся сложность теоремы 2.1.3, она иллюстрирует вообще говоря довольно простой и интуитивно понятный порядок вещей – если кто-либо желает получить какие-либо права на кого-то, то при отсутствии ограничений на взаимоотношения субъектов, он может скооперироваться с третьим(ми) субъектом, кто такие права уже имеет, и позаимствовать их у него.
Авторы модели провели анализ санкционированного получения прав доступа также и в графе произвольного вида, состоящего как из субъектов, так и объектов. Для рассмотрения предиката "возможен доступ" в произвольном графе вводится ряд дополнительных понятий.
Определение 2.1.8. Островом в произвольном графе доступов Γ называется его максимальный tg-связный подграф, состоящий только из вершин субъектов.
Заметим, что остров, по сути, характеризует некую группу субъектов, кооперация которых в правах доступа не ограничена и процессы получения доступа внутри группы описываются теоремой 2.3.
Определение 2.1.9. Мостом в графе доступов Γ называется tg–путь, концами которого являются вершиныr * s-*субъектыr * gr s * r; * gприs s * этом словарная* запись tg-пути должна иметь вид t ,t ,t t ,t t , где символ означает многократное (в том числе нулевое) повторение.
Определение 2.1.10. Начальным пролетом моста в графе доступов Γ называется tg-путь, началом которого является вершинаr * gr -субъект; при этом словарная запись tg-пути должна иметь вид t .
Определение 2.1.11. Конечным пролетом моста в графе доступов Γ называется tg-путь, началом которого является вершинаr * -субъект; при этом словарная запись tg-пути должна иметь вид t .
Справедлива следующая теорема.
Теорема 2.1.4. В произвольном графе доступов Γ0 (S0, O0, E0) предикат "возможен доступ(α, x, y, Γ0)" истинен тогда и только тогда, когда выполняются условия 2.1.4.1, 2.1.4.2 и 2.1.4.3:
Условие 2.1.4.1. Существуют объекты s1,…,sm такие, что (si, y, γi)∈E0 для i=1, …, m и α=γ1 ∪…∪γm.
Условие 2.1.4.2. Существуют вершины-субъекты x1',…, xm' и s1',…, sm' такие, что:
Do'stlaringiz bilan baham: |