Verification of P4 programs in feasible time using assertions

An optional shortened abstract.

Uncovering Bugs in P4 Programs with Assertion-based Verification

An optional shortened abstract.

POSTER: Finding vulnerabilities in P4 programs with assertion-based verification

Current trends in SDN extend network programmability to the data plane through the use of programming languages such as P4. In this context, the chance of introducing errors and consequently software vulnerabilities in the network increases …

Sandboxing Data Plane Programs for Fun and Profit

This paper describes the design and implementation of a general-purpose compile-time sandbox for P4 data plane programs. Our mechanism allows a supervisor to interpose on another program's interaction with the forwarding device. The sandboxing …