Withdraw
Loading…
Practical verification of network planes
Prabhu Muraleedhara Prabhu, Santhosh
Loading…
Permalink
https://hdl.handle.net/2142/108300
Description
- Title
- Practical verification of network planes
- Author(s)
- Prabhu Muraleedhara Prabhu, Santhosh
- Issue Date
- 2020-05-05
- Director of Research (if dissertation) or Advisor (if thesis)
- Caesar, Matthew C
- Doctoral Committee Chair(s)
- Caesar, Matthew C
- Committee Member(s)
- Godfrey, Philip B
- Xu, Tianyin
- Mishchenko, Alan
- Panda, Aurojit
- 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)
- Computer Networks, Formal Verification
- Abstract
- Formal network verification is a rapidly advancing field of research, encompassing a wide array of verticals such as data plane verification, configuration verification, network software verification etc. More and more real-world networks are deploying network verification as a tool to prevent outages and vulnerabilities. However, the fundamental challenges of scope and scalability make network verification unusable in a significant fraction of real-world networks. In this thesis, we discuss a new generation of verification techniques, algorithms and data structures designed to make network verification more universally applicable. We first present Plankton, a configuration verification platform that combines efficient explicit state model checking with domain-specific optimizations to enhance the scalability of configuration verification. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000× speedup compared to the state of the art. Then, we discuss how the model checking-based technique can be used to verify network dataplanes with software components. We propose Plankton-neo, a tool for checking such dataplanes without the need for faithful middlebox models. Our design is effectively a hybrid, using an explicit-state model checker to explore all network-wide execution paths and event orderings, but executing real software as a subroutine for each device. Plankton-neo incorporates predefined models of specific protocols such as TCP and ICMP, along with a rich collection of policies that can be checked over dataplanes incorporating NFV components. We show that Plankton-neo can detect correctness issues that would be missed both by existing verification and testing approaches, and describe an implementation that can scale to large networks with good performance. Finally, we identify the fundamental challenges for scalable dataplane verification in the real world and propose ways to solve them better than the state of the art. We describe a new data structure for representing symbolic sets of packets for dataplane verification. Our design is inspired by Binary Decision Diagrams, but is able to overcome some specific limitations of BDDs in the context of storing packet sets. We describe a set of benchmark traces for evaluating packet set data structures, and perform an experimental comparison of our proposed data structure with BDDs. The experiments show that we are able to improve the time and memory overhead by significant amounts compared to BDDs.
- Graduation Semester
- 2020-05
- Type of Resource
- Thesis
- Permalink
- http://hdl.handle.net/2142/108300
- Copyright and License Information
- Copyright 2020 Santhosh Prabhu Muraleedhara Prabhu
Owning Collections
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisDissertations and Theses - Computer Science
Dissertations and Theses from the Dept. of Computer ScienceManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…