Integrated security analysis framework for an enterprise network - a formal approach

In a typical enterprise network, correct implementation of security policies is becoming increasingly difficult owing to complex security constraints and dynamic changes in network topology. Usually, the network security policy is defined as the collection of service access rules between various network zones. The specification of the security policy is often incomplete since all possible service access paths may not be explicitly covered. This policy is implemented in the network interfaces in a distributed fashion through sets of access control (ACL) rules. Formally verifying whether the distributed ACL implementation conforms to the security policy is a major requirement. The complexity of the problem is compounded as some combination of network services may lead to inconsistent hidden access paths. Further, failure of network link(s) may result in the formation of alternative routing paths and thus the existing security implementation may defy the policy. In this study, an integrated formal verification and fault analysis framework has been proposed which derives a correct ACL implementation with respect to given policy specification and also ensures that the implementation is fault tolerant to certain number of link failures. The verification incorporates boolean modelling of the security policies and ACL implementations and then formulates a satisfiability checking problem.