Revised (new start time) ----------------------------------- Qinshi Wang will present his Pre FPO "Formally verifiable data plane programming" on Wednesday, April 20, 2022 in CS 401 at 1:30pm and Zoom. Zoom link: [ https://princeton.zoom.us/j/98911716346?pwd=eGltYUw0eWZ6MHRuUGhERXVnMEQrdz09 | https://princeton.zoom.us/j/98911716346?pwd=eGltYUw0eWZ6MHRuUGhERXVnMEQrdz09 ] . His committee is as follows: Andrew Appel (advisor) David Walker (reader) Nate Foster, Cornell (reader) Jen Rexford (examiner) Zachary Kincaid (examiner) All are welcome to attend. Title: Formally verifiable data plane programming Older-generation network devices were not end-user programmable. Software-defined network has been successful in separating the control plane and the data plane and providing more programmability for the control plane. But the data plane still lacks programmability. In recent years, programmable data plane devices and the P4 programming language, which programs these devices, have been developed. Because of P4's special language features for high-speed packet processing, and because extra consideration is needed to write P4 programs that fit into limited hardware resources, programming in P4 is hard and error-prone. Tools have been developed to check safety properties, but those are far from guaranteeing correctness. Meanwhile, P4 compilers and hardware may also have bugs. And when the network fails, it is hard to identify the cause between the P4 program, the compiler, and the hardware. We suggest that the solution is to adopt formal verification to P4 to make all the tools in the toolchain provably correct. Toward this goal, we first define an intermediate representation called P4light, which can encode the full P4 language after processing by the front end, and define the abstract syntax tree (AST) of P4light. We then define the mechanized operational semantics for P4light in the Coq proof assistant, according to the P4 specification and reference implementations. In the semantics, we establish a phase distinction between the instantiation phase (static resource allocation) and the execution phase. This phase distinction clarifies the explanation of the language, simplifies the operational semantics, and avoids tracking complicated objects when analyzing programs' behavior. Still, proving programs correct directly with respect to the semantics is too complicated to be tractable. So we build a verifier that helps users prove correctness of P4 programs. The verifier consists of an expressive program logic proved sound with respect to the semantics and a proof automation system that applies the program logic rules to prove programs correct. The verifier is powerful enough to prove the behavior of a Bloom filter on a sequence of packets with moderate human effort.