P4R-Type: A Verified API for P4 Control Plane Programs

Explore a 19-minute conference talk from OOPSLA2 2023 that introduces P4R-Type, a novel verified P4Runtime API for Scala. Delve into the world of Software-Defined Networking (SDN) and learn how P4R-Type addresses critical risks in programming SDN devices. Discover how this innovative approach performs static checks for P4 control plane operations, preventing mismatches between P4 tables, allowed actions, and action parameters. Examine the FP4R calculus and its typing system, which form the formal foundation of P4R-Type, ensuring well-typed programs never issue invalid P4Runtime operations. Gain insights from three case studies evaluating the safety and flexibility of P4R-Type. Understand the significance of this groundbreaking work in formalizing P4Runtime control plane applications and establishing a typing discipline for P4Runtime operations correctness.