Validation of availability and policy based management for programmable networks (2016)
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