P4 is a major standardized programming language for programming and specifying the network data plane. P4 is widely applied 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 P4 program modules, 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 the sliding-window Bloom filter with Verifiable P4 and evaluated its utility.