Типизированная матрица доступа

Дискреционная модель Type Access Matrix(TAM) – типизированная матрица доступа – является развитием модели Xappисона- Руззо-Ульмана. Модель ТАМ дополняет модель Xappисона- Руззо-Ульмана концепцией типов, что позволяет смягчить те условия, для которых возможно доказательство безопасности системы.

В модели ТАМ рассматриваются:

· конечное множество объектов компьютерной системы O = [oj], 1,…n;

· конечное множество субъектов компьютерной системы S = [si],
1, …m.

Считается, что все субъекты системы одновременно являются и ее объектами.

· конечное множество прав доступа R = [rg], 1, …k.

Матрица прав доступа, содержащая права доступа субъектов к объектам A = [aij], i = 1, …m, j = 1,…n+m, причем элемент матрицы aij рассматривается как подмножество множества R.

Каждый элемент матрицы aij содержит права доступа субъекта si к объекту oj.

Множество типов, которые могут быть поставлены в соответствие объектам и субъектам системы T = [ tb ], b = 1,…w.

Конечное множество команд С=[ cz (аргументы с указанием типов )], z=1,...I, включающих условия выполнения команд и их интерпретацию в терминах элементарных операций. Элементарные операции ТАМ отличаются от элементарных операций дискреционной модели Xappисона- Руззо-Ульмана использованием типизированных аргументов.

Структура команды

Command cz (аргументы и их типы)

Условия выполнения команды

Элементарные операции

End .

Смысл элементарных операций совпадает со смыслом аналогичных операций, используемых в модели Xappисона- Руззо-Ульмана с точностью до использования типов.

Поведение системы моделируется с помощью понятия состояние. Состояние системы определяется:

· конечным множеством субъектов (S);

· конечным множеством объектов (O), считается, что все субъекты системы одновременно являются и ее объектами (SO);

· матрицей прав доступа (А)

и описывается тройкой Q ( S, O, A ).

Выполнение элементарных операций переводит систему, находящуюся в состоянии Q в другое состояние Q'.

В модели ТАМ определены следующие элементарные операции:

Добавление субъекту si права rg для объекта oj.

Enter rg into aij

Удаление у субъекта si права rg для объекта oj.

Delete rg from aij

Типы объектов и субъектов при выполнении этих операций остаются без изменения.

Создание нового субъекта si с типом tsx

Create subject si of type tsx

Субъекту sx и объекту ox ставится в соответствие тип tsx из множества T, типы остальных субъектов и объектов остаются без изменения.

Удаление существующего субъекта si с типом tsx

Destroy subject sx of type tsx

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

Создание в системе нового объекта oj типом toy

Create object oy of type toy

Объекту oy ставится в соответствие тип toy из множества T, типы остальных объектов и субъектов при выполнении этой операций остаются без изменения.

Удаление существующего объекта oy с типом toy

Destroy object oy of typetoy

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

Строгий контроль соответствия типов в модели ТАМ позволяет смягчить требование одноусловности, заменив его ограничением на типы аргументов команд, при выполнении которых происходит создание новых объектов и субъектов.

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

Cz (sj : tsj, oi : toi, sx :tsx, oy : toy)

cчитается дочерним, если в этой команде используются элементарные операции вида:

Create Subject sj of type tsj ;

Create Object oi of type toi ,

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

В рассматриваемой команде:

tsj и toi считаются дочерними типами;

tsx и toy считаются родительскими типами.

Другими словами, для того, чтобы создать объект oi типа toi или субъект sj типа tsj в системе должен быть объект oy типа toy или субъект sx типа tsx.

Следует отметить, что в одной команде тип может быть одновременно и родительски и дочерним. Например,

Command_1 (s1 : t1, s2 : t1)

Create Subject s2 of type t1

End.

В этой команде тип t1 считается родительским относительно субъекта s1 и дочерним относительно субъекта s2.

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

Граф создания представляет собой направленный граф с множеством вершин Т, в котором ребро от ti к tj существует тогда и только тогда, когда в системе имеется команда создания субъекта или объекта, в которой ti является родительским типом, a tj– дочерним.

Этот граф для каждого типа позволяет определить:

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

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

Наши рекомендации