Header space analysis
Abstract/Contents
- Abstract
- In many engineering disciplines, such as digital design or software engineering, there is an abundance of theoretical foundations and practical tools for verification and debugging. In sharp contrast, the field of networking mostly relies on rudimentary tools such as ping and traceroute, together with the accrued wisdom and intuition of network administrators, for verification and debugging of networks. The verification and debugging of networks is difficult because (1) the forwarding state—the set of rules that determines how an incoming packet is processed and forwarded by network boxes—is distributed across multiple boxes, expressed in vendor dependent command line interface (CLI) formats, and is defined by the forwarding tables, filter rules, and other configuration parameters. As a result it is hard to observe and analyze the forwarding state and understand the overall system behavior. (2) The forwarding state is written by multiple independent programs, protocols, and humans. This may result in complex and unpredictable interactions between these independently generated forwarding states. Therefore, the first step in making tools for network verification and debugging is to create a simple model for the forwarding functionality of the network that abstracts away the complexities of understanding the forwarding state. One observation is that packet headers, despite carrying multiple protocols, are just sequences of bits, and networking boxes, despite all their complexities, simply rewrite and forward packet headers. Therefore, in our analytical framework, called the Header Space Analysis (HSA), a packet header is viewed as a flat sequence of bits and is modeled as a point in a {0,1}^L space, called the Header Space, where L is the length of the header. Each dimension in the header space corresponds to one bit in the packet header. Also, networking boxes are modeled as Transfer Functions, transforming packets from one point in the header space to another point or set of points. This easy-to-use formalism abstracts away the complexity of the protocols and vendor-specific semantics of network boxes and gives us a model to analytically prove properties about networks that are otherwise hard to ensure. In this dissertation, after introducing the header space analysis, I will describe three set of techniques and tools for network verification and testing based on HSA: 1) Hassel, a static and offline verification tool for verifying properties such as reachability of end hosts and finding loops and black holes 2) NetPlumber, a real time policy and invariant checking tool for networks and 3) Automatic Test Packet Generation (ATPG) framework for maximally testing network with the optimal number of test packets.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2013 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Kazemian, Peyman |
|---|---|
| Associated with | Stanford University, Department of Electrical Engineering. |
| Primary advisor | McKeown, Nick |
| Thesis advisor | McKeown, Nick |
| Thesis advisor | Prabhakar, Balaji, 1967- |
| Thesis advisor | Varghese, George, 1960- |
| Advisor | Prabhakar, Balaji, 1967- |
| Advisor | Varghese, George, 1960- |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Peyman Kazemian. |
|---|---|
| Note | Submitted to the Department of Electrical Engineering. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2013. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2013 by Peyman Kazemian
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...