В современных системах автоматизированного проектирования ши

if
r
1
in
M
[
x
s
1
, 
x
o
1
] 
and
(условия выполнения команды) 
r
2
in
M
[
x
s
2
, 
x
o
2
] 
and
. 
. 
r
m
in
M
[
x
sm
, 
x
om
] 
and
then 
op
1
, 
op
2
… 
op
n
(операции, составляющие команду). 
Перед выполнением команды происходит проверка типов фактиче-
ских параметров, и если они не совпадают с указанными в определении, 
команда не выполняется. Фактически, введение контроля типов для пара-
метров команд приводит к неявному введению дополнительных условий, 
так как команды могут быть выполнены только при совпадении типов па-
раметров. В модели используются следующие шесть элементарных опера-
ций, отличающихся от аналогичных операций модели Харрисона-Руззо-
Ульмана только использованием типизованных параметров. 

---

180
Монотонные операции 
Немонотонные операции 
enter
r
into
M
[
s
, 
o
]
 
delete
r
from
M
[
s
, 
o
]
 
create subject
s
of type
t 
destroy subject
s 
create object
o
of type
t 
destroy object
o 
Смысл элементарных операций совпадает со смыслом аналогичных 
операций из классической модели Харрисона-Руззо-Ульмана с точностью 
до использования типов: 
enter
r
into
M
[
s
, 
o
] (где 
s

S
,
o

O
) 
O
` = 
O
S
` = 
S
t
`(
o
) = 
t
(
o
) для всех 
o

O
M
`[
x
s
, 
x
o
] = 
M
[
x
s
, 
x
o
], если (
x
s
, 
x
o
) 

(
s
, 
o
) 
M
`[
s
, 
o
] = 
M
[
s
, 
o
] 

{
r
} 
delete
r 
from
 M
[
s
, 
o
] (где 
s

S
, 
o

O
)
 
O
` = 
O
S
` = 
S
t
`(
o
) = 
t
(
o
) для всех 
o

O
M
`[
x
s
, 
x
o
] = 
M
[
x
s
, 
x
o
], если (
x
s
, 
x
o
) 

(
s
, 
o
) 
M
`[
s
, 
o
] = 
M
[
s
, 
o
] \ {
r
} 
create subject
s
of type
t
s
(где 
s

S
)
 
O
` = 
O

{
s
} 
S
` = 
S

{
s
} 
t
`(
o
) = 
t
(
o
) для всех 
o

O
t
`(
s
) = 
t
s
M
`[
x
s
, 
x
o
] = 
M
[
x
s
, 
x
o
] для всех (
x
s
, 
x
o
) 

S
× 
O

---

181
M
`[
s
, 
x
o
] = 

для всех 
x
o

O
` 
M
`[
s
, 
x
s
] = 

для всех 
x
s

S
` 
destroy subject
s
(где 
s

S
)
 
O
` = 
O
\{
s
} 
S
` = 
S
\{
s
} 
t
`(
o
) = 
t
(
o
) для всех 
O

O
` 
t
`(
s
) = не определено 
M
[
x
s
, 
x
o
]` = 
M
[
x
s
, 
x
o
] для всех (
x
s
, 
x
o
) 

S
` × 
O
` 
create object
o
of type
t
o
(где 
o

O
)
 
O
` = 
O

{
o
} 
S
` = 
S
t
`(
O
) = 
t
(
O
) для всех 
O

O
M
`[
x
s
, 
x
o
] = 
M
[
x
s
, 
x
o
] для всех (
x
s
, 
x
o
) 

S
× 
O
M
`[
x
s
, 
o
] = 

для всех 
x
s

S
` 
destroy object
o
(где 
o

O
\
S
)
 
O
` = 
O
\{
o
} 
S
` = 
S
t
`(
x
o
) = 
t
(
x
o
) для всех 
x
o

