Information Technology Reference
In-Depth Information
Input:
σ
- a reverse attack path,
σ ∈ S
∗
.
∆
-setofrules.
∆
- noninterfering ruleset of
∆
.
as
- attributes to be reacquired.
Output:
A successful attack path, if one exists; else
.
Algorithm:
TVA(σ, ∆, ∆
,as)
σ
=
findMaximal
(
σ, ∆
)
s
=
head
(
σ
)
if
s ∈ S
G
then
return
σ
else
if
as
=
∅
then
σ
=
recoverAttributes
(
σ
,as
)
σ
=
TVA
(
σ
,∆,∆
, ∅
)
if
σ
=
then
return
σ
for each
δ
(
A, B, C, D
)
∈ ∆ − ∆
do
if
A ⊆ s
and
B ∩ s
=
∅
then
s
=(
s ∪ C
)
− D
if
s
=
s
then
σ
=
TVA
(
s
.σ
,∆,∆
,s− s
)
if
σ
=
then
return
σ
return
Fig. 5.
TVA()
algorithm
tacks using a similar approach. Our model is also based on this representation
of attacks.
Phillips and Swiler [9] present a model which uses “attack templates” and
a “physical network topology” description to generate attack graphs. Swiler et
al. [17] describe a tool that implements this model but they do not present
or analyze the algorithms used to generate attack graphs. We present several
scalable algorithms for our formal model of vulnerability analysis.
Ritchey and Ammann [14] propose the use of model checking to automat-
ically generate attack paths, while Sheyner et al. [15,16] propose the use of
model checking to automatically generate attack graphs. Jha et al. [7,6] present
two analyses of attack graphs. Ramakrishnan and Sekar [10,11] use a model
checker to discover individual vulnerabilities on single hosts. Ritchey
et al.
[13]
present improvements to Ritchey and Ammann's model [14] by presenting a
more expressive model for the connectivity of networks. This body of work pro-
vides a model checker with a model of a specific system and of known attacks,
and a safety property; the model checker determines whether the given safety
property is satisfied in the model. When the safety property is not satisfied, the
model checker generates a counterexample in the form of an attack path. While
