Information Technology Reference
In-Depth Information
∑
∑
={
S
Σ
,
T
,
A system
Σ
,
Q
} is a finite machine: a state
is reachable in the sys-
∑
∑
∑
∑
tem
Σ
if and only if there is the sequence <(
q
0
,
), ..., (
q
n
,
)> such that
=
,
∑
∑
∑
∑
−
∑
s
=
, and
=
T
(
q
i
,
) if 0<
i
<
n
. Note that for any system
is trivially
1
reachable.
A General Security Model.
A general security model
M
is an ensemble of sets,
M
={
S
,
R
,
C
}, where:
•
S
denotes the set of the security states defined by the security model,
•
R
is the set of the access control rules in the form of logical predicates
r
(
s
,
s'
) de-
fined on
S
×
S
and checking that the transition from
s
to
s'
meets to the security
model,
•
C
is the set of the state security criteria in the form of logical predicates
c
(
s
) de-
fined on
S
and checking security of the state
s
. A state
s
∈
S
is secure if and only if
for every security criterion
c
from
C
the predicate
c
(
s
) is true:
∀
c
∈
C
:
c
(
s
)=true.
A System Safety Property.
A system safety property Λ can be formulized as Λ={
M
,
Σ,
D
}, where:
•
M
is the access control model,
M
={
S
,
R
,
C
},
• Σ
∑
= {
S
Σ
,
T
,
denotes the system,
Σ
,
Q
},
D
is the mapping function,
D
:
S
Σ
→
S
, which sets the relation between the system
states and the security states.
By the definitions being specified, a system safety statement may be formulated.
•
A System Safety Statement
The system Σ implementing the model
M
is safe if and only if:
1. ∀
c
∈
C
:
c
(
D
(
∑
))=
true
,
∑
∑
+
∑
+
∑
∑
∑
+
∈
S
Σ
:
2. ∀
,
=
T
(
q
,
) ∃
s
i
=
D
(
),
s
i
+1
=
D
(
) and ∀
r
∈
R
:
r
(
s
i
,
s
i
+1
)=
true
,
∑
∑
∑
∑
∈
S
Σ
:
3. ∀
))=
true
.
This statement declares an analogous of the General Security Theorem [4, 5], but
in reference to the safety problem in real computer systems.
is reachable from
, ∀
c
∈
C
:
c
(
D
(
Security Tasks Statement
The introduced theory establishes a basis of the problems which face every participant
of IT-security: the theoreticians, the system developers and the evaluators. According
to the proposed definitions we can state three problems.
Model Proof.
For the given model
M
we have to prove that any reachable state from
S
satisfies the security criteria
C
. In this case we prove that every system realized on
such a mode will be safe in general.
System Design.
For the given system Σ, the security criteria
C
, and the security states
S
we have to create the access control rules
R
so that system Σ with
M
={
C
,
S
,
R
} will
be safe.