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. The two inputs to a model checker are a finite system model and a formal correctness property specifying acceptable behaviors. The correctness property induces a bipartition on the set of behaviors of the model: correct behaviors, which satisfy the property, and faulty behaviors, which violate the property. Traditional model checkers give users a single counterexample, chosen from the set of faulty behaviors. Giving the user access to the entire set, however, lets him have more control over the design refinement process. The focus of our work is on ways of generating, presenting, and analyzing faulty behavior sets.

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
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu