VERCEL: Verification and Rectification of Configuration Errors with Least Squares

TL;DR

A key highlight of Vercel is that while evaluating for reachability, the tool can incorporate intents, and transform these into auto-configurable table entries, implying a recommendation/correction system.

Abstract

We present Vercel, a network verification and automatic fault rectification tool that is based on a computationally tractable, algorithmically expressive, and mathematically aesthetic domain of linear algebra. Vercel works on abstracting out packet headers into standard basis vectors that are used to create a port-specific forwarding matrix $\mathcal{A}$, representing a set of packet headers/prefixes that a router forwards along a port. By equating this matrix $\mathcal{A}$ and a vector $b$ (that represents the set of all headers under consideration), we are able to apply \textit{least squares} (which produces a column rank agnostic solution) to compute which headers are reachable at the destination. Reachability now simply means evaluating if vector $b$ is in the column space of $\mathcal{A}$, which can efficiently be computed using least squares. Further, the use of vector representation and least squares opens new possibilities for understanding network behavior. For example, we are able to map rules, routing policies, what-if scenarios to the fundamental linear algebraic form, $\mathcal{A}x=b$, as well as determine how to configure forwarding tables appropriately. We show Vercel is faster than the state-of-art such as NetPlumber, Veriflow, APKeep, AP Verifier, when measured over diverse datasets. Vercel is almost as fast as Deltanet, when rules are verified in batches and provides better scalability, expressiveness and memory efficiency. A key highlight of Vercel is that while evaluating for reachability, the tool can incorporate intents, and transform these into auto-configurable table entries, implying a recommendation/correction system.

Figures (7)

• Figure 1: (a) A toy network of 4 routers in which a new rule at router $Q$ is being inserted in its forwarding table (shown in dashed block). Vercel represents all rules in a binary tree and after insertion of a new rule, identifies 3 headers whose reachability might be affected. (b) An example to demonstrate reachability between router $Y$ and $R$ along the path $Y-U-R$ with least squares. Vercel represents 3 headers in 3-dimension with the orthogonal vectors. Forwarding rules of routers $Y$ and $U$ are represented in $x$-$y$ and $y$-$z$ planes, respectively. Vercel computes reachability by sequentially projecting a point in 3-dimension to the subspace created for router $Y$ and $U$.
• Figure 2: Steps for Vercel’s handling of user-specified intent related to service configuration (in the network shown on the right side of the figure).
• Figure 3: Example demonstrating internals of Vercel's rectification system. Initially, $R$ is not reachable from $Y$. However, after applying Vercel's rectification at $Q$, reachability till $R$ is ensured along the path $Y-U-Q-R$.
• Figure 4: Vercel components.
• Figure 5: CDF of the verification time of Vercel on 8 datasets deltanet-datsetstanford-datset during a rule update.