Seed Project: Machine checkable verification of P4 programs

P4 is a programming language for controlling the data plane in programmable network devices such as routers and switches. The behaviour of switches programmed via P4 depends on the P4 program and the configuration of the control plane. This project has two main objectives: the identification of a proper formalization of security properties for systems configured via P4; and the development of the foundation for machine cheackable verification of P4 programs. To achieve these goals we will use an interactive theorem prover for modelling the semantics of (a subset of) the P4 language and devise a verification method to identify the possible control plane configurations that enable a given security property for a P4 program. While some verification tools for P4 have been made, existing analysis are not machine checkable and they do not take into account the interaction between the control plane and the data plane.



Scope: Formal Verification
Funding: CASTOR
Timeline: 2020
Main KTH Staff Involved: Roberto Guanciale
Other Partners: SAAB