Validando modelos para verificação de programas P4 por execução simbólica

Abstract

A linguagem P4 permite a programação do plano de dados de dispositivos de rede, facilitando a criação de novos protocolos e funcionalidades. No entanto, ao passo que planos de dados programáveis aumentam a flexibilidade de Redes Definidas por Software (SDN), aumentam também a chance de erros devido à possibilidade de bugs nos programas implementados. A fim de prevenir falhas provenientes da programação do plano de dados, técnicas de teste e verificação podem ser aplicadas para encontrar erros antes da implantação de softwares nos dispositivos de rede. Neste trabalho, é apresentada uma metodologia de validação de modelos para a ferramenta de verificação de programas P4 assert-p4.

The P4 programming language allows a network device’s dataplane to be programmed, simplifying the introduction of new protocols and features. However, while programmable dataplanes improve flexibility for Software-Defined Networking (SDN), they also increase the chance of errors due to possible bugs in the implemented software. In order to prevent failures arising from dataplane programmability, testing and verification techniques can be applied to identify errors before a software’s implementation on network devices. In this work, we present a model validation methodology for assert-p4, a P4 program verification tool.