Information Technology Reference
In-Depth Information
An important feature of an access control is therefore an ability to verify the safety
of system configurations.
Safety Problem in Theory
Security concerns arise in many different contexts; so many security models have
been developed. A typical categorization of access control models is between manda-
tory and discretionary models.
MAC is safe by definition, and no safety problem resolving is needed for the
MAC-based system, because safety for MAC was proved theoretically in general case
(e.g., [8]). Verification of the safety of any kind of MAC policy is obvious, but, unfor-
tunately, in general case safety cannot be verified for an arbitrary access control
model and system.
By the way Harrison, Ruzzo, and Ullman showed that the safety problem for DAC
models is undecidable in general case [9], and the determining whether the system
implementing access control model is safe in the given state must be resolved for
every system and every state. Unfortunately the great majority of the systems (operat-
ing systems, DBMS, etc.) uses exactly the DAC-based security models as the basis of
an access control mechanism.
Therefore, the safety problem resolving is the actual problem for the security
evaluation, especially, for the DAC-based computer systems.
Mathematical Basis
It is fundamental to ensure that the enforcing of the access control model will guaran-
tee a system security. The system in the given system state is safe according to the
access control model, if:
1. A security state corresponding to the given (initial) system state conforms to the
security criteria.
2. A system access control mechanism realizes the access control rules.
3. All security states reachable from the initial one keep the security criteria fair.
By solving the safety problem, process of producing the reachable states and
evaluating them by criteria is called a safety problem resolving. To make the resolv-
ing process precise it was considered the following formalization.
∑
= {
S
Σ
,
T
,
A General System.
A general system
Σ
is a state machine:
Σ
,
Q
},
where:
•
S
Σ
is the set of the system states,
•
Q
denotes the set of the queries executed by the system,
T
is the state transition function,
T
:
Q
×
S
Σ
→
S
Σ
moves the system from one state to
another: a request
q
is issued in the state
•
∑
and moves the system to the next state
∑
+
=
T
(
q
,
s
Σ
),
∑
•
denotes the initial system state.
