Mutating Network Models to Generate Network Security Test Cases

  • Ronald W. Ritchey
Part of the The Springer International Series on Advances in Database Systems book series (ADBS, volume 24)


Security testing is normally limited to the scanning of individual hosts with the goal of locating vulnerabilities that can be exploited to gain some improper level of access on the target network Scanning is a successful approach for discovering security problems, but it suffers from two major problems. First, it ignores security issues that can arise due to interactions of systems on a network. Second, it does not provide any concept of test coverage other than the obvious criteria of attempting all known exploitation techniques on every system on the network.

In this paper, I present a new method for generating security test cases for a network This method extends my previous work in model checking network security by defining mutant operators to apply to my previously defined network security model. The resulting mutant models are fed into a model checker to produce counterexamples. These counterexamples represent attack scenarios (test cases) that can be run against the network. I also define a new coverage criterion for network security that requires a much smaller set of exploits to be run against the network to verify the network’s security.


Model Checker Mutant Operator Security Requirement Network Security Mutant Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Apache]
    Apache Web Server information and software on the web at Scholar
  2. [Beizer]
    B. Beizer, “Software Testing Techniques, 2nd edition,” Thomson Computer Press, 1990.Google Scholar
  3. [Birch]
    J. Birch, E. Clark, K. McMillan, D. Dill, and L.J. Hwang, Symbolic Model Checking: 1020 States and Beyond, Proceedings of the ACM/SIGDA International Workshop in Formal Methods in VLSI Design, January, 1991.Google Scholar
  4. [Chan]
    W. Chan, R. Anderson, P. Beame, S. Bums, E Modugno, and D. Notkin, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, Vol. 24, No. 7, July 1998.Google Scholar
  5. [Clark]
    E. Clark, O. Grumberg, and D. Long, Verification Tools For Finite-State Concurrent Systems, A Decade of Concurrency–Reflections and Perspectives, Springer Verlag, 1994.Google Scholar
  6. [COPS]
    Computer Oracle and Password System (COPS) information and software on the web at /pub/tools/cops.
  7. [Holzmann]
    G. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, Vol 23, No 5, May 1997.Google Scholar
  8. [ISS]
    Internet Security Systems, System Scanner information on the web at
  9. [Mayer]
    A. Mayer, A. Wool and E. Ziskind, Fang: A Firewall Analysis Engine, Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, 2000.Google Scholar
  10. [NAI]
    Network Associates, CyberCop Scanner information on the web at /aspset/products/tns/ccscanner intro.asp.
  11. [Offutt]
    J. Offutt, Practical Mutation Testing, Twelfth International Conference on Testing Computer Software, pages 99–109, Washington, DC, June 1995.Google Scholar
  12. [RedHat]
    RedHat Linux information and software on the web at
  13. [Ritchey]
    R. Ritchey and P. Ammann, Using Model Checking To Analyze Network Security, 2000 IEEE Symposium on Security and Privacy, May 2000.Google Scholar
  14. [SMV]
    SMV information and software on the web at–modelcheck.
  15. [Zerkle]
    D. Zerkle and K. Levitt, NetKuang–A Multi-Host Configuration Vulnerability Checker, In Proceedings of the Sixth USENIX Unix Security Symposium, San Jose, CA, 1996.Google Scholar

Copyright information

© Springer Science+Business Media New York 2001

Authors and Affiliations

  • Ronald W. Ritchey
    • 1
  1. 1.Booz•Allen & HamiltonFalls ChurchUSA

Personalised recommendations