Files in this item

FilesDescriptionFormat

application/pdf

application/pdfPRABHUMURALEEDHARAPRABHU-DISSERTATION-2020.pdf (5MB)Restricted Access
(no description provided)PDF

Description

Title:Practical verification of network planes
Author(s):Prabhu Muraleedhara Prabhu, Santhosh
Director of Research:Caesar, Matthew C
Doctoral Committee Chair(s):Caesar, Matthew C
Doctoral Committee Member(s):Godfrey, Philip B; Xu, Tianyin; Mishchenko, Alan; Panda, Aurojit
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(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.
Issue Date:2020-05-05
Type:Thesis
URI:http://hdl.handle.net/2142/108300
Rights Information:Copyright 2020 Santhosh Prabhu Muraleedhara Prabhu
Date Available in IDEALS:2020-08-27
Date Deposited:2020-05


This item appears in the following Collection(s)

Item Statistics