Skip navigation
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 SizeFormat 
Wang_princeton_0181D_14768.pdf860.86 kBAdobe PDFView/Download


Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.