Host-centric model checking for network vulnerability analysis

Rattikorn Hewett, Phongphun Kijsanayothin

Research output: Contribution to journalConference articlepeer-review

27 Scopus citations


Recent research has successfully applied model checking, a formal verification technique, to automatically generate chains of vulnerability exploits that an attacker can use to reach his goal. Due to the combinatorial explosion of the chain generation problem space, model checkers do not scale well to networks containing a large number of hosts. This paper proposes a methodology that uses a host-centric modeling approach together with a monotonicity assumption to alleviate the scalability problem of model checkers. We describe the proposed approach, its limitations, and show how it can reduce the time complexity of chain generation to a quadratic polynomial of the number of hosts, both theoretically and empirically. We also compare its advantages over similar customized graph-based approaches.

Original languageEnglish
Article number4721560
Pages (from-to)225-234
Number of pages10
JournalProceedings - Annual Computer Security Applications Conference, ACSAC
StatePublished - 2008
Event24th Annual Computer Security Applications Conference, ACSAC 2008 - Anaheim, CA, United States
Duration: Dec 8 2008Dec 12 2008


Dive into the research topics of 'Host-centric model checking for network vulnerability analysis'. Together they form a unique fingerprint.

Cite this