Skip navigation
Please use this identifier to cite or link to this item:
Title: Computer Network Verification and Management using Constraint Solvers
Authors: Zhang, Shuyuan
Advisors: Malik, Sharad
Contributors: Electrical Engineering Department
Keywords: Computer Network
Data Plane
Formal Method
Subjects: Computer science
Issue Date: 2016
Publisher: Princeton, NJ : Princeton University
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.
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Electrical Engineering

Files in This Item:
File Description SizeFormat 
Zhang_princeton_0181D_11656.pdf3.35 MBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.