Scenario and Attack Graphshttp://www.cs.cmu.edu/~scenariograph/

<a href="http://people.cis.ksu.edu/~xou/mulval/">http://people.cis.ksu.edu/~xou/mulval/</a>

<a href="http://web.mit.edu/tlo/www/industry/comp_security_tech.html#NetSPA">http://web.mit.edu/tlo/www/industry/comp_security_tech.html#NetSPA</a>

<a href="http://www.redsealnetworks.com/">http://www.redsealnetworks.com/</a>

<a href="http://cyvisiontechnologies.com/cauldron">http://cyvisiontechnologies.com/cauldron</a>

<a href="#introduction">Introduction</a>

<a href="#people">People</a>

<a href="#publications">Publications</a>

<a href="#software">Software</a>

Model checking is a technique for determining whether a formal model of a system satisfies a given property. If the property is false in the model, model checkers typically produce a single counterexample. The developer uses this counterexample to revise

the model (or the property), which often means fixing a bug in the design of the system. The developer then iterates through the process, rechecking the revised model against the (possibly revised) property.

Sometimes, however, we would like all counterexamples, not just one. Rather than produce one example of how the model does not satisfy a given property, why not produce all of them at once? We call the set of all counterexamples ascenario graph.

For a traditional use of model checking, e.g., to find bugs, each path in the graph represents a counterexample, i.e., a failure scenario. In our application to security, each path represents an attack, a way in which an intruder can attack a system. Attack

graphs are a special case of scenario graphs.

Attack graphs depict ways in which an adversary can exploit vulnerabilities to break into a system. System administrators analyze attack graphs to understand where their system's weaknesses lie and to help decide which security measures will be

effective to deploy. In practice, attack graphs are produced manually by Red Teams. Construction by hand, however, is tedious, error-prone, and impractical for attack graphs larger than a hundred nodes.

Our attack graph toolkit generates scenario graphs from a network attack model and a security property. An example security property is that an intruder should never gain root access to a specific host. Since each scenario graph is property-specific, in

practice, we might need to generate many scenario graphs to represent the entire attack graph that a Red Team might construct manually. Our main advantage is that we automate the process of producing scenario graphs.

<a href="http://www.cs.cmu.edu/~wing">Jeannette M. Wing</a>

Dilsun Kaynar

David Swasey

<a href="http://www.cs.cmu.edu/People/oleg/">Oleg Sheyner</a>

Oren Dobzinski

Yanjing Li

Meera Sridhar

Arvind Kannan

Roman V. Lototski

Alexey Roschyna

Kaufmann Publishers, Elsevier, Inc., draft submitted December 2006.

in Intrusion Detection, Hamburg, Germany, September 2006. Springer LNCS 4219.

Security, Timisoara, Romania, March 2005. Summary paper.

on Formal Methods for Components and Objects, Leiden, The Netherlands, November 2003. Springer LNCS 3188.

May 2002.

October 2000.

Maliciowns FauIts, New York, NY, June 2000.

The current release of the attack graph toolkit is version 20070201.

<dl></dl>

<dt></dt>

<a href="attackgraph-20070201.tar.gz">attackgraph-20070201.tar.gz</a>

<dd>The code has been reorganized and made to work with recent C/C++ compilers. </dd>

<dd>The original release of the attack graph toolkit, developed by Oleg Sheyner, Roman Lototski, Alexey Roschyna, and others.</dd>