PLACIDUS : Plataforma de gerenciamento com verificação formal para redes definidas por software

Abstract

Verificação formal é um passo importante na checagem de operações e propriedades em redes de computadores, como por exemplo, a corretude das configurações de dispositivos inseridos na mesma. Entretanto, historicamente, técnicas de verificação formal são limitadas por desempenho, escalabilidade e expressividade, principalmente devido à complexidade das redes de computadores atuais. Problemas para processar uma tarefa ou função específica em uma rede podem ser críticos para a confiabilidade de um sistema como um todo. Além disso, a execução de testes ficam limitadas, na maioria das ocasiões, ao ambiente final de produção. Com validações feitas apenas em estágios mais avançados, quaisquer modificações necessárias ao sistema se tornam caras, e muitas vezes, demoradas. Para tratar essa combinação de problemas, várias técnicas para verificação formal podem ser utilizadas em estágio inicial de desenvolvimento. Essas técnicas podem ser (i) atualização das informações sobre os contextos e estados de dispositivos da rede e (ii) utilização de estratégicas inteligentes para combinar modelos de representação para garantir performance e escalabilidade. Ademais, é preciso um ambiente para simulações de rede para que essas regras sejam verificadas, o qual contenha um emulador de rede e um controlador de rede para obtenção dos fluxos a serem validados dentro da topologia. Arquiteturas para SDN oferecem a essência necessária para resolver problemas desse tipo, uma vez que disponibilizam a combinação de diferentes técnicas para aumentar a qualidade dos resultados obtidos por um sistema de seleção. Nesse trabalho, é proposto o Placidus, que é uma plataforma de gerenciamento com verificação formal para SDN. A plataforma possui incluso um sistema de autenticação de usuários. Ademais, ela tem um dashboard, onde é possível fazer o gerenciamento de topologias de rede, além de ser possível executar a verificação de propriedades das mesmas. A plataforma utiliza um framework flexível, que atualmente possui scripts de verificação para verificar alcançabilidade entre dispositivos de rede, além de inconsistências entre fluxos, tais como redundâncias e conflitos de regras.

Formal verification is an important step in checking network operations and ensuring properties, for instance, the accuracy of device configurations. Nevertheless, historically, formal verification techniques are limited by performance, scalability, and expressiveness, mainly due to the complexity of the current networks. Problems on processing a specific task or function in computer networks may be critical for the reliability of a whole system. Furthermore, the executions of tests are mostly limited to the final production environment. With variations made only in advanced stages, any needed changes to the system become expensive and very time-consuming. In order to solve these possible complications, several techniques for formal verification can be used in early developing stages. These techniques can be (i) updating the information about the context and state of network devices, and (ii) using intelligent strategies for combining representation models for guaranteeing performance and scalability. In addition, an environment for simulations is required in order to have rules verified within the network topology. This environment ought to have at least a network emulator and a network controller to obtain the flows within the topology. Software defined networking (SDN) architectures offer the essence needed for resolving this kind of issue. It enables the selection of a set of different techniques for increasing the quality of the results obtained by a selection system. In this work, we propose Placidus, which is a platform of management with formal verification for software defined networking. The platform has a user authentication system included. Besides, it has a dashboard where network topologies can be created and rules in it can be verified. It uses a flexible framework, which is currently capable of verifying network properties, such as reachability, redundancy in network devices, and other inconsistencies.