Host-Centric Model Checking for Network Vulnerability Analysis

PDF
1.1MB

Rattikorn Hewett
Texas Tech University
United States

Phongphun Kijsanayothin
Texas Tech University
United States

Abstract:
Network vulnerability analysis generates chains of vulnerabilities exploitable by an attacker. These chains of possible exploits are then used to determine the work required to secure the network, typically by repairing the vulnerabilities and configuration errors. Recent research has successfully applied model checking, a formal verification technique, to automatically generate chains of exploits reachable to that an attacker can use to reach his goal. However, it is well known that, 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 foundation for host-centric model checking that uses a host-centric modeling approach together with a monotonicity assumption to alleviate the scalability problem of model checkers. By representing the states in the problem space in host-centric rather than the traditional network-centric, each state is represented by the attribute values relevant to a target host instead of the attribute values of all hosts in the target network. The assumption assumes the validated pre-condition of an exploit is never invalidated. 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. We also illustrate its advantages over similar previous customized graph-based approaches by giving examples, complexity analysis and experimental results.