P4 switch code data flow analysis : towards stronger verification of forwarding plane software

• Ano de defesa: 2020
• Autor(a) principal: Birnfeld, Karine
• Orientador(a): Cordeiro, Weverton Luis da Costa
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Palavras-chave em Português: Software
• Palavras-chave em Inglês: Programmable Network; Programmable Dataplane; Software Testing.; Data Flow Testing
• Link de acesso: http://hdl.handle.net/10183/213157

O advento de linguagens específicas de domínio como POF e P4 permitiram pela primeira vez que operadores de rede pudessem prontamente redefinir como os dispositivos de encaminhamento de dados (por exemplo, switches) interpretam e processam pacotes em uma Rede Definida por Software (SDN). Nesse contexto, a verificação de software para o plano de dados desenvolvido “em casa” se torna fundamental para evitar interrupções na rede e no serviço devido a problemas de implementação. Várias técnicas, como execução simbólica, anotações e asserções, foram usadas recentemente para garantir códigos de planos de dados programáveis livres de erros. Apesar das potencialidades, elas são limitadas nas classes de erros que podem capturar. Mais importante, as propostas existentes para verificação do programa de switch geralmente exigem que o programador escreva um código de verificação personalizado (por exemplo, anotações), uma abordagem propensa a erros. Nesta dissertação, apresentamos o design e a implementação do P4-DATA-FLOW, uma ferramenta prática que utiliza a análise de fluxo de dados para verificação de programas de switch. Nós nos concentramos na linguagem P4 e apresentamos experimentos mostrando que a análise do fluxo de dados pode revelar defeitos de classes ainda não cobertas pelos trabalhos existente, sem exigir mais esforço do programador.