Information Technology Reference
In-Depth Information
S
0
δ
0
(
S
0
)
,δ
0
∈∆
S
1
∆
∗
⎬
S
n
δ
1
(
S
n
)
,δ
1
∈∆−∆
∆ − ∆
⎭
•
•
•
...
...
∆
∗
⎬
⎭
•
∆ − ∆
•
•
•
...
...
∆
∗
.
Fig. 6.
Graphical representation of
TVA()
algorithm
the model checking techniques appear promising for automatic attack graph
generation, these techniques break down when handling non-trivial, real world
examples. The model checker's complexity grows exponentially in the size of the
state space and hence it does not scale to the enormous state space of non-trivial,
real world computer networks. In this paper, we present scalable algorithms for
common real-world situations.
To compensate for the state explosion problem inherent in the model checking
approach, Ammann
et al.
[1] propose “a more compact and scalable graph-based
approach to network vulnerability analysis”. Their approach relies heavily on
the assumption of monotonicity: (i) an attacker can gain capabilities, but never
lose them; and (ii) gaining additional capabilities does not reduce the exploits
available to an attacker. The problem with this approach is that it does not allow
for non-monotonic rules in a system. In this paper, we present ecient algorithms
for vulnerability analysis of a system containing monotonic and non-monotonic
rules, thus reflecting a model for real world examples.
6Con lu on
In this paper, we have presented a formal model and a set of scalable algorithms
for performing topological vulnerability analysis. Our approach is more scal-
able than model-checker-based solutions and more expressive than monotonicity-
based solutions. We represent individual attacks as the transition rules of a
