A Verification framework for Analyzing Security Implementations in an Enterprise LAN

In a typical local area network (LAN), the global security policies, often defined in abstract form, are implemented through a set of access control rules (ACL) placed in a distributed fashion to the access switches of its sub-networks. Proper enforcement of the global security policies of the network demands well-defined policy specification as a whole as well as correct implementation of the policies in various interfaces. But, ensuring correctness of the implementation manually is hard due to the complex security policies and presence of hidden access paths in the network. This paper presents a formal verification framework to verify the security implementations in a LAN with respect to a defined security policy. The proposed framework stems from formal models of network security policy specifications, device-specific security implementations, and deploys verification supported by SAT based procedures. The novelty of the work lies in the analysis of the hidden access paths, which plays a significant role in correct security implementations.