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

Abstract

The advent of Domain Specific Languages (DSL) like POF and P4 has enabled for the first time network operators to quickly redefine how forwarding plane devices (e.g., switches) parse and process packets in a Software-Defined Network (SDN). In this context, proper verification of home-brewed forwarding plane software becomes paramount to avoid network and service disruption due to buggy implementations. Various techniques like symbolic execution, annotations, and assertions have been recently used to ensure bug-free forwarding plane code. In spite of the potentialities, they are limited in the classes of errors they can capture. More importantly, existing proposals for verifying forwarding plane software often require a programmer to write additional verification code (e.g., annotations), an error-prone approach in itself. In this dissertation, we present the design and implementation of P4-DATA-FLOW, a practical tool which uses data flow analysis for verification of switch programs. We focus on the P4 language, and present experiments showing that data flow analysis may reveal defects from classes not yet covered by existing work, without demanding further programmer effort

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.