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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

End.

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

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

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

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

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

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

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

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

Добавление субъекту s_i права r_g для объекта o_{j .}

Enter r_g into a_ij

Удаление у субъекта s_i права r_g для объекта o_j.

Delete r_g from a_ij

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

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

Create subject s_i of type t_sx

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

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

Destroy subject s_x of type t_sx

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

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

Create object o_y of type t_oy

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

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

Destroy object o_y of type t_oy

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

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

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

C_z (s_j: t_sj, o_i: t_oi, s_x:t_sx, o_y: t_oy)

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

Create Subject s_j of type t_sj;

Create Object o_i of type t_oi,

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

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

t_sj и t_oi считаются дочерними типами;

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

Другими словами, для того, чтобы создать объект o_i типа t_oi или субъект s_j типа t_sj в системе должен быть объект o_y типа t_oy или субъект s_x типа t_sx.

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

Command_1 (s₁: t₁, s₂: t₁)

Create Subject s₂ of type t₁

End.

В этой команде тип t₁ считается родительским относительно субъекта s₁ и дочерним относительно субъекта s₂.

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

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

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

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

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