Foundations for practical network verification

Kheradmand, Ali

Permalink

https://hdl.handle.net/2142/113886 Copy

Description

Title

Foundations for practical network verification

Author(s)

Kheradmand, Ali

Issue Date

2021-12-02

Director of Research (if dissertation) or Advisor (if thesis)

Godfrey, Brighten

Doctoral Committee Chair(s)

Godfrey, Brighten

Committee Member(s)

• Rosu, Grigore
• Xu, Tianyin
• Padhye, Jitendra

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)

• network verification
• formal verification
• data plane verification
• network reliability
• symbolic execution
• packet equivalence class
• intent inference
• invariant detection
• policy mining
• network behavior summarization
• anomaly analysis
• misconfiguration detection
• hierarchical clustering
• r-tree
• p4 language
• formal semantics
• semantics based analysis
• model checking
• deductive verification
• translation validation

Abstract

Computer networks are large and complex and the often manual process of configuring such systems is error-prone, leading to network outages and breaches. This has ignited research into network verification tools that given a set of operator intents, automatically check whether the configured network satisfies the intents. In this dissertation, we argue that existing works in this area have important limitations that prevent their widespread adoption in the real world. We set to address these limitations by revisiting the main aspects of network verification: verification framework, intent specification, and network modeling. First, we develop #PEC, a symbolic packet header analysis framework that resolves the tension between expressiveness and efficiency in previous works. We provide an extensible library of efficient match-types that allows encoding and analyzing more types of forwarding rules (e.g. Linux iptables) compared to most previous works. Similar to the state-of-the-art, #PEC partitions the space of packet headers into a set of equivalence classes (PECs) before the analysis. However, it uses a lattice-based approach to do so, refraining from using computationally expensive negation and subtraction operations. Our experiments with a broad range of real-world datasets show that #PEC is 10× faster than similarly expressive state-of-the-art. We also demonstrate how empty PECs in previous works lead to unsound/incomplete analysis and develop a counting-based method to eliminate empty PECs from #PEC that outperforms baseline approaches by 10 − 100×. Next, we note that network verification requires formal specifications of the intents of the network operator as a starting point, which are almost never available or even known in a complete form. We mitigate this problem by providing a framework to utilize existing low-level network behavior to infer the high-level intents. We design Anime, a system that given observed packet forwarding behavior, mines a compact set of possible intents that best describe the observations. Anime accomplishes this by applying optimized clustering algorithms to a set of observed network paths, encoded using path features with hierarchical values that yield a way to control the precision-recall tradeoff. The resulting inferred intents can be used as input to verification/synthesis tools for continued maintenance. They can also be viewed as a summary of network behavior, and as a way to find anomalous behavior. Our experiments, including data from an operational network, demonstrate that Anime produces higher quality (F-score) intents than past work, can generate compact summaries with minimal loss of precision, is resilient to imperfect input and policy changes, scales to large networks, and finds actionable anomalies in an operational network. Finally, we turn our attention to modeling networking devices. We envision basing data plane analysis on P4 as the modeling language. Unlike most tools, we believe P4 analysis must be based on a precise model of the language rather than its informal specification. To this end, we develop a formal operational semantics of the P4 language during the process of which we have identified numerous issues with the design of the language. We then provide a suite of formal analysis tools derived directly from our semantics including an interpreter, a symbolic model checker, a deductive program verifier, and a program equivalence checker. Through a set of case studies, we demonstrate the use of our semantics beyond just a reference model for the language. This includes applications for the detection of unportable code, state-space exploration, search for bugs, full functional verification, and compiler translation validation.

Graduation Semester

2021-12

Type of Resource

Thesis

Permalink

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

Copyright and License Information

Copyright 2021 Ali Kheradmand

Owning Collections