SwitchV: Automated SDN Switch Validation with P4 Models
Abstract
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.
Research Areas
