Verification of P4 programs in feasible time using assertions

• DOI: 10.1145/3281411.3281421
• Publication Date: 2018-11-28T19:16:10Z
• Authors: Miguel Neves; Lucas Freire; Alberto Schaeffer...; Marinho Barcellos
• Keywords: Program slicing; Leverage (statistics)

Recent trends in software-defined networking have extended network programmability to the data plane. Unfortunately, chance of introducing bugs increases significantly. Verification can help prevent by assuring that program does not violate its requirements. Although research on verification P4 programs is very active, we still need tools make easier for programmers express properties and rapidly verify complex invariants. In this paper, leverage assertions symbolic execution propose a more general approach. Developers annotate with expressing correctness properties; result transformed into C models all possible paths symbolically executed. We implement prototype, use it show feasibility Because scale well, investigate set techniques speed up process specific case programs. prototype implemented gains provided three (use constraints, slicing, parallelization), experiment different compiler optimization choices. our tool uncover broad range bugs, do less than minute considering various applications.