P4 Formalization

Anoud Alshnakat

Software-Defined Networking (SDN) permits programming the data plane of the network devices using languages such as P4. This capability can impact the network correctness due to the error-prone programs. Therefore, we have built a formalization of P4 semantics using the interactive theorem prover HOL4. This semantics allows us to analyse security properties in P4 packet forwarding programs. Finally, we are planning to develop verification tools and generate a verified interpreter for the language.