Aluno: Lucas Menezes Freire
Orientador: Prof. Dr. Antonio Marinho Pilla Barcellos
Coorientador: Prof. Dr. Alberto Egon Schaeffer Filho
Título: Uncovering Bugs in P4 Programs with Assertion-based Verification
Linha de Pesquisa: Segurança Cibernética
Local: Prédio 43412 – AUD-0 (auditório 0) do Instituto de Informática.
-Prof. Dr. Theophilus Benson (Brown University – por videoconferência)
-Prof. Dr. Guofei Gu (TAMU – por videoconferência)
-Prof. Dr. Luciano Paschoal Gaspary (UFRGS)
Presidente da Banca: Prof. Dr. Antonio Marinho Pilla Barcellos
Abstract: Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. To prevent bugs from violating network properties, the techniques of enforcement or verification can be applied. While enforcement seeks to actively monitor the data plane to block property violations, verification aims to find bugs by assuring that the program meets its requirements. Existing data plane verification approaches that are able to model P4 programs present severe restrictions in the set of properties that can be verified. In this work, we propose Assert-P4, a data plane program verification approach based on assertions and symbolic execution. Network programmers annotate P4 programs with assertions expressing general correctness properties. The annotated programs are transformed into C models and all their possible paths are symbolically executed. Since symbolic execution is known to have scalability challenges, we also propose a set of techniques that can be applied in this domain to make verification feasible. Namely, we investigate the effect of the following techniques on verification performance: parallelization, compiler optimizations, packet and control flow constraints, bug reporting strategy, and program slicing. We implemented a prototype to study the efficacy and efficiency of the proposed approach. We show it can uncover a broad range of bugs and software flaws, and can do it in less than a minute considering various P4 applications proposed in the literature. We show how a selection of the optimization techniques on more complex programs can reduce the verification time in approximately 85 percent.
Keywords: P4, Verification, Programmable Data planes.