Study Of Scenario Graph And Attack Graph Based On Model Checking

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. System administrators use attack graphs to determine how vulnerable their systems are and to determine what security measures to deploy to defend their systems. Today security analysts determine the vulnerability of networked systems by drawing graphs by hand. But constructing attack graphs by hand is tedious, error-prone, and impractical for large systems. So it is nessceary to study how to generate and analyze attack graph automatically. By viewing an attack as a violation of a safety property, we can use model checking to produce attack graphs automatically: a successful path from the intruder's viewpoint is a counterexample produced by the model checker. But traditional model checkers give users a single counterexample, chosen from the set of faulty behaviors. So it's also necessary to study how to give the user access to the entire set.In this paper, we develop formal techniques that give users flexibility in examining design errors discovered by automated analysis. We build our results using the model checking approach to verification. We introduce a new formalism that defines faulty behavior sets as failure scenario graphs. We discuss two algorithms for generating scenario graphs: Symbolic Model Checking Algorithm and Explicit-State Model Checking Algorithms. The algorithms use model checking techniques to produce faulty behavior sets that are sound and complete. We apply the formalism and algorithms to the security domain. We define and analyze attack graphs, an application of scenario graphs to represent ways in which intruders attack computer networks. We focus our work on ways of generating, presenting, and analyzing attack graphs, .We organize this paper in the following parts: we first define and analyze failure scenario graphs. We then describe algorithms for generating scenario graphs from finite models and measure the algorithms'performance. Then we give a definition for attack models and attack graphs, and consider some post-generation analyzes that can be done on attack graphs. Then we introduce a usable attack graph toolkit, including its framework, modules and graphical user interfaces. By applying the toolkit in a small network example, we illustrate how we generate an attack graph and analyze it. Finally, we state our conlusions.