Formal verification of security policy implementations in enterprise networks

Abstract

In enterprise networks, the management of security policies and their configurations becoming increasingly difficult due to complex security constraints of the organizations. In such networks, the overall organizational security policy (global policy) is defined as a collection of rules for providing service accesses between various network zones. Often, the specification of the global policy is incomplete; where all possible service access paths may not be covered explicitly by the “permit” and “deny” rules. This policy is implemented in a distributed manner through appropriate sets of access control rules (ACL rules) in the network interfaces. However, the implementation must be complete i.e., all service access paths across the network must be implemented as “permit” and “deny” ACL rules. In that case, the unspecified access paths in a given policy must be implemented as either “permit” or “deny” rules; hence there may exist multiple ACL implementations corresponding to that policy. Formally verifying that the ACL rules distributed across the network interfaces guarantees proper enforcement of the global security policy is an important requirement and a major technical challenge. The complexity of the problem is compounded by the fact that some combination of network services may lead to inconsistent hidden access paths in the network. The ACL implementations ignoring these hidden access paths may result in violation of one or more policy rules implicitly. This paper presents a formal verification framework for analyzing security policy implementations in enterprise networks. It stems from boolean modeling of the network topology, network services and security policy where the unspecified access paths are modeled as “don’t-care” rules. The framework formally models the hidden access rules and incorporates them in the distributed ACL implementations for extracting a security implementation model, and finally formulates a QSAT (satisfiability of quantified boolean formulae) based decision problem to verify whether the ACL implementation conforms to the global policy both in presence and absence of the hidden access paths.