Network configuration in a box: towards end-to-end verification of network reachability and security
- 1 October 2009
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Recent studies show that configurations of network access control is one of the most complex and error prone network management tasks. For this reason, network misconfiguration becomes the main source for network unreachablility and vulnerability problems. In this paper, we present a novel approach that models the global end-to-end behavior of access control configurations of the entire network including routers, IPSec, firewalls, and NAT for unicast and multicast packets. Our model represents the network as a state machine where the packet header and location determines the state. The transitions in this model are determined by packet header information, packet location, and policy semantics for the devices being modeled. We encode the semantics of access control policies with Boolean functions using binary decision diagrams (BDDs). We then use computation tree logic (CTL) and symbolic model checking to investigate all future and past states of this packet in the network and verify network reachability and security requirements. Thus, our contributions in this work is the global encoding for network configurations that allows for general reachability and security property-based verification using CTL model checking. We have implemented our approach in a tool called ConfigChecker. While evaluating ConfigChecker, we modeled and verified network configurations with thousands of devices and millions of configuration rules, thus demonstrating the scalability of this approach.Keywords
This publication has 13 references indexed in Scilit:
- Automated pseudo-live testing of firewall configuration enforcementIEEE Journal on Selected Areas in Communications, 2009
- Shadow configuration as a network management primitivePublished by Association for Computing Machinery (ACM) ,2008
- Modeling and Verification of IPSec and VPN Security PoliciesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Conflict classification and analysis of distributed firewall policiesIEEE Journal on Selected Areas in Communications, 2005
- On static reachability analysis of IP networksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Firewall design: consistency, completeness, and compactnessPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- Integrity for virtual private routed networksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Symbolic model checking: 1020 States and beyondInformation and Computation, 1992
- Temporal and Modal LogicPublished by Elsevier BV ,1990
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986