Host-centric model checking for network vulnerability analysis

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.