How Delta-net Achieves Sub‑Millisecond Real‑Time Network Verification with Atoms

As computer networks grow in scale and complexity, configuration errors and hardware faults increasingly cause forwarding loops, blackholes, and reachability problems that can lead to severe economic and societal impacts. Manual debugging is slow and error‑prone, prompting researchers to seek automated network verification.

Most real‑time verification techniques rely on two observations: (1) a single data‑plane update affects only a small portion of forwarding behavior, and (2) many packets share identical forwarding paths. The first enables incremental verification between snapshots, while the second allows analysis by packet equivalence classes.

Delta‑net innovatively represents packets as integer intervals and models the data‑plane forwarding as an edge‑labeled directed graph. When a new rule is added, Delta‑net creates new Atoms (if needed) and updates the Atom labels on each edge to keep the graph consistent with actual forwarding. Each Atom denotes a set of packets that exhibit identical forwarding throughout the network.

To illustrate the Atom construction, Delta‑net splits all IP prefixes of the network rules into disjoint half‑open intervals [lo, hi). Initially there is a single Atom representing the whole IPv4 space [0, 2^32). New rules cause these intervals to be partitioned into multiple adjacent half‑open intervals, each becoming a distinct Atom. By labeling graph edges with multiple Atoms, the complete forwarding behavior is captured.

With the Atom‑labeled graph, Delta‑net can incrementally build a forwarding sub‑graph and quickly verify reachability properties such as the absence of forwarding loops whenever a rule is inserted or deleted. The design also maps known algorithmic techniques to network verification: set union and intersection over Atom collections replace max‑plus operations, allowing the Floyd–Warshall algorithm to compute the transitive closure of packet flows.

Performance evaluation was conducted with roughly 4,000 lines of C++ code on a 3.47 GHz Intel Xeon CPU with 94 GB RAM. For each rule insertion or deletion, an incremental forwarding graph was constructed and checked for loops. Across all datasets, verification time per update remained in the microsecond range, thanks to the efficient interval‑based Atom representation.

Beyond update verification, Delta‑net supports “what‑if” queries: after a link failure, the system clears Atom labels on the failed edge and re‑verifies forwarding, enabling rapid (millisecond‑level) analysis of catastrophic network events.

In summary, the interval‑based Atom model allows Delta‑net to achieve sub‑millisecond real‑time verification of network policies and to swiftly analyze disaster scenarios such as link failures.