Validation of availability and policy based management for programmable networks

Abstract

Software-Defined Networking (SDN) is a technology to develop communications networks that separates the network control layer from the data layer (packet forwarding). This separation allows greater flexibility when establishing new configurations. Thus, administrators can control the network through software without the need to access the physical configuration of each device. SDN networks have become important today due to the rapid growth of computer and network virtualization. Furthermore, this technology quickly responds to changes that may occur in the network due to its operation, failures or security incidents. That is, the network can be reprogrammed to respond to dynamic circumstances. Moreover, network functionalities such as load balancers, firewalls and intrusion detection systems can be programmed as logical rules of traffic. However, this technology is in continuous development and still faces interesting challenges for us. One of the challenge that generate high impact is errors in programming and configuration. These types of errors are the most common and account for between 50% and 80% of network failures. This dissertation seeks to contribute to verification mechanisms, based on logical techniques for specifying and verifying network functions as SDN applications. This thesis is focused on verifying the availability and network management based policies, and these policies are used for the specification and validation configurations. This research focuses on four aspects: 1) verification of invariants to validate network topologies, 2) network security by verifying firewall functions, 3) auditing of network settings against high-level policies, and 4) the validation of a SDN model as interdependent networks that suffers a sequential targeted attack

Las redes definidas por software o Software-Defined Networking (SDN) son una tecnología para elaborar redes de comunicaciones que separa la capa de control de red de la capa de datos (reenvío de paquetes). Esta separación permite mayor flexibilidad al momento de establecer nuevas configuraciones. De esta forma, los administradores de red pueden controlar la red por medio de software sin necesidad de acceder a la configuración física de cada dispositivo. Las redes SDN han cobrado mayor importancia en la actualidad debido al crecimiento acelerado de virtualización en computación. Por otro lado, este tipo de tecnología responde rápidamente a los cambios que se pueden presentar en la red debido a su funcionamiento, fallas de seguridad o incidentes. Es decir, la red puede ser reprogramada para responder ante la dinámica de las circunstancias. Funciones de red como balanceadores de carga, firewalls, y sistemas de detección de intrusos pueden ser programados como reglas de tráfico. Sin embargo, esta tecnología se encuentra en una etapa de desarrollo temprana y aún enfrenta interesantes desafíos para su utilización. Uno de los que genera más impacto son los errores en la programación y configuración. Este tipo de errores son los más comunes y representan entre el 50% y el 80% de los fallos de red. Esta tesis de doctorado busca contribuir en mecanismos de verificación, basados en técnicas matemáticas para la especificación y verificación de funciones de red como aplicaciones para SDN. Esta tesis está orientada a la administración de redes basada en políticas, y dichas políticas son usadas para la especificación y validación de las configuraciones. Esta investigación se enfoca en tres aspectos: la verificación de invariantes de red para validar topologías, seguridad en redes mediante la verificación de funciones de firewall y una auditoría sobre las configuraciones dadas políticas de red de alto nivel