Scenario Graphs and Attack Graphs

For the past twenty years, model checking has been used successfully in many engineering projects. Model checkers assist the engineer in identifying automatically individual design flaws in a system. A typical model checker takes as input a model of the system and a correctness specification. It checks the model against the specification for erroneous behavior. If erroneous behavior exists, the model checker produces an example that helps the user understand and address the problem. Once the problem is fixed, the user can repeat the process until the model satisfies the specification perfectly. In some situations the process of repeatedly checking for and fixing individual flaws does not work well. Sometimes it is not feasible to eliminate every undesirable behavior. For instance, network security cannot in practice be made perfect due to a combination of factors software complexity, desire to keep up with the latest features, expense of fixing known system vulnerabilities, etc. Despite these difficulties, network system administrators would invest the time and resources necessary to find and prevent the most destructive intrusion scenarios. However, the find problem- fix problem-repeat engineering paradigm inherent in traditional uses of model checkers does not make it easy to prioritize the problems and focus the limited available resources on the most pressing tasks.