O
` 
t
`(
o
) = не определено 
M
`[
x
s
, 
x
o
] = 
M
[
x
s
, 
x
o
] для всех (
x
s
, 
x
o
) 

S
` × 
O
`. 
Таким образом, ТАМ является обобщением модели Харрисона-
Руззо-Ульмана,. которую можно рассматривать как частный случай ТАМ с 
одним-единственным типом, к которому относятся все объекты и субъек-
ты. Появление в каждой команде дополнительных неявных условий, огра-
ничивающих область применения команды только сущностями соответст-
вующих типов, позволяет несколько смягчить жесткие условия классиче-
ской модели, при которых критерий безопасности является разрешимым. 

---

182
В работе [142] Харрисон, Руззо и Ульман показали, что критерий 
безопасности дискреционной модели может быть доказан для систем, в 
которых все команды 
α
i
(
x
1
,..., 
x
k
) являются одноусловными и монотонны-
ми. Строгий контроль соответствия типов позволяет смягчить требование 
одноусловности, заменив его ограничением на типы параметров команд, 
при выполнении которых происходит создание новых сущностей. 
Для того чтобы сформулировать это ограничение, определим отно-
шения между типами. Пусть 
α
(
x
1
:
t
1
, 
x
2
:
c
, …, 
x
k
:
t
k
) – некоторая команда 
ТАМ. Будем говорить, что 
t
i
является 
дочерним типом
в 
α
, если в теле 
α
имеет место одна из следующих элементарных операций: 
create subject
x
i
of 
type
t
i
или 
create object
x
i
of type
t
i
. В противном случае будем говорить, что 
t
i
является 
родительским типом
в 
α
. 
Отметим, что в одной команде тип может быть одновременно и ро-
дительским, и дочерним, например: 
command
foo
(
s
1
:
u
, 
s
2
:
u
, 
s
3
:
w
, 
o
:
b
) 
create subject
s
2 
of type
u
; 
create subject
s
3 
of type
v
;
 
end. 
Здесь 
u
является родительским типом относительно 
s
1
и дочерним 
типом относительно 
s
2.
Кроме того, 
w
и 
b
являются родительскими типами, 
а 
v
– дочерним типом.
Тогда можно описать взаимосвязи между различными типами с по-
мощью графа, определяющего отношение "наследственности" между ти-
пами, устанавливаемые через операции порождения сущностей (объектов 
и субъектов). Такой граф называется 
графом cоздания
и представляет со-
бой направленный граф с множеством вершин 
Т
, в котором ребро от 
u
к 
v
существует тогда и только тогда, когда в системе имеется создающая ко-
манда, в которой 
u
является родительским типом, а 
v
– дочерним типом.
Этот граф для каждого типа позволяет определить: 

---

183
1.
сущности каких типов должны существовать в системе, чтобы в ней 
мог появиться объект или субъект заданного типа; 
2.
сущности каких типов могут быть порождены при участии сущностей 
заданного типа. 
Модель монотонной типизированной матрицы доступа (МТАМ) 
идентична ТАМ за исключением того, что в ней отсутствуют немонотон-
ные элементарные операции 
delete
, 
destroy subject
и 
destroy object
. 
Реализация МТАМ, состоящая из множеств объектов, субъектов, ти-
пов, матрицы прав доступа и множества команд, называется 
ациклической
тогда и только тогда, когда её граф создания не содержит циклов, в про-
тивном случае говорят, что реализация 
циклическая
. Например, граф соз-
дания для приведённой выше команды 
foo
содержит следующие ребра:
{(
u
, 
u
), (
u
, 
v
), (
w
, 
u
), (
w
, 
v
), (
b
, 
u
), (
b
, 
v
)}. Реализация МТАМ, содержащая 
эту команду, будет циклической, поскольку тип 
u
является для неё одно-
временно и родительским и дочерним, что приводит к появлению на графе 
цикла (
u
, 
u
). 
Доказано, что критерий безопасности, предложенный Харрисоном, 
Руззо и Ульманом, разрешим для ациклических реализаций МТАМ, и что 
требование одноусловности команд можно заменить требованием ацик-
личности графа создания [141]. Смысл этой замены состоит в том, что по-
следовательность состояний системы должна следовать некоторому мар-
шруту на графе создания, поскольку невозможно появление сущностей 
дочерних типов, если в системе отсутствуют сущности родительских ти-
пов, которые должны участвовать в их создании. Отсутствие циклов на 
графе создания позволяет избежать зацикливания при доказательстве кри-
терия безопасности, так как количество путей на графе без циклов является 
ограниченным. 
Это означает, что поведение системы становится предсказуемым, 
поскольку в любом состоянии можно определить сущности каких типов 

---

184
могут появиться в системе, а каких – нет. Но, к сожалению, доказано, что в 
общем случае сложность проверки критерия безопасности для МТАМ яв-
ляется NP-трудной задачей, то есть с ростом размерности задачи (количе-
ства объектов и субъектов) время на её решение растёт в степенной зави-
симости от её размерности. Этот недостаток может быть преодолен с по-
мощью 
тернарной
ТАМ, в которой команды могут иметь не более трёх 
параметров. Тернарная МТАМ является монотонной версией тернарной 
ТАМ. Для тернарной МТАМ доказательство безопасности радикально уп-
рощается, поскольку при проверке условной части команды всегда исполь-
зуется только небольшой фрагмент матрицы доступа. Тернарная МТАМ по 
своим выразительным способностям эквивалентна МТАМ, несмотря на 
это, доказано, что безопасность её ациклической реализации разрешима за 
время, зависящее от размера начальной матрицы. 
Следовательно, введение строгого контроля типов в дискреционную 
модель Харрисона-Руззо-Ульмана позволило доказать критерий безопас-
ности систем для более приемлемых ограничений, что существенно рас-
ширило область её применения.