Hierachical Formal Modeling and Verification of Router Policies with an Applied Case Study to Cisco Router Configurations

摘要

Today's economy and society's well-being are dependent on secure information technology systems and networks. Securing enterprise-size technology systems with thousands of interconnected devices in hundreds of networks has proven a grand challenge. Within this environment, network administrators and cybersecurity personnel need a method for verifying, with a high degree of accuracy and efficiency, that security policies are being correctly implemented throughout the enterprise's network. In this thesis, we describe a formal model, and associated developed tools, for policy verification of network routing policies. We also describe the practical application of this model and tools to a an enterprise-class case study for a Cisco-based network. The specific contributions are: formal modeling of router policies, high-level querying of enterprise router policies, formal router policy verification, and toward formal routing policy concatenation. This work demonstrates that it is possible to formally model and verify real router policies in an enterprise network.