Information Technology Reference
In-Depth Information
Corollary 1.
If
T
has no reachable goal state, then
T
has no reachable goal
state.
The corollary provides us with an ecient way of testing that a system is
secure (i.e., has no exploitable vulnerabilities): A system is secure if its monotonic
approximation has no reachable goal state. Note that this test is sucient but
not necessary—a system may be secure even if its monotonic approximation is
vulnerable.
Figure 4 presents an algorithm
transform()
(with complexity
O
(
)) for com-
puting the monotonic approximation of a state transition system. The algorithms
of Section 3 can then be used to check whether the monotonic approximation is
secure.
|∆|
Input:
T
- state transition rule-system.
Output:
T
- monotonic state transition rule-system.
Algorithm:
transform(T )
let
T
=(
A,∆,s
0
,S
G
)in
∆
=
∅
for
each
δ
(
A, B, C, D
)
∈ ∆
do
∆
=
∆
∪{δ
(
A, ∅,C,∅
)
}
return
(
A,∆
,s
0
,S
G
)
Fig. 4.
Monotonic approximation algorithm
Example 2
Let
δ
1
be the transition rule for the
BIND NXT remote root exploit
described in Section 2.5. Then,
∆
=
{δ
1
}
,where
δ
1
is (as defined earlier):
a
1
,a
2
,a
3
,a
4
,a
5
,a
6
,a
7
,a
8
,a
9
;
b
1
δ
1
c
1
;
d
1
The rule
δ
1
has two negative attributes, namely
b
1
=
service(DNS, 53,
l
3
,H)
and
d
1
=
service(vul-DNS, 53,
l
2
,V)
.Then
∆
, the monotonic approximation
of
∆
,is
∆
=
{δ
1
}
where
δ
1
is defined as:
δ
1
c
1
;
If an attacker is unable to carry out the exploit
δ
1
in a less restrictive environment
(i.e., in an environment where a DNS service may or may not be present on the
attacker's host), then clearly the attacker will not be able to execute the exploit
δ
1
in a more restrictive environment in which a DNS service is absent. This
simple example shows that if the monotonic approximation has no reachable
goal state, then the original system has no reachable goal state.
a
1
,a
2
,a
3
,a
4
,a
5
,a
6
,a
7
,a
8
,a
9
;
4.2 Nonmonotonicity
Let us assume that
T
=(
A,∆,s
0
,S
G
) is a state transition rule-system and
∆
=
computeNRS
(
∆
) the noninterfering rule subset of
T
. Figure 5 presents
