Please use this identifier to cite or link to this item:
http://arks.princeton.edu/ark:/88435/dsp011v53k128c
Title: | Foundationally Verified Data Plane Programming |
Authors: | Wang, Qinshi |
Advisors: | Appel, Andrew W. |
Contributors: | Computer Science Department |
Keywords: | Formal verification Software-defined networking |
Subjects: | Computer science Computer engineering Logic |
Issue Date: | 2023 |
Publisher: | Princeton, NJ : Princeton University |
Abstract: | P4 is a major standardized programming language for programming and specifying the network data plane. P4 is widely used in a variety of network functionalities, including monitoring, traffic management, forwarding, and security. Recently, stateful applications have been emerging in this area, as supported by programmable hardware. Typical stateful applications include network telemetry (heavy hitters, distributed denial-of-service (DDoS) detection, performance monitoring), middleboxes (firewalls, network address translation (NAT), load balancers, intrusion detection), and distributed services (in-network caching, lock management, conflict detection). Their complexity and rich properties are beyond the ability of existing P4 verifiers. In this thesis, we propose Verifiable P4: a new framework for P4 program verification based on interactive theorem proving that is (1) capable of proving multi-packet properties, (2) modular in terms of the structure of P4 programs, and (3) foundationally sound with respect to a mechanized formal semantics of P4. In order to achieve these goals, we built (1) a mechanized formal semantics of P4 more comprehensive and convenient than existing formal semantics, (2) a set of program logic rules that are proven sound, and (3) an interactive verification system based on the program logic and Coq tactic mechanism. We verified a stateful firewall fully implemented in P4 using a sliding-window Bloom filter with Verifiable P4 and evaluated its utility. |
URI: | http://arks.princeton.edu/ark:/88435/dsp011v53k128c |
Type of Material: | Academic dissertations (Ph.D.) |
Language: | en |
Appears in Collections: | Computer Science |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Wang_princeton_0181D_14768.pdf | 860.86 kB | Adobe PDF | View/Download |
Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.