Policy Based Security Analysis in Enterprise Networks: A Formal Approach

In a typical enterprise network, there are several sub-networks or network zones corresponding to different departments or sections of the organization. These zones are interconnected through set of Layer-3 network devices (or routers). The service accesses within the zones and also with the external network (e.g., Internet) are usually governed by a enterprise-wide security policy. This policy is implemented through appropriate set of access control lists (ACL rules) distributed across various network interfaces of the enterprise network. Such networks faces two major security challenges, (i) conflict free representation of the security policy, and (ii) correct implementation of the policy through distributed ACL rules. This work presents a formal verification framework to analyze the security implementations in an enterprise network with respect to the organizational security policy. It generates conflict-free policy model from the enterprise-wide security policy and then formally verifies the distributed ACL implementations with respect to the conflict-free policy model. The complexity in the verification process arises from extensive use of temporal service access rules and presence of hidden service access paths in the networks. The proposed framework incorporates formal modeling of conflict-free policy specification and distributed ACL implementation in the network and finally deploys Boolean satisfiability (SAT) based verification procedure to check the conformation between the policy and implementation models.