P4 Switch Code Data Flow Analysis: Towards Stronger Verification of Forwarding Plane Software

With the advent of languages like POF and P4 and the ability to write code for redefining switch behavior, software verification becomes paramount to avoid network and service disruption due to buggy implementations. Various techniques like symbolic execution, annotations, and assertions have been recently used to ensure bug-free switch code. In spite of the potentialities, they are limited in the classes of errors they can capture. More importantly, existing proposals for switch program verification often require a programmer to write custom verification code (e.g., annotations), an error-prone approach in itself. In this paper, we present the design and implementation of p4-data-flow, a practical tool which uses data flow analysis for verification of switch programs. We focus on the P4 language, and present experiments showing that data flow analysis may reveal defects from classes not yet covered by existing work, without demanding further programmer effort.

I. INTRODUCTION

The concept of programmable forwarding planes has experienced a renewed research interest since the advent of Software Defined Networking (SDN) [1], [2]. Domain-specific languages like POF [3] and P4 [4] now allow network operators to redefine how forwarding devices parse and process packets, thus enabling faster provisioning of novel and/or home-brewed protocols, and unleashing innovation in the forwarding plane.