University of Illinois Urbana-Champaign

Monitoring and verifying network behavior using data-plane state

Khurshid, Ahmed

Content Files
KHURSHID-DISSERTATION-2015.pdf

Permalink

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

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
Date of Ingest
2016-05-04T21:49:06Z
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

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois