DBVal: Validating P4 Data Plane Runtime Behavior

The P4 software ecosystem to operate programmable data planes is increasingly becoming complex. The packet-processing behavior is defined by several components: the P4 program, the compiler that maps P4 programs to resource-constrained switch pipeline, the control-plane program that installs rules, and the switch software agents that configure the data plane. Bugs in any one or more of these components would potentially introduce packet-processing errors in the data plane. Prior work verifies P4 programs before deployment and found many program bugs. But bugs can happen in other components after the program deployment and may not be found during testing and only manifest themselves in production.

In this work, our goal is to detect packet-processing errors induced by bugs that are not caught (or are difficult to catch) before the P4 program deployment. Our key idea is to let P4 programmers specify the intended packet-processing behavior and validate the actual packet-processing behavior against the intended behavior at runtime. We obtain intended behavior from the P4 programmers in the form of assertions, where each assertion specifies which tables and actions should be applied and in what order on a certain subset of traffic. Next, the assertions are compiled and translated to P4 implementation such that the implementation efficiently tracks the packet execution path, that is, the set of tables applied and actions executed, and then validates the tracked behavior at line rate. We show that our techniques can be used to effectively detect bugs that are difficult, if not impossible, to catch with existing techniques for testing and verifying programmable data planes.