University of Illinois Urbana-Champaign

Guided synthesis of network behavior

Zhou, Wenxuan

Content Files
ZHOU-DISSERTATION-2017.pdf

Permalink

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

Description

Title
Guided synthesis of network behavior
Author(s)
Zhou, Wenxuan
Issue Date
2017-12-05
Director of Research (if dissertation) or Advisor (if thesis)
Caesar, Matthew
Doctoral Committee Chair(s)
Caesar, Matthew
Committee Member(s)
  • Borisov, Nikita
  • Godfrey, Brighten
  • 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
2018-03-13T17:35:41Z
Keyword(s)
  • Network management
  • Verification
  • Synthesis
Abstract
In the past decades, the world has witnessed how essential modern networks, such as data centers and enterprise networks, have become in our daily lives. However, on the other hand, configuring and maintaining a modern network, is a challenging and error-prone process. Administrators must often consider security policies from a variety of sources simultaneously, including regulatory requirements, industry standards, to mitigate attack vectors. Erroneous implementation of a policy, however, can result in costly data breaches and intrusions. Relying on humans to discover and troubleshoot violations is slow and prone to error, considering the speed at which new attack vectors propagate and the increasing network dynamics, partly an effect of SDN. To ensure the network is always in a state consistent with the desired policies, administrators need frameworks to automatically diagnose and repair violations as the network evolves. To address this problem, in this dissertation, we present a system automatically synthesizing network changes that meets a network correctness specification given as a policy. If we consider a network as a distributed program, the problem here is essentially a program synthesis problem. Recent work on program synthesis illustrates many benefits of allowing the user to augment the correctness specification with some guidance. We adopt a similar philosophy: our system is guided by user instructions to constrain the space of allowed implementations in order to keep pace with network dynamics. As the foundation of our system, we first develop a verification technique that detects network-wide invariant violations responsively. Based on the verification results, our core algorithm repairs network updates in two aspects. If an update violates a policy defined by an administrator, such as reachability or segmentation, our algorithm transforms the update into one that complies with the policy. In addition, given two correct network states, our algorithm synthesizes a feasible and efficient update ordering to migrate the network from one to the other. With our prototype implementation, we tested our system on physical testbed, emulated SDN networks, and a large enterprise network’s operational traces. We demonstrated that it is practical and efficient to use user instructions as guidance to incrementally build/maintain a network state, where desirable properties are automatically preserved all the time.
Graduation Semester
2017-12
Type of Resource
text
Permalink
http://hdl.handle.net/2142/99498
Copyright and License Information
Copyright 2017 Wenxuan Zhou

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Siebel School of Computer Science