CMU-CS-04-122Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-04-122
Oleg Mikhail Sheyner April 2004 Ph.D. Thesis
CMU-CS-04-122.ps
Keywords: Unavailable
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. 141 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |