Formal Specifications for Data Plane Programs

Networks are complex in nature consisting of numerous configurations. Each network configuration requires careful consideration due to the high runtime impact. Software-defined Networking (SDN) opens control plane and data plane programmability for the end user. The network programmability, on one hand, allows flexibility of defining custom headers and protocols. On the other hand, it opens new horizons of network misconfigurations. Formal methods are being applied in various domains for building robust systems. Recent studies explored the applications of formal methods in network programming. This paper explores the possibility of using Backus-Naur Form (BNF) for writing formal specifications for P4 parsers and tables. The compiler checks at compile time that the specifications are consistent with the implementation and ensures correctness.