P4 Formalization
Software-Defined Networking (SDN) permits programming the data plane of the network devices using languages such as P4. This capability can impact network correctness due to error-prone programs. To address this, 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.
Researchers
Publications
- HOL4P4: semantics for a verified data plane. A Alshnakat, D Lundberg, R Guanciale, M Dam, K Palmskog. EuroP4 '22: Proceedings of the 5th International Workshop on P4 in Europe. 2022.