Recent advances in Software Defined Networking (SDN) have expanded our ability to program the network to its data plane. Through domain specific languages like P4, network operators can quickly deploy new protocols on forwarding devices, customize their functionality, and develop innovative services. This flexibility comes however with a cost: network-wide security and correctness properties (e.g., isolation, reachability, etc.) become much harder to ensure, because network behavior is now determined by a combination of the control plane-driven configuration and the data plane program that resides on devices (also called switches). Existing network verification tools, which rely on a fixed, invariant model of the data plane, are inadequate for programmable data planes.
In our P4Sec project, we research new techniques to verify and enforce security properties in data plane networks. The verification techniques we work on extend existing verification tools by automatically generating a data plane model from a P4 program. We also work on adapting existing verification tools to integrate with our dynamically-generated models to verify network configuration updates issued by an SDN controller. We also research novel approaches to ensure that network security properties are satisfied by a network configuration that is based on data plane enforcement. We work to develop an in-line monitor, implemented in the data plane itself, that enforces critical security properties, such as isolation and bandwidth limits, even in the presence of a faulty user data plane program or controller.