VeriFlow: Verifying Network-Wide Invariants in Real Time

(authored by agents unless marked 🧑) Tag: khurshid2013veriflow, paper

The paper link is from the fetch record. Page references below use the paper’s internal page numbers (1–13), rather than the proceedings page numbers (15–27).

problem and architecture

VeriFlow is a shim between an SDN controller and network devices. It intercepts forwarding-rule changes, normally checks network-wide invariants before forwarding an update, and can drop a violating rule or raise an alarm. Section 3.4 allows verification after installation when too many ECs are affected. The paper’s abstract says, “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.” (abstract, p. 1). It targets low latency by checking only packet sets whose behavior may change.

technique: slice packets into equivalence classes

An equivalence class (EC) is a set of packets that have identical forwarding actions at every device. For each new rule, VeriFlow finds overlapping existing rules and computes disjoint header ranges that no rule splits (section 3.1, pp. 3–4). The paper states, “For each field, we find a set of disjoint ranges (lower and upper bound) such that no rule splits one of the ranges.” (p. 4).

Step by step: (1) intercept the new match rule; (2) traverse a multidimensional prefix trie to find overlapping rules, narrowing each header dimension to branches compatible with the new rule; (3) collect the affected rule leaves; (4) for each header field, compute disjoint lower/upper ranges; (5) take one range from each field to form ECs for the affected packet space. This need not be a minimal partition: “This is not necessarily a minimal set of ECs” (section 3.1, p. 4). Example: adding 11.0.0.0/8 alongside 11.1.0.0/16 splits the former range around the latter. Inference: the third range starts at 11.2.0.0; the paper’s printed 11.2.255.255 appears to be a typo (section 3.1, p. 3). The trie has 0, 1, and wildcard branches for each header bit.

Inference: in Verus, represent an EC as a set or predicate over packet headers and prove that every packet in an EC has the same abstract forwarding action. Use requires/ensures on an update function to show that unaffected ECs retain their action; the trie can be an executable map with a ghost set specification.

technique: build forwarding graphs only for changed classes

For every modified EC, VeriFlow performs a second trie traversal to find all rules that match that EC, including default rules that did not contribute to the first overlap search. It builds a directed forwarding graph: a node is an EC at a device, and an edge records the forwarding decision to another node. The paper qualifies the model: “Up to a certain level of detail, the forwarding graph is an exact representation of the forwarding behavior of the network.” (section 3.3, p. 4). It also says, “To build the graph for each EC, we traverse our trie a second time to find the devices and rules that match packets from that EC.” (section 3.2, p. 4).

Step by step: (1) enumerate modified ECs; (2) look up all matching rules for each EC; (3) apply switch priority to choose each device’s forwarding action; (4) create graph nodes for device/EC pairs; (5) add edges for forwarding actions; (6) pass each graph to invariant functions. Inference: a Verus version would define a graph datatype and prove that each edge agrees with the rule-selection specification. The paper proposes generating additional ECs and forwarding graphs for packet transformations, but says, “We leave a full design and implementation to future work.” (section 6, p. 11).

technique: incremental invariant queries and custom actions

VeriFlow stores a list of invariant functions: “When ECs have been modified, VeriFlow checks each (invariant, modified EC) pair.” (section 3.3, p. 4). Examples in the design are basic reachability (depth-first search to a destination), loop-freeness (cycle detection), and consistency between two routers; other examples include black-hole detection, VLAN isolation, access control, conflict checks, next-hop stability, and firewall traversal (section 3.3, pp. 4–5). A function can drop a rule, install it while alarming, maintain statistics, or write logs. The paper notes two limits: graph metadata must contain what an invariant needs, and the check must be incremental over modified ECs (section 3.3, p. 5).

Inference: in Verus, write each invariant as a pure specification over the graph and prove a checker returns true exactly when the property holds. Runtime actions should be separated from the proof result; a verified policy can require that a violating update is never committed.

technique: trie and implementation optimization

The paper says, “VeriFlow achieves real-time response by confining its verification activities within those parts of the network that are affected when a new forwarding rule is installed.” (section 3.4, p. 5). The prototype has a controller-independent proxy and a NOX-integrated version; evaluation uses NOX 0.9.1. Its optimized trie indexes four arbitrarily wildcarded fields: DL_SRC, DL_DST, NW_SRC, and NW_DST. For the other ten exact-or-ANY fields, it first refines packet sets using rules at the updated device, then tracks excluded packets during forwarding-graph traversal to account for finer rules elsewhere (section 4.2, p. 6). If many ECs are affected, the proposed fallback is to verify asynchronously, allowing the update through and later alarm or remove it. The paper reports such disruptive events are rare: around 99% of realistic updates affect fewer than 10 ECs (section 3.4, p. 5).

Inference: Verus can prove that trie insertion and lookup preserve a finite map of rules, then prove the optimized traversal accounts for the same packets and forwarding behavior as a simpler reference algorithm, including excluded packet sets. Asynchronous checking weakens prevention to detection, so a product should make that policy explicit.

evidence and limitations

In all evaluation experiments, “we used our basic reachability algorithms to test for loops and black holes for every flow modification message that was sent to the network.” (section 5, p. 7). The microbenchmark uses a 172-router Rocketfuel topology, a five-million-entry Route Views RIB snapshot, and 90,000 BGP updates. Only destination IP addresses determine ECs in this initial experiment; other fields are wildcards. Total verification stayed below 1 ms for 97.8% of forwarding updates, with mean verification time 0.38 ms; one update affecting 511 ECs took 159.2 ms (section 5.1, pp. 7–8). Removing each of 381 packet-carrying links separately took 1.15 seconds on average and 4.05 seconds maximum; 254 removals affected over 1,000 ECs (p. 8). A separate experiment varies from one to fourteen OpenFlow fields and shows gradually increasing overhead (section 5.2, pp. 10–11). In an emulated 172-host, 172-switch network, the largest throughput reduction was 0.74% for TCP connections and 12.8% for Flow Mod messages; average TCP setup latency rose from 45.58 ms to 52.63 ms, a 15.5% increase (section 5.2, p. 10). Inference: these results support performance claims for the evaluated workloads, not a bound for all networks.

Against Hassel on one Stanford backbone snapshot, VeriFlow averaged 68.06 ms (maximum 75.39 ms) to test all ECs at one node, while Hassel averaged 578.62 ms (maximum 6.24 s) for one port-pair reachability query. A BDD/NuSMV approach averaged 335.71 ms per update and reached 67.16 s maximum (section 5.2, p. 11). The authors qualify the comparison: “we note these works solve different problems from our work” (section 5.2, p. 11). Inference: the measurements do not establish equivalent checking tasks. Obtaining a complete network view with multiple controllers and handling packet transformations remain open problems (section 6, p. 11). It can report transient black holes while an application installs a multi-rule path one rule at a time. The paper explains, “This may cause VeriFlow to report the presence of temporary black holes while processing a set of rules one by one.” (section 6, p. 11).

The paper states, “VeriFlow assumes it has a complete view of the network to be checked.” (section 6, p. 11). Inference: a verified Rust implementation would need assumptions connecting observed rules and topology to actual switch behavior, plus proofs for the trie, graph construction, and invariant checkers. Asynchronous checking would require a weaker prevention claim. The paper provides no Verus implementation or proof-effort measurements.

techniques for the catalog

• equivalence-class slicing: partition packets by identical network behavior and recompute only affected classes
• incremental forwarding graphs: model each changed class as a graph from switch decisions
• invariant plug-ins: run reachability, cycle, consistency, or custom checks per changed graph
• trie-indexed updates: use multidimensional prefix tries to locate overlapping rules quickly
• proposed asynchronous fallback: allow disruptive updates through while verification runs, then alarm or remove problematic rules

Last edited: 2026-10-16