Two Formal Analyses of Attack Graphs
An attack graph is a succinct representation of all paths through a system
that end in a state where an intruder has successfully achieved his
goal. Today Red Teams determine the vulnerability of networked systems by
drawing gigantic attack graphs by hand. Constructing attack graphs by hand
is tedious, error-prone, and impractical for large systems. By viewing an
attack as a violation of a safety property, we can use off-the-shelf model
checking technology to produce attack graphs automatically: a successful
path from the intruder's viewpoint is a counterexample produced by the
model checker. In this paper we present an algorithm for generating attack
graphs using model checking as a subroutine.
Security analysts use attack graphs for detection, defense and
forensics. In this paper we present a minimization analysis technique
that allows analysts to decide which minimal set of security measures
would guarantee the safety of the system. We provide a formal
characterization of this problem: we prove that it is polynomially
equivalent to the minimum hitting set problem and we present a greedy
algorithm with provable bounds. We also present a reliability
analysis technique that allows analysts to perform a simple
cost-benefit trade-off depending on the likelihoods of attacks. By
interpreting attack graphs as Markov Decision Processes we can use the
value iteration algorithm to compute the probabilities of intruder
success for each attack the graph.
Download:[PS,PDF]
Somesh Jha
Last modified: Mon Mar 31 09:56:10 CST 2003