Computer Science Department
School of Computer Science, Carnegie Mellon University
Scenario Graphs and Attach Graphs
Oleg Mikhail Sheyner
We present our results in two parts. In Part I we introduce concepts that let us define faulty behavior sets as "failure scenario graphs." We then describe algorithms for generating scenario graphs. The algorithms use model checking techniques to produce sound and complete faulty behavior sets.
In Part II we apply our formal concepts to the security domain. Building on the foundation established in Part I, we define and attack graphs, an application of scenario graphs to represent ways in which intruders attack computer networks. Attack graphs depict ways in which an adversary exploits system vulnerabilities to achieve a desired state. System administrators use attack graphs to determine how vulnerable their systems are and to determine what security measures to deploy to defend their systems. This application of formal analysis contributes to techniques and tools for strengthening network security.