Формулировка теоремы о разрешимости проблемы безопасности в общем случае.

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

8. Доказательство теоремы о разрешимости проблемы безопасности для модели Харрисона-Руззо-Ульмана в общем случае.

Монооперационные команды - команды в которых присутствует одна операция, к примеру:

     enter r into a[p,q]

Запросы общего вида содержат несколько монооперационных команд, например:

    command create (p, f)

    create object f;

    enter own into a[p,f]

    enter r into a[p,f]

    enter w into a[p,f]

    end

Есть модель Харрисона-Руззо-Ульмана, встает вопрос о том является ли система с запросами общего вида безопасной? (под безопасностью для права r подразумевается как я понял то, что не существует последовательности команд, которые запишут это право в ячейку, хотя его не было в исходной матрице доступа)

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

Теорема о разрешимости.

    Проблема определения безопасности для данного права r в системе с запросами общего вида является неразрешимой.

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

Есть Машина Тьюринга, далее именуемая как МТ.

Она бесконечна только вправо. Изначальное состояние q0, головка указывает на самую левую ячейку.

Каждая ячейка пронумерована и соответствует субъекту {s₁,s₂,...s_n), здесь мы объединяем множество субъектов и объектов в одно понятие субъект!

Правами для МТ будут состояния и символы МТ.

Введены три операции:

Эти операции грубо говоря моделируют модель ХРУ, остановка данной МТ означает утечку прав, но поскольку проблема остановки произвольной МТ не разрешима, значит и проблема безопасности для права r неразрешима.

9.      Модель Take-Grant. Основные определения. Разделение права доступа в терминах модели Take-Grant, необходимые и достаточные условия разделения права, сложность задачи определения разделения права субъектами в модели Take-Grant.

Господа Харрисон, Рузо и Ульман, доказали, что, в общем случае, основной вопрос безопасности является неразрешимым. Но он разрешим в частных случаях. Для того, чтобы определить условия, в которых данный вопрос разрешим, господа Джонс, Липтон и Шнайдер разработали модель Take-Grant. В этой модели основной вопрос безопасности не только разрешим, но и разрешим за линейное время(относительно кол-ва объектов и прав).

В данной модели система представляется в виде направленного графа. Вершинами являются субъекты(черные кружки) и объекты(белые кружки).

Направленные дуги обозначают права. Множество прав R, помимо стандартных прав, содержит еще 2 права — Take(t) и Grant(g).

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

Правила переписывания графа:

            Take

 

 

Субъект X имеет право take на Z. Z имеет какое-то право b на y. Тогда право take определяет новый граф (который справа).

Простыми словами, если у X есть право t на что-то, то он может забирать у него права.

"X берет право b по отношению к Y от Z"

            Grant

 

 

 

 

Если X имеет право g на что-то, то он  этому "что-то" может дать свои права.

"X дает Z право b по отношению к Y"

            Create

"X создает вершину Y с правом b по отношению к Y"

 

            Remove

 

"X удаляет право a для Y"

 

Разделение прав в терминах модели take-grant

Если существует последовательность графов G₀,G₁,...,G_n : G₀ |-* G_n (G_n выводится из G₀ за конечное число шагов), и в G_n есть стрелка с правом a от X к Y, то выполнен предикат canshare(a,X,Y,G₀).

Данный предикат показывает, может ли вершина X получить право a кY.

tg-путь — непустая последовательность направленных дуг графа G такая, что для любых i от 1 до n-1 v_i соединена с v_i-1 стрелкой take и/или grant.

Лемма

2 субъекта, связанные tg-путем длины 1 разделяют права.

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

Я заебусь рисовать его.

Остров — максимальный tg-связанный подграф, состоящий из субъектоа

Из леммы следует теорема:

Теорема: Все субъекты в острове разделяют права

 

Мост — tg-путь между V₀ и V₁ субъектами. Имеет вид:

{t*->, <-*t, t*->g-><-*t, t*-><-g<-*t } (лучше это посмотреть в тетрадке)

 

Добавим еще парочку штук:

Говорят, что x initially spans y, если x — субъект и между x и y существует tg-путь вида {t*->g*->}

Говорят, что x terminally spans y, если x — субъект и между x и y существует tg-путь вида {t*->}

И теперь главная теорема:

Т (видимо необходимое и достаточное условие разделения прав)

Предикат canshare(a,x,y,G₀) истинен тогда и только тогда, когда существует tg-путь {a->} от x к y (примитивный случай) либо выполнено:

1. Существует s из G₀: s a-> y. (стрелка a из s в y)

2. Существует субъект x': x'=x или x' initially spans x.

3. Существует s': s'=s или s' terminally spans s

4. Существуют острова J₁,...J_n: x' из J₁, s' из J_n  и, для любых y от 1 до n-1, существует мост между J₁ и J_n