Information Technology Reference
In-Depth Information
Safety Problem Resolver.
A special tool was developed for interpreting and process-
ing the SPSL-specifications, named a safety problem resolver (SPR). SPR is a logical
machine based on the Prolog kernel. It gets SPSL specification and uses the logical
rules for resolution. We can apply SPR to a safety problem solving as it is described
below (Fig. 3).
If we need to evaluate given system state
∑
∈
S
Σ
by the model criteria
C
, we can
∑
put the system state
and criteria
C
to SPR and determine its safety according to
∑
the security criteria
C
: ∀
c
∈
C
:
c
(
s
=
D
(
)) =
true
. We make the assumption that the
system security mechanism implements the access control
R
properly.
If we need to generate the states
∑
∑
∈
S
Σ
reachable from
and evaluate their
∑
∈
S
Σ
, access rules
R
and security criteria
safety, we need to put the current state
∑
∑
C
, and produce all the states
reachable from
and test their security in two
stages:
1. ∀
∑
∑
+
∑
+
∑
∑
∑
+
∈
S
Σ
:
,
=
T
(
q
,
) ∃
s
i
=
D
(
),
s
i
+1
=
D
(
)
and ∀
r
∈
R
:
r
(
s
i
,
s
i
+1
) =
true
2. ∀
∑
∑
∑
∑
∈
S
Σ
:
is reachable from
,
s
i
=
D
(
):∀
c
∈
C
:
c
(
s
i
) =
true
!
"
init
s
#$
Fig. 3.
Safety Problem Resolver
Safety Evaluation Workshop
Evaluation Framework Structure
On the basis of SPR we build a number of tools, which bring the process of safety
evaluation to the routine procedure: