Enforcing properties in programmable networks

• Ano de defesa: 2020
• Autor(a) principal: Neves, Miguel Cardoso
• Orientador(a): Barcellos, Antonio Marinho Pilla
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Palavras-chave em Português: Redes programáveis; Rede definida por software; Monitoramento de rede; Escalabilidade
• Palavras-chave em Inglês: Network verification; Network debugging; SDN; P4
• Link de acesso: http://hdl.handle.net/10183/212265

Evitar bugs e erros de configuração em redes programáveis é um desafio. Estudos recentes mostram que essas estão entre as maiores causas de falhas em infraestruturas de rede. Além disso, as consequências dessas falhas podem ser catastróficas. Trabalhos na literatura propõem técnicas de depuração e verificação de redes como forma de checar se a infraestrutura está funcionando da maneira esperada, mas tais técnicas comumente levam a soluções incapazes de identificar todos os bugs e enfrentam sérios problemas de escalabilidade. Nesta tese nós introduzimos o conceito de monitores de planos de dados, módulos especiais que permitem a programadores de rede assegurar propriedades de interesse de forma expressiva e escalável. Juntamente com o sistema que estamos propondo para instrumentar programas de rede com monitores de planos de dados, chamado P4box, nosso mecanismo cria um núcleo de proteção que não pode ser impedido, violado ou evitado por programas sujeitos a falhas. A fim de mostrar os benefícios do nosso mecanismo, exploramos dois casos de uso: assegurar propriedades dinamica e estaticamente. Enquanto o primeiro é útil em cenários onde verificação não consegue atingir restrições de tempo, o segundo permite a verificação de propriedades que não eram possíveis até então. Resultados mostram que monitores de planos de dados implicam numa baixa sobrecarga aos dispositivos de rede em termos de latência e consumo de recursos ao assegurar propriedades dinamicamente. Além disso, eles permitem que o sistema proposto (i.e., P4box) verifique propriedades de rede como atingibilidade entre hosts em grandes topologias (com mais de 190 roteadores) em poucos minutos.