We present Vera, a tool that exhaustively verifies P4 programs using symbolic execution. Vera automatically uncovers a number of common bugs including parsing/deparsing errors, invalid memory accesses, loops and tunneling errors, among others. Vera can also be used to verify user-specified properties described in a novel specification language called NetV. To enable scalable, exhaustive verification Vera automatically generates of all valid header layouts, uses symbolic table entries to simulate a variety of table rule snapshots and uses novel data-structure for match-action processing optimized for verification. These techniques allow Vera to scale very well: it only takes around 30 seconds to track the execution of a purely symbolic packet in the largest P4 program currently available (6K LOC of P4) and can process online table insertions and deletions in huge match-action tables in under one second. We have used Vera to analyze all P4 programs we could find including the P4 tutorials, P4 programs in the research literature and the switch code from https://p4.org. Vera has found several bugs in all of them.

About Radu Stoenescu

Radu Stoenescu is a student during the final year of his Masters studies at University Politehnica of Bucharest under supervision by Costin Raiciu. His research interests are static analysis, formal verification and, in particular, and symbolic execution.

This event will be conducted in English