Biblio

Network operators face a challenge of ensuring correctness as networks grow more complex, in terms of scale and increasingly in terms of diversity of software components. Network-wide verification approaches can spot errors, but assume a simplified abstraction of the functionality of individual network devices, which may deviate from the real implementation. In this paper, we propose a technique for high-coverage testing of end-to-end network correctness using the real software that is deployed in these networks. Our design is effectively a hybrid, using an explicit-state model checker to explore all network-wide execution paths and event orderings, but executing real software as subroutines for each device. We show that this approach can detect correctness issues that would be missed both by existing verification and testing approaches, and a prototype implementation suggests the technique can scale to larger networks
with reasonable performance.

Recent years have seen significant advancement in the field of formal network verification. Tools have been proposed for offline data plane verification, real-time data plane verification and configuration verification under arbitrary, but static sets of failures. However, due to the fundamental limitation of not treating the network as an evolving system, current verification platforms have significant constraints in terms of scope. In real-world networks, correctness policies may be violated only through a particular combination of environment events and protocol actions, possibly in a non-deterministic sequence. Moreover, correctness specifications themselves may often correlate multiple data plane states, particularly when dynamic data plane elements are present. Tools in existence today are not capable of reasoning about all the possible network events, and all the subsequent execution paths that are enabled by those events. We propose Plankton, a verification platform for identifying undesirable evolutions of networks. By combining symbolic modeling of data plane and control plane with explicit state exploration, Plankton
performs a goal-directed search on a finite-state transition system that captures the behavior of the network as well as the various events that can influence it. In this way, Plankton can automatically find policy violations that can occur due to a sequence of network events, starting from the current state. Initial experiments have successfully predicted scenarios like BGP Wedgies.

Enterprise networks today have highly diverse correctness requirements and relatively common performance objectives. As a result, preferred abstractions for enterprise networks are those which allow matching correctness specification, while transparently managing performance. Existing SDN network management architectures, however, bundle correctness and performance as a single abstraction. We argue that this creates an SDN ecosystem that is unnecessarily hard to build, maintain and evolve. We advocate a separation of the diverse correctness abstractions from generic performance optimization, to enable easier evolution of SDN controllers and platforms. We propose Oreo, a first step towards a common and relatively transparent performance optimization layer for SDN. Oreo performs the optimization by first building a model that describes every flow in the network, and then performing network-wide, multi-objective optimization based on this model without disrupting higher level correctness.

Commercial networks today have diverse security policies, defined by factors such as the type of traffic they carry, nature of applications they support, access control objectives, organizational principles etc. Ideally, the wide diversity in SDN controller frameworks should prove helpful in correctly and efficiently enforcing these policies. However, this has not been the case so far. By requiring the administrators to implement both security as well as performance objectives in the SDN controller, these frameworks have made the task of security policy enforcement in SDNs a challenging one. We observe that by separating security policy enforcement from performance optimization, we can facilitate the use of SDN for flexible policy management. To this end, we propose Oreo, a transparent performance enhancement layer for SDNs. Oreo allows SDN controllers to focus entirely on a correct security policy enforcement, and transparently optimizes the dataplane thus defined, reducing path stretch, switch memory consumption etc. Optimizations are performed while guaranteeing that end-to-end reachability characteristics are preserved – meaning that the security policies defined by the controller are not violated. Oreo performs these optimizations by first constructing a network-wide model describing the behavior of all traffic, and then optimizing the paths observed in the model by solving a multi-objective optimization problem. Initial experiments suggest that the techniques used by Oreo is effective, fast, and can scale to commercial-sized networks.

Commercial networks today have diverse security policies, defined by factors such as the type of traffic they carry, nature of applications they support, access control objectives, organizational principles etc. Ideally, the wide diversity in SDN controller frameworks should prove helpful in correctly and efficiently enforcing these policies. However, this has not been the case so far. By requiring the administrators to implement both security as well as performance objectives in the SDN controller, these frameworks have made the task of security policy enforcement in SDNs a challenging one. We observe that by separating security policy enforcement from performance optimization, we can facilitate the use of SDN for flexible policy management. To this end, we propose Oreo, a transparent performance enhancement layer for SDNs. Oreo allows SDN controllers to focus entirely on a correct security policy enforcement, and transparently optimizes the dataplane thus defined, reducing path stretch, switch memory consumption etc. Optimizations are performed while guaranteeing that end-to-end reachability characteristics are preserved – meaning that the security policies defined by the controller are not violated. Oreo performs these optimizations by first constructing a network-wide model describing the behavior of all traffic, and then optimizing the paths observed in the model by solving a multi-objective optimization problem. Initial experiments suggest that the techniques used by Oreo is effective, fast, and can scale to commercial-sized networks.