programmable data planes

Dynamic Property Enforcement in Programmable Data Planes

An optional shortened abstract.

P4sec -- Securing Networks in the Programmable Data Plane Era

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.

Dynamic Property Enforcement in Programmable Data Planes

An optional shortened abstract.

Verification of P4 programs in feasible time using assertions

An optional shortened abstract.

Uncovering Bugs in P4 Programs with Assertion-based Verification

An optional shortened abstract.

POSTER: Finding vulnerabilities in P4 programs with assertion-based verification

Current trends in SDN extend network programmability to the data plane through the use of programming languages such as P4. In this context, the chance of introducing errors and consequently software vulnerabilities in the network increases …

Sandboxing Data Plane Programs for Fun and Profit

This paper describes the design and implementation of a general-purpose compile-time sandbox for P4 data plane programs. Our mechanism allows a supervisor to interpose on another program's interaction with the forwarding device. The sandboxing …