Networking Research Laboratory
Department of Computer Science
The University of Texas at Austin

Director: Simon S. Lam (more publications)

 

Atomic Predicates for Network Verification

Open source software downloads: networks with packet filters only, networks with packet filters and transformers (downloads have been disabled due to excessive spam).
This work has been re-implemented by Google for verifying its virtual private clouds.   

 

Atomic Predicates is the name of a packet equivalence relation defined in 2013 by Hongkun Yang and Simon Lam [1, 2] which can be used to reduce the computation time and space requirements of  network verification by orders of magnitude when compared to prior work [3].

Network Verification problem

Consider a packet network, such as any IP network.  The problem of network verification is to prove (by covering all cases) that some properties hold, for examples, “no packet will travel in a loop in the network,” “all packets with a source address x must pass through firewall y before delivery to destination z.” 

The topology of a packet network is a connected graph where nodes are boxes (routers, switches, and other middle boxes) and edges are communication links.  Each box has a set of input ports and a set of output ports. The state of the network in the “data plane” is determined by the forwarding tables and access control lists (ACLs) in the network's boxes.

Each packet consists of a string of header bits and a string of data bits.  The header is divided into many subfields, e. g., source IP address, destination IP address, source port number, destination port number, protocol, etc. 

Forwarding tables and ACLs can be parsed and represented by predicates that guard input and output ports of each box. The variables of such a predicate represent packet header bits. Conceptually both forwarding tables and ACLs are packet filters and work as follows: For each arriving packet to a packet filter, if the predicate evaluates to true for its header bits, then the packet passes through; else, it is dropped.

The above model for static reachability analysis of network state in the data plane was first presented in 2005 by Xie et al. [4], which can be analyzed as follows:

The set of packets that can travel from port to port through a sequence of packet filters can be obtained by computing the conjunction of predicates in the sequence (or by intersection of the corresponding packet sets).  This idea can be used to compute the reachability tree from any port to all other locations in the network.

However, the intersection and union of IP packet sets are highly computation-intensive because they operate on multi-dimensional sets which could have many allowed intervals in each dimension as well as arbitrary overlaps in each dimension between two packet sets. (Each dimension corresponds to a separate subfield in the header, e.g., destination IP address.) In the worst case, the computation time of such set intersection/union is O(2n) where n is the number of bits in the packet header. Efficiency of these operations determines the efficiency of reachability computation, irrespective of which formal method is used to compute reachability.

For a gentle and fun introduction to a variety of formal methods applied to the above network verification problem, the reader is referred to the blog, ''It’s the Equivalence Classes, Stupid," by Professor George Varghese of UCLA [5].

 

Atomic Predicates – the ultimate packet equivalence relation

There are many packet equivalence relations that are obvious and we use them without even explicitly thinking about it.  For examples, all packets with an identical packet header but different data bits are equivalent in network verification. Another example: all packets with the same destination IP address prefix can be considered to be an equivalence class. 

In 2013, Hongkun Yang and Simon Lam defined a novel idea of packet equivalence, namely: For a network with a set \( \mathcal{P} \) of packet filters, two packets are equivalent if and only if they are treated the same (drop or pass) by every filter in the set \( \mathcal{P} \).  The definition of Atomic Predicates in mathematical notation [1, 2] follows:

Consider a set \(U\) of elements. A predicate \(P\) specifies a subset of elements. Predicate true specifies \(U\). Predicate false specifies the empty set.

Definition 1 (Atomic Predicates): Given a set \( \mathcal{P} \) of predicates, its set of atomic predicates \( \{p_{1},\dots ,p_{k}\} \) satisfies these five properties:
  1. \(p_{i}\neq {\text{false}},\forall i\in \{1,\dots ,k\}\)
  2. \( \bigvee _{i=1}^{k}p_{i}=\text{true}.\)
  3. \( p_{i}\wedge p_{j}=\text{false, if }i\neq j.\)
  4. Each predicate \( P\in \mathcal{P},P\neq \text{false}\), is equal to the disjunction of a subset of atomic predicates: \begin{equation} P=\bigvee _{i\in S(P)}p_{i},\text{where }S(P)\subseteq \{1,\dots ,k\}. \text{ (1)} \end{equation}
  5. \(k \) is the minimum number such that the set \( \{p_{1},\dots ,p_{k}\}\) satisfies the above four properties.

Note that if \( P=\text{true}\), then \( S(P)=\{1,\dots ,k\}\); if \( P=\text{false}\), \( S(P)=\emptyset \). Since \( p_{1},\dots ,p_{k}\) are disjoint, the expression in (1) is unique for each predicate \( P\in \mathcal{P}\).

Given a set \(\mathcal{P}\), there are numerous sets of predicates that satisfy the first four properties of Definition 1. In the most trivial case, these four properties are satisfied by the set of predicates each of which specifies a single element. Atomic predicates must also satisfy property 5; they are the set with the smallest number of predicates.

Yang and Lam also presented an algorithm to compute from the set \( \mathcal{P} \) of predicates (representing all filters), its set of atomic predicates, together with a proof that the algorithm terminates and the resulting set of predicates is smallest [1, 2].

 

For reachability computations, each atomic predicate is identified by a unique integer. To compute a reachability tree, intersection and union operations are performed on sets of integers.  Thus the computation and storage of rearchability trees are highly efficient.

For real networks, each atomic predicate typically represents a very large number of equivalent packets in numerous disjoint fragments of the packet space.  Thus the use of atomic predicates reduces the time and space required for computing and storing these trees, as well as for verifying reachability properties, by orders of magnitude compared to prior work [3].

Professor Gordon Plotkin of the University of Edinburgh coined the term “Yang-Lam Equivalence” for the equivalence relation specified by a set of atomic predicates [6].

Professor George Varghese of UCLA wrote “The full fruition of this idea (equivalence) came with the Atomic Predicates paper by Yang and Lam.” [5] 

 

Atomic Predicates for networks with packet transformers

Towards scalable verification of packet networks in the real world, where several types of packet transformers (e.g., IP-in-IP and MPLS tunnels, and network address translation gateways) are widely used,  When a packet arrives at a transformer, it may be filtered. If not filtered, it may exit unchanged, exit as another packet (deterministic transformation), or exit as any packet in a specified set of packets (non-deterministic transformation).

A general theory of packet equivalence. Every packet injected into the network may possibly be transformed into other packets by any sequence of transformers in the network. Yang and Lam  conceived a new packet equivalence relation that formalizes the following intuition: namely, two packets are equivalent if and only if they are treated identically by every filter and by every possible sequence of one or more transformers in the network.  Subsequently, they solved two additional hard problems: (i) formulating a new definition of atomic predicates for transformers and filters with a proof that they specify the coarsest equivalence classes of packets, and (ii) designing a new algorithm for computing atomic predicates for transformers and filters with a proof that the algorithm terminates and, upon termination, it returns the set of atomic predicates. The definition, algorithm, and theorems, as well as a comprehensive performance evaluation using four large real-world datasets are presented in [7]

 

References

  1. Hongkun Yang and Simon S. Lam, "Real-time Verification of Network Properties Using Atomic Predicates,'' Proceedings of IEEE International Conference on Network Protocols 2013, Göttingen, Germany, October 2013.
  2. Hongkun Yang and Simon S. Lam, "Real-time Verification of Network Properties Using Atomic Predicates,'' IEEE/ACM Transactions on Networking, April 2016, Volume 24, No. 2.

  3. P. Kazemian, G. Varghese, and N. McKeown, "Header space analysis:Static checking for networks," in Proceedings USENIX NSDI, San Jose, California, 2012.

  4. Geoffrey G. Xie et al., "On Static Reachability Analysis of IP Networks,'' Proceedings IEEE INFOCOM, Miami, Florida, 2005.

  5. George Varghese, "It's the Equivalence Classes, Stupid," netverify.fun website, March 26, 2020.

  6. Gordon Plotkin, et al., "Scaling Network Verification using Symmetry and Surgery,'' Proceedings ACM POPL 2016, St. Petersburg, Florida, January 2016 (doi/10.1145/2837614.2837657).

  7. Hongkun Yang and Simon S. Lam, "Scalable Verification of Networks With Packet Transformers Using Atomic Predicates,'' IEEE/ACM Transactions on Networking, October 2017, Volume 25, No. 5.

 

The text of this webpage is available for modification and reuse under the terms of the Creative Commons Attribution-Sharealike 3.0 Unported License and the GNU Free Documentation License (unversioned, with no invariant sections, front-cover texts, or back-cover texts).