Show simple item record

dc.contributor.advisorBarcellos, Antonio Marinho Pillapt_BR
dc.contributor.authorFreire, Lucas Menezespt_BR
dc.date.accessioned2018-09-15T02:57:11Zpt_BR
dc.date.issued2018pt_BR
dc.identifier.urihttp://hdl.handle.net/10183/182010pt_BR
dc.description.abstractRecent 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.en
dc.description.abstractTendências recentes em redes definidas por software têm estendido a programabilidade de rede para o plano de dados através de linguagens de programação como P4. Infelizmente, a chance de introduzir bugs na rede também aumenta significativamente nesse novo contexto. Para prevenir bugs de violarem propriedades de rede, as técnicas de imposição e verificação podem ser aplicadas. Enquanto imposição procura monitorar ativamente o plano de dados para bloquear violações de propriedades, verificação visa encontrar bugs assegurando que o programa satisfaz seus requisitos. Abordagens de verificação de plano de dados existentes que são capazes de modelar programas P4 apresentam restrições severas no conjunto de propriedades que podem ser verificadas. Neste trabalho, nós propomos ASSERT-P4, uma abordagem de verificação de programas de plano de dados baseada em asserções e execução simbólica. Programadores de rede anotam programas P4 com asserções expressando propriedades gerais de corretude. Os programas anotados são transformados em modelos C e todos os seus caminhos possíveis são executados simbolicamente. Como execução simbólica é conhecida por possuir desafios de escalabilidade, nós também propomos um conjunto de técnicas que podem ser aplicadas neste domínio para tornar a verificação factível. Nomeadamente, nós investigamos o efeito das seguintes técnicas sobre o desempenho da verificação: paralelização, otimizações de compilador, limitações de pacotes e fluxo de controle, estratégia de reporte de bugs, e fatiamento de programas. Nós implementamos um protótipo para estudar a eficácia e eficiência da abordagem proposta. Nós mostramos que ela pode revelar uma ampla gama de bugs e defeitos de software, e é capaz de fazer isso em menos de um minuto considerando diversas aplicações P4 encontradas na literatura. Nós mostramos como uma seleção de técnicas de otimização em programas mais complexos pode reduzir o tempo de verificação em aproximadamente 85 por cento.pt_BR
dc.format.mimetypeapplication/pdfpt_BR
dc.language.isoengpt_BR
dc.rightsOpen Accessen
dc.subjectVerificationen
dc.subjectRedes : Computadorespt_BR
dc.subjectProgrammable Data Planesen
dc.subjectLinguagem de programaçãopt_BR
dc.titleUncovering bugs in P4 programs with assertion based verificationpt_BR
dc.title.alternativeRevelando bugs em programação P4 com verificação baseada em asserções pt
dc.typeDissertaçãopt_BR
dc.contributor.advisor-coSchaeffer Filho, Alberto Egonpt_BR
dc.identifier.nrb001075943pt_BR
dc.degree.grantorUniversidade Federal do Rio Grande do Sulpt_BR
dc.degree.departmentInstituto de Informáticapt_BR
dc.degree.programPrograma de Pós-Graduação em Computaçãopt_BR
dc.degree.localPorto Alegre, BR-RSpt_BR
dc.degree.date2018pt_BR
dc.degree.levelmestradopt_BR


Files in this item

Thumbnail
   

This item is licensed under a Creative Commons License

Show simple item record