Practical verification of network planes

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2020

Author dc:creator

• Prabhu Muraleedhara Prabhu, Santhosh

Contributors dc:contributor

• Caesar, Matthew C
• Godfrey, Philip B
• Xu, Tianyin
• Mishchenko, Alan
• Panda, Aurojit

• Computer Networks, Formal Verification

Statement dc:rights

• Copyright 2020 Santhosh Prabhu Muraleedhara Prabhu

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/108300

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/108300