Princeton University

School of Engineering & Applied Science

Computer Network Verification and Management Using Constraint Solvers

Shuyuan Zhang
Engineering Quadrangle J401
Tuesday, February 16, 2016 - 2:00pm to 3:30pm

Today’s computer networks have become extremely large and complicated. The increased scale is observed in datacenters, which can have hundreds of thousands of network devices. The increased complexity is due to multiple kinds of networking devices (routers, switches, etc.) that need to work together to execute diverse network functions such as routing, access control, and etc. 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. (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.