Publication:
NETWORK DEVICE SOFTWARE GENERATION

Loading...
Thumbnail Image
Authors
Shi, Ronghua
Se, Xi Yang Ronald
Subjects
networking device
software generation
software engineering
symbolic finite automata
unicast forwarding
MAC address learning
socket learning
stateful firewall
Advisors
Volpano, Dennis M.
Date of Issue
2019-09
Date
Publisher
Monterey, CA; Naval Postgraduate School
Language
Abstract
Verification of data-plane software is limited to verifying point properties such as bounded packet processing time or not misinterpreting malformed packet headers, which usually are chosen to illustrate the merits of some verification technique. Therefore, these techniques can be thought of as vertical verification techniques. There are, however, many other properties of interest that vertical techniques do not address, such as timing, which is important for verifying the correct behavior of, say, a MAC address learning table. What is needed is a horizontal verification technique, one that enables us to reason about a wide variety of temporal properties. Volpano has proposed such a technique but with a major twist. Data-plane software is not verified ex post facto but rather, it is verified by construction. His approach focuses on building code that guarantees the assertions of the specification, instead of attempting to verify the assertions after the code has been generated. The correctness of complex networks can be verified by simply verifying the basic components that compose it. This thesis explores the feasibility of implementing such an approach by first specifying the behaviors of some basic network functions. More complex data-plane behavior, such as switching and firewalling, are then built using these basic functions. C code is then automatically generated for the data-plane that is guaranteed to exhibit the more complex behavior.Verification of data-plane software is limited to verifying point properties such as bounded packet processing time or not misinterpreting malformed packet headers, which usually are chosen to illustrate the merits of some verification technique. Therefore, these techniques can be thought of as vertical verification techniques. There are, however, many other properties of interest that vertical techniques do not address, such as timing, which is important for verifying the correct behavior of, say, a MAC address learning table. What is needed is a horizontal verification technique, one that enables us to reason about a wide variety of temporal properties. Volpano has proposed such a technique but with a major twist. Data-plane software is not verified ex post facto but rather, it is verified by construction. His approach focuses on building code that guarantees the assertions of the specification, instead of attempting to verify the assertions after the code has been generated. The correctness of complex networks can be verified by simply verifying the basic components that compose it. This thesis explores the feasibility of implementing such an approach by first specifying the behaviors of some basic network functions. More complex data-plane behavior, such as switching and firewalling, are then built using these basic functions. C code is then automatically generated for the data-plane that is guaranteed to exhibit the more complex behavior.
Type
Thesis
Description
Series/Report No
Department
Computer Science (CS)
Computer Science (CS)
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
Copyright is reserved by the copyright owner.
Collections