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 and type system using the interactive theorem prover HOL4. This semantics allows us to analyze 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. HOL4P4: mechanized small-step semantics for P4. A Alshnakat, D Lundberg, R Guanciale, M Dam. Proceedings of the ACM on Programming Languages, Volume 8, Issue OOPSLA1. 2024. Proof-Producing Symbolic Execution for P4. D Lundberg, R Guanciale, M Dam. Verified Software. Theories, Tools and Experiments (VSTTE 2024).