Computer Network Verification and Management using Constraint Solvers

Abstract

Today’s computer networks have become extremely large and complicated. The

increased scale is observed in datacenters, which can have hundredes of

thousands of network devices. The increased complexity is due to multiple kinds

of networking devices (routers, Network Address Translators, firewalls, etc.)

that need to work together to execute diverse network functions such as

routing, access control, and network address translation. In addition,

networking devices need to support multiple protocols to make the network safer

and faster. Consequently, it is non-trivial to manage such a large and complex

system. Many research works have shown that network configuration is prone to

human errors. Thus, it is critical to automate the network configuration and

management tasks to achieve more reliable networks.

In my thesis, I mainly focus on three aspects of network management automation.

(i) It is important that network administrators can utilize automatic

verification and error detection mechanisms to reveal the underlying bugs and

warn administrators whenever the network cannot satisfy certain critical

properties, such as reachability and absence of forwarding loop. (ii) Firewalls

have to be managed automatically in order to guarantee a correct packet access

control policy. A simple error in firewall configuration can potentially leak

confidential corporate information. (iii) Network changes and updates need to

be managed correctly at a low cost. A network is a dynamic system and the state

of a network may change frequently because of a new network policy enforcement,

a bug-fix of existing network states, an installation of new network devices,

etc. It is important to handle these different updates correctly to guarantee a

smooth functioning of a network.

This thesis addresses these three problems by proposing a constraint solver

based framework that can be applied to these problems and experimentally

evaluates its scalability and feasibility. My study demonstrates that the

constraint based solution is capable of handling the verification problem, the

firewall management problem, and the update problem for medium sized networks

in reasonable time.