Monitoring and verifying network behavior using data-plane state

Khurshid, Ahmed

Permalink

https://hdl.handle.net/2142/90066 Copy

Description

Title

Monitoring and verifying network behavior using data-plane state

Author(s)

Khurshid, Ahmed

Issue Date

2015-07-16

Director of Research (if dissertation) or Advisor (if thesis)

Caesar, Matthew C

Doctoral Committee Chair(s)

Caesar, Matthew C

Committee Member(s)

• Sanders, William H
• Borisov, Nikita
• Godfrey, Philip B
• Rexford, Jennifer

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Network debugging
• Data-plane verification
• Software-Defined Network

Abstract

Modern computer networks are complex, incorporating hundreds or thousands of network devices from multiple vendors performing diverse functions such as routing, switching, and access control across physical and virtual networks (VPNs and VLANs). As in any complex computer system, these networks are prone to a wide range of errors such as misconfigurations, software bugs, or unexpected interactions across protocols. Previous tools to assist operators in debugging network anomalies primarily focus on analyzing control plane configuration. Configuration analysis is limited in that it cannot find bugs in router software, and is harder to generalize across protocols since it must model complex configuration languages and dynamic protocol behavior. This thesis studies an alternate approach: diagnosing problems through static analysis of a network's data-plane state. We call it data-plane verification. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. To prove the applicability and usefulness of data-plane verification, we designed and implemented two tools to rigorously check important network invariants, such as absence of routing loops, routing consistency of replicated devices, and other reachability properties. Our first tool, called Anteater, translates a network's data-plane state and invariants into boolean satisfiability problems, and checks them using a SAT solver. Our second tool, called VeriFlow, creates a device independent graph model of the network state, and uses standard graph traversal algorithms to detect invariant violations. We tested our tools with real world network data-plane traces, and with large emulated networks. Both of our tools were able to detect real bugs that went unnoticed to network operators for more than a month. Our tools helped them to narrow down the faulty configurations, and resolve those quickly. Results from emulated larger networks showed that the running time performance of our tools, especially that of VeriFlow, is good enough to detect bugs quickly before they can be exploited by outside attackers. Due to the fast response time of VeriFlow, it can be used in the emerging Software-Defined Networking (SDN) setting as a proactive tool to detect and filter out faulty configurations before they reach network devices.

Graduation Semester

2015-08

Type of Resource

text

Permalink

http://hdl.handle.net/2142/90066

Copyright and License Information

Copyright 2015 Ahmed Khurshid

Owning Collections