Networks are difficult to configure correctly, and tricky to debug. These problems are accentuated by temporal and stateful behavior. Static verification, while useful, is ineffectual for detecting behavioral deviations induced by hardware faults, security failures, and so on, so dynamic property monitoring is also valuable. Unfortunately, existing monitoring and runtime verification for networks largely focuses on properties about individual packets (such as connectivity) or requires a digest of all network events be sent to a server, incurring enormous cost. We present a network monitoring system that avoids these problems. Because traces of network events correspond well to temporal logic, we use a subset of Metric First-Order Temporal Logic as the query language. These queries are compiled down to execute completely on the network switches. This vastly reduces network load, improves the precision of queries, and decreases detection latency. We show the practical feasibility of our work by extending a widely-used software switch and deploying it on networks. Our work also suggests improvements to network instruction sets to better support temporal monitoring.
Purely static tools, such as network configuration analyzers @cite_34 @cite_28 @cite_11 @cite_2 @cite_9 @cite_19 and languages built for analysis (e.g., @cite_13 @cite_35 ) are powerful but not sufficient for robust network testing. Veriflow @cite_29 statically analyzes to (stateless) OpenFlow switch rules in real time. This hybrid approach is nevertheless limited to switches governed by an SDN controller. Since our approach only on SDN switches, it can be used even in a hybrid network. @cite_20 enhance SDN programs with annotations that reference program state directly. These compile to new VeriFlow assertions as the program state changes, and are therefore limited to analyzing switch-rule updates.
@cite_35 @cite_28 @cite_9 @cite_29 @cite_19 @cite_2 @cite_34 @cite_13 @cite_20 @cite_11
1675033504 1697123834 2122695394 106863888
Networks are complex and prone to bugs. Existing tools that check network configuration files and the data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise. Is it possible to check network-wide invariants in real time, as the network state evolves? The key challenge here is to achieve extremely low latency during the checks so that network performance is not affected. In this paper, we present a design, VeriFlow, which achieves this goal. VeriFlow is a layer between a software-defined networking controller and network devices that checks for network-wide invariant violations dynamically as each forwarding rule is inserted, modified or deleted. VeriFlow supports analysis over multiple header fields, and an API for checking custom invariants. Based on a prototype implementation integrated with the NOX OpenFlow controller, and driven by a Mininet OpenFlow network and Route Views trace data, we find that VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion or deletion. 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. Networks are complex and prone to bugs. Existing tools that check configuration files and data-plane state operate offline at timescales of seconds to hours, and cannot detect or prevent bugs as they arise. Is it possible to check network-wide invariants in real time, as the network state evolves? The key challenge here is to achieve extremely low latency during the checks so that network performance is not affected. In this paper, we present a preliminary design, VeriFlow, which suggests that this goal is achievable. VeriFlow is a layer between a software-defined networking controller and network devices that checks for network-wide invariant violations dynamically as each forwarding rule is inserted. Based on an implementation using a Mininet OpenFlow network and Route Views trace data, we find that VeriFlow can perform rigorous checking within hundreds of microseconds per rule insertion. Software defined networking (SDN) and OpenFlow as one of its key technologies have received a lot of attention from the networking community. While SDN enables complex network applications and easier network management, the paradigm change comes along with new security threats. In this paper, we analyze attacks against a software-defined network in a scenario where the attacker has been able to compromise one or more OpenFlow-capable switches. We find out that such attacker can in suitable environments perform a wide range of attacks, including man-in-the-middle attacks against control-plane traffic, by using only the standard OpenFlow functionality of the switch. Furthermore, we show that in certain scenarios it is nearly impossible to detect that some switch has been compromised. We conclude that while the existing security mechanisms, such as TLS, give protection against many of the presented attacks, the threats should not be overlooked when moving to SDN and OpenFlow.