A Simple Approach to Verify and Debug Data Plane Programs

The advances in data plane programmability through domain-specific languages such as P4 require the adoption of verification methods to ensure that a given code behaves appropriately. The standard approach in the literature is to use formal methods to verify a provided software. However, traditional techniques are often time-consuming and expensive. In this work, we propose a model to demonstrate the behavior of a P4 program that is simple and fast. To validate our model, we have used a name-based forwarding program and a control plane application that injects in a P4 table a total of 1 million random name prefixes. The results have shown that our model can quickly indicate whether or not a given program is behaving correctly.