Enforcing properties in programmable networks

Abstract

Avoiding software bugs and misconfigurations in programmable networks is challenging. Recent studies show that they are among the biggest causes of failures in network infrastructures. Moreover, their consequences can be disastrous. Previous efforts have proposed network debugging and verification techniques as a means to check that the network behaves as expected, but these techniques usually lead to incomplete solutions that can not catch all bugs or face severe scalability issues. In this thesis, we introduce the abstraction of data plane monitors, special modules that allow network programmers to enforce desired properties in a scalable and expressive way. Together with P4box, a system we propose for instrumenting data plane programs with monitors, our abstraction creates an enforcement kernel that cannot be hindered, tampered or circumvented by faulty code. To assess the benefits of our mechanism, we are exploring two use cases: dynamic and static property enforcement. The former is useful when verification does not meet time constraints while the latter enables the verification of previously unfeasible properties. Our experiments using P4box in programmable network hardware show that monitors represent a small overhead in terms of latency and resource consumption when dynamically enforcing a broad range of properties. Moreover, they enable P4box to verify (or statically enforce) reachability properties for large networks (> 190 routers) within a few minutes using off-the-shelf equipment.

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.