12. Схематичная модель защиты (spm). Анализ безопасности с использованием spm. Теорема о максимально достижимом состоянии. Объявлено уг.

Рассказываем вначале об SPM.

Вообщем h - состояние системы.

Пусть X,Y сущности и если для X≠Y выполняется одно из условий:

•    link^h_j(X,Y)  = true

•   существует такая последовательность x= x₀,x₁,... x_n, такая что link^h_j(x₀,x₁)  = link^h_j(x₁,x₂)  = ... = link^h_j(x_n-1,x_n)  = true, где x₀=X, x_n=Y,

  

    то говорят что path^h(X,Y)=true, где path предикат.

    Множество ярлыков которые могут быть переданы от X к Y указанным путем есть cap(pathⁿ,X,Y) - множество ярлыков

    значит это множество ярлыков cap вычисляется следующим образом:

    1. если link^h_j(X,Y), тогда cap(pathⁿ,X,Y) = f_i(t(X),t(Y))

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

cap(path^h(X, Y)) = { t(Y)/r:c | t(Y)/rc & f₀(t(X),t(X₀)) t(Y)/rc  & f_k(t(X_k–1),t(X_k)) (for k = 1, …, n),  & t(Y)/r:c f_n(t(X_n),t(Y)) }.

Пусть есть различные пути path от X к Y тогда функция flow это объединение cap для всех этих путей:

Есть множество состояний системы (см. определение контрольных прав, они типа когда команда меняет состояние системы). Вообщем есть такое состояние *, для которого flow максимальна, оно называется максимальным состоянием. Функция flow*(X,Y) отвечает этому состоянию, и если ярлык находится в этом множестве flow*, это означает что тогда существует такая последовательность операций что этот ярлык может быть скопирован из X в Y.

Возникает два вопроса - уникально ли максимальное состояние? И любая ли система имеет максимальное состояние?

Вводим отношение порядка < (см. в конспекте как оно на самом деле пишется, просто тут такого знака нету).

Определение 1.

Отношение g < h является истинным, только если для любых X,Y (из начального состояния!!!!):

flow^g(X, Y) содержится в flow^h(X, Y)

    Если g < h и h < g то состояния считаются эквивалентными.

    Определение 2.

    Для данной системы, состояние m максимально тогда и только тогда когда h < m для любого состояния h.

    Теорема о достижимом состоянии. 

 Существует максимально достижимое состояние для любой системы описанной SPM.

Доказательство.

Это просто редчайшее УГ, можете конечно почитать в оригинале на английском или в конспекте у рудиной но не советую терять время

13. Выразительная мощность моделей дискреционного контроля доступа. Сравнение spm и модели хру. Расширенная схематическая модель защиты (espm). Сравнение spm, espm и хру.

.

Выразительность в общем это как мы можем выразить одну модель через другую.

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

Модели HRU и SPM показывают различные ответы на вопрос о безопасности. Как же соотносятся этим модели.

SPM - монотонная модель (нет delete и destroy)

ХРУ - множественное создание и удаление сущностей.

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

NT(x) – множество типов вершин для схемы X

ET(x) – множество типов дуг

Схема A согласуется с B <=> граф, описывающий A получается из графа, описывающего B, удалением вершин, не содержащихся в A и всех дуг в B

т: E->T – множество типов вершин

т: ExR->TxR - множество типов дуг

A выражает B <=>

для любого состояния b доступного в B существует согласующееся с ним состояние a в схеме A, которое согласуется с ним, а так же наоборот.

Если существует схема моделей МА, которую не может выразить ни одна модель в схеме MB, то модель MB менее выразительна.

Если любая может выразить любую то эквивалентны.

Т: монотонные модели в в которых операции создания ограничиваются 1м субъектом, менее выразительны чем монотонные модели с совместным созданием (например, ESPM более выразительна чем SPM)

//ESPM это тот же SPM ток с совместным созданием (те к созданному объекту могут //передаваться права от нескольких субъектов)

Т: ESPM эквивалентна ХРУ