SWITCHV: Automated SDN Switch Validation with P4 Models

Increasing demand on computer networks continuously pushes manufacturers to incorporate novel features and capabilities into their switches at an ever-accelerating pace. However, the traditional approach to switch development relies on informal specifications and handcrafted tests to ensure reliability, which are tedious and slow to maintain and update, effectively putting feature velocity at odds with reliability. This work describes our experiences following a new approach during the development of switch software stacks that extend fixed-function ASICs with SDN capabilities. Specifically, we focus on SWITCHV, our system for automated end-to-end switch validation using fuzzing and symbolic analysis, that evolves effortlessly with the switch specification. Our approach is centered around using the P4 language to model the data plane behavior of the switch as well as its control plane API. Such P4 models are then used as a formal specification by SWITCHV, as well as a switch-agnostic contract by SDN controllers, and a living documentation by engineers. SWITCHV found a total of 154 bugs spanning all switch layers. The majority of bugs were highly relevant and fixed within 14 days.