Systematically testing OpenFlow controller applications

The emergence of OpenFlow-capable switches enables exciting new network functionality, at the risk of programming errors that make communication less reliable. The centralized programming model, where a single controller program manages the network, seems to reduce the likelihood of bugs. However, the system is inherently distributed and asynchronous, with events happening at different switches and end hosts, and inevitable delays affecting communication with the controller. In this paper, we present efficient, systematic techniques for testing unmodified controller programs. Our NICE tool applies model checking to explore the state space of the entire system the controller, the switches, and the hosts. Scalability is the main challenge, given the diversity of data packets, the large system state, and the many possible event orderings. To addressthis, we propose a novel way to augment model checking with symbolic execution of event handlers (to identify representative packets that exercise code paths on the controller). We also present a simplified OpenFlow switch model (to reduce the state space), and effective strategies for generating event interleavings likely to uncover bugs. Our prototype tests Python applications on the popular NOX platform. In testing three real applications-a MAC-learning switch, in-network server load balancing, and energy-efficient traffic engineering-we uncover 13 bugs. (C) 2015 Elsevier B.V. All rights reserved.

A NICE Way to Test OpenFlow Applications

Marco Canini, Dejan Kostic, Peter Peresini, Jennifer Rexford

The emergence of OpenFlow-capable switches enables exciting new network functionality, at the risk of programming errors that make communication less reliable. The centralized programming model, where a single controller program manages the network, seems to reduce the likelihood of bugs. However, the system is inherently distributed and asynchronous, with events happening at different switches and end hosts, and inevitable delays affecting communication with the controller. In this paper, we present efficient, systematic techniques for testing unmodified controller programs. Our NICE tool applies model checking to explore the state space of the entire system—the controller, the switches, and the hosts. Scalability is the main challenge, given the diversity of data packets, the large system state, and the many possible event orderings. To address this, we propose a novel way to augment model checking with symbolic execution of event handlers (to identify representative packets that exercise code paths on the controller). We also present a simplified OpenFlow switch model (to reduce the state space), and effective strategies for generating event interleavings likely to uncover bugs. Our prototype tests Python applications on the popular NOX platform. In testing three real applications—a MAC-learning switch, in-network server load balancing, and energy-efficient traffic engineering—we uncover eleven bugs.

2012

Simplifying Development and Management of Software-Defined Networks

Peter Peresini

Computer networks are an important part of our life. Yet, they are traditionally hard to manage and operate. The recent shift to Software-Defined Networking (SDN) is promised to change the way in which the networks are run by their operators. However, SDN is still in its initial stage and as such it lags behind traditional networks in terms of correctness and reliability; both the properties being vitally important for the network operators. Meanwhile, general purpose computers were following Moore's law for years and as a result, together with algorithmic improvements, the costs of computing have been declining --- we have more processing power available to us than anytime before. In this dissertation I strive to reduce the correctness and reliability gap of SDN and help speed up the adoption of SDN by providing tools that help programmers and operators gain confidence in their networks. These tools leverage the today's trend in the increasing availability of vast amounts of computing power and combine it with the past research on systematic validation, optimization and satisfiability solving. The first tool this thesis introduces, NICE, focuses on debugging of an SDN controller. In particular, while SDN is conceptually a centralized system with the controller in the command, SDN is still a distributed system. As such, programmers might miss various event interleavings and race conditions that lead to a buggy behavior. NICE uncovers such insidious bugs by systematically exploring possible network states by a novel combination of two techniques -- symbolic execution and model checking. The combination of the two techniques and SDN-related heuristics let NICE explore possible scenarios deeper than any existing technique alone. This thesis also introduces Monocle, a tool aimed at ensuring reliability of SDN switches. Specifically, Monocle continuously verifies that a switch data plane processes packets as configured by the SDN controller. Such monitoring is important in the presence of silent errors ranging from switch firmware bugs, through memory corruption, to transient inconsistencies. To verify that the switch data plane works as intended, Monocle constructs data plane packets and injects them into the network. Such packet construction is, however, a rather intricate problem when considering a complicated nature of the switch packet matching mechanism in the presence of multiple overlapping rules. In the thesis I formally describe the constraints that the generated packets need to satisfy, and I leverage an off-the-shelf satisfiability solver to solve them. Finally, this thesis introduces ESPRES, a tool focused on scheduling network updates. I first observe that big network updates such as traffic engineering or failure re-routing usually contain many subupdates that are independent (e.g, updates of different flows). Then I conjecture that while the length of the total update is bottlenecked by the slowest switch, the time when an individual subupdate finishes can be greatly improved for a majority of them. To achieve this goal in an online fashion, ESPRES uses a greedy mechanism to reorder individual switch commands according to the current situation on different switches.

EPFL2016

Cybersecurity Solutions for Active Power Distribution Networks

Teklemariam Tsegay Tesfay

An active distribution network (ADN) is an electrical-power distribution network that implements a real-time monitoring and control of the electrical resources and the grid. Effective monitoring and control is realised by deploying a large number of sensing and actuating devices and a communication network to facilitates the two-way transfer of data. The reliance of ADN operations on a large number of electronic devices and on communication networks poses a challenge in protecting the system against cyber-attacks. Identifying these challenges and commissioning appropriate solutions is of utmost importance to realize the full potential of a smart grid that seamlessly integrates distributed generation, such as renewable energy sources. As a first step, we perform a thorough threat analysis of a typical ADN. We identify potential threats against field devices, the communication infrastructure and servers at control centers. We also propose a check-list of security solutions and best practices that guarantee a distribution network's resilient operation in the presence of malicious attackers, natural disasters, and other unintended failures that could potentially lead to islanded communication zone. For the next step, we investigate the security of MPLS-TP, a technology that is mainly used for long-distance inter-domain communication in smart grid. We find that an MPLS-TP implementation in Cisco IOS has serious security vulnerabilities in two of its protocols, BFD and PSC. These two protocols control protection-switching features in MPLS-TP. In our test-bed, we demonstrate that an attacker who has physical access to the network can exploit the vulnerabilities in order to inject forged BFD or PSC messages that affect the network's availability. Third, we consider multicast source authentication for synchrophasor data communication in grid monitoring systems (GMS). Ensuring source authentication without violating the stringent real-time requirement of GMS is challenging. Through an extensive review of existing schemes, we identified a set of schemes that satisfy some desirable requirements for GMS. The identified schemes are ECDSA, TV-HORS and Incomplete- key-set. We experimentally compared these schemes using computation, communication and key management overheads as performance metrics. A tweak in ECDSA's implementation to make it use pre-generated tokens to generate signatures significantly improves the computation overhead of ECDSA, making it the preferred scheme for GMS. This finding is contrary to the generally accepted view that asymmetric cryptography is inapplicable for real-time systems. Finally, we studied a planning problem that arises when a utility wants to roll out a software patch that requires rebooting to all PMUs while maintaining system observability. The problem we address is how to find a partitioning of the set of the deployed PMUs into as few subsets as possible such that all the PMUs in one subset can be patched in one round while all the PMUs in the other subsets provide full observability. We show that the problem is NP-complete in the general case and and formulated it as binary integer linear programming (BILP) problem. We have also provided an heuristic algorithm to find an approximate solution. Furthermore, we have identified a special case of the problem where the grid is a tree and provided a polynomial-time algorithm that finds an optimal patching plan that requires only two rounds to patch the PMUs.