[Nets-seminars] Nets talk by Costin Raiciu

[Mark Handley]

Costin Raiciu will be giving a talk on Thursday on the work his group just got into Sigcomm.  It's really nice work - abstract below.  Foster Court 219 at 2pm.

Mark


Title: Debugging P4 programs with Vera

Abstract: 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 in a novel language we call NetCTL. To enable scalable, exhaustive verification of P4 programs with concrete table entries, Vera automatically generates all valid header layouts and uses a novel data-structure for match-action processing optimized for verification. These techniques allow Vera to scale very well: it only takes between 5s-15s to track the execution of a purely symbolic packet in the largest P4 program currently available (6KLOC) and can compute SEFL model updates according to table insertions and deletions in milliseconds. Vera can also explore multiple concrete dataplanes at once by allowing the programmer to insert symbolic table entries; the resulting verification highlights possible failures resulting from faulty dataplane entries, and can help debug controller programs. 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 each of them in seconds/minutes.

Bio: Costin Raiciu is Associate Professor in the CS department of the University Politehnica of Bucharest, where he leads a research group working on networking, systems and verification. He has finished his PhD at UCL working with Mark Handley, and some of his better known previous work is on  Multipath TCP.