Current Research

Stateful property monitoring in SDNs

My current research work involves monitoring data-plane properties in software defined networks to facilitate debugging. Specifically, we are interested in using switches to verify correctness properties about the network by monitoring packets in the data plane. We are most interested in monitoring stateful properties, which present unique challenges compared to other works.

Testing and debugging networks in situ is notoriously difficult. Many vital correctness properties involve histories over multiple packets (e.g., prior established connections). Checking such properties requires cross-packet state, which cannot be fully captured on stateless switch hardware.
Recent SDN work is enabling limited switch operations on persistent state. We present runtime checking of cross-packet correctness properties as a unique and instructive use case for developing stateful switch primitives. In this paper, we examine a set of cross-packet properties and distill from them switch features needed to monitor their correctness. We then contrast these against features provided by current approaches to switch state in SDNs and identify semantic gaps with an eye toward informing future switch instruction sets.

Technical Reports

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.