Introduction
Introduction Statistics Contact Development Disclaimer Help
NETWORK DEVICE SOFTWARE GENERATION
by:
Shi, Ronghua
Se, Xi Yang Ronald
Thumbnail
Download
Web page
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.
Date Published: 2019-11-19 12:41:19
Identifier: networkdevicesof1094563503
Item Size: 111274165
Language: English
Media Type: texts
# Topics
networking device
software generation
software engineering
symbolic finite automata
unicast forwarding
MAC address learning
socket learning
stateful firewall
# Collections
navalpostgraduateschoollibrary
fedlink
# Uploaded by
@nps_calhoun_institutional_repository
# Similar Items
View similar items
PHAROS
You are viewing proxied material from tilde.pink. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.