Title :
Using model checking to analyze network vulnerabilities
Author :
Ritchey, Ronald W. ; Ammann, Paul
Author_Institution :
Booz, Allen & Hamilton Inc., Falls Church, VA, USA
Abstract :
Even well administered networks are vulnerable to attacks due to the security ramifications of offering a variety of combined services. That is, services that are secure when offered in isolation nonetheless provide an attacker with a vulnerability to exploit when offered simultaneously. Many current tools address vulnerabilities in the context of a single host. We address vulnerabilities due to the configuration of various hosts in a network. In a different line of research, formal methods are often useful for generating test cases, and model checkers are particularly adept at this task due to their ability to generate counterexamples. We address the network vulnerabilities problem with test cases, which amount to attack scenarios, generated by a model checker. We encode the vulnerabilities in a state machine description suitable for a model checker and then assert that an attacker cannot acquire a given privilege on a given host. The model checker either offers assurance that the assertion is true on the actual network or provides a counterexample detailing each step of a successful attack
Keywords :
computer networks; security of data; telecommunication security; attack scenarios; computer network security; formal methods; model checking; network vulnerabilities; state machine description; test cases; Computer bugs; Computer networks; Information filtering; Information filters; National security; Network servers; Software engineering; Web server;
Conference_Titel :
Security and Privacy, 2000. S&P 2000. Proceedings. 2000 IEEE Symposium on
Conference_Location :
Berkeley, CA
Print_ISBN :
0-7695-0665-8
DOI :
10.1109/SECPRI.2000.848453