Files in this item



application/pdfKHURSHID-DISSERTATION-2015.pdf (4MB)Restricted to U of Illinois
(no description provided)PDF


Title:Monitoring and verifying network behavior using data-plane state
Author(s):Khurshid, Ahmed
Director of Research:Caesar, Matthew C
Doctoral Committee Chair(s):Caesar, Matthew C
Doctoral Committee Member(s):Sanders, William H; Borisov, Nikita; Godfrey, Philip B; Rexford, Jennifer
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(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.
Issue Date:2015-07-16
Rights Information:Copyright 2015 Ahmed Khurshid
Date Available in IDEALS:2016-05-04
Date Deposited:2015-08

This item appears in the following Collection(s)

Item Statistics