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.
Narayana, et al @cite_10 compile path queries'' about packet forwarding to switches. Path queries, by their nature, are distributed across multiple switches, whereas we compile stateful queries only for single switches. Path queries are restricted to regular expressions over possible forwarding paths, and so cannot express the array of stateful properties that targets, but do not require extensions to OpenFlow.
@cite_10
2303191924
Measuring the flow of traffic along network paths is crucial for many management tasks, including traffic engineering, diagnosing congestion, and mitigating DDoS attacks. We introduce a declarative query language for efficient path-based traffic monitoring. Path queries are specified as regular expressions over predicates on packet locations and header values, with SQL-like "groupby" constructs for aggregating results anywhere along a path. A run-time system compiles queries into a deterministic finite automaton. The automaton's transition function is then partitioned, compiled into match-action rules, and distributed over the switches. Switches stamp packets with automaton states to track the progress towards fulfilling a query. Only when packets satisfy a query are the packets counted, sampled, or sent to collectors for further analysis. By processing queries in the data plane, users "pay as they go", as data-collection overhead is limited to exactly those packets that satisfy the query. We implemented our system on top of the Pyretic SDN controller and evaluated its performance on a campus topology. Our experiments indicate that the system can enable "interactive debugging"-- compiling multiple queries in a few seconds--while fitting rules comfortably in modern switch TCAMs and the automaton state into two bytes (e.g., a VLAN header).