Atomic Predicates

---

Atomic Predicates is the name of a packet equivalence relation defined by Hongkun Yang and Simon Lam in 2013 which can be used to reduce the computation time and space requirements of network verification by orders of magnitude.

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, 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 described below.

For an arriving packet to a packet filter, if the predicate evaluates to true for its header, 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. 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., source IP address.) In the worst case, the computation time of such set intersection/union is O(2ⁿ) 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 network verification, the reader is referred to the blog by Professor George Varghese of UCLA.

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}}$.

Their definition of Atomic Predicates in mathematical notation follows:

Consider a set $U$ of elements. A predicate Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P} specifies a subset of elements. Predicate true specifies Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U} . Predicate false specifies the empty set.

Definition 1 (Atomic Predicates): Given a set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathcal{P}} of predicates, its set of atomic predicates Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{p_1, \dots, p_k\}} satisfies these five properties:

1. $p_{i}\neq {\text{false}},\forall i\in \{1,\dots ,k\}$.
2. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \vee_{i=1}^k p_i = \text{true}} .
3. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle p_i\wedge p_j = \text{false, if } i\neq j } .
4. Each predicate Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P\in\mathcal{P}, P\neq\text{false}} , is equal to the disjunction of a subset of atomic predicates:

   Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P=\bigvee_{i\in S(P)} p_i, \text{where } S(P)\subseteq \{1,\dots,k\}.} (1)

5. Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle k} is the minimum number such that the set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \{p_1,\dots, p_k\}} satisfies the above four properties.

Note that if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P=\text{true}} , then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle S(P)=\{1,\dots,k\}} ; if $P={\text{false}}$, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle S(P)=\emptyset} . Since Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle p_1,\dots,p_k} are disjoint, the expression in (1) is unique for each predicate Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P\in\mathcal{P}} .

Given a set Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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.

Professor Gordon Plotkin (University of Edinburgh) coined the term “Yang-Lam Equivalence” for the equivalence relation specified by Atomic 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.

For reachability computations, each atomic predicate is identified by a unique integer. Thus a packet set is represented by a set of integers. To compute a reachability tree, intersection and union operations are performed on sets of integers.

For real networks, each atomic predicate represents a very large number of equivalent packets in numerous disjoint fragments of the packet space. Yang and Lam showed that the use of atomic predicates reduces the time and space required for computing and storing reachability trees, as well as for verifying reachability properties, by orders of magnitude.

Atomic Predicates for networks with packet transformers

Towards scalable verification of packet networks in the real world, where several types of packet transformers (IP in IP and MPLS tunnels, and NATs) are widely used, Yang and Lam developed a general theory of packet equivalence for networks with both transformers and filters. 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 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 their 2017 Transactions on Networking paper.

Open source software downloads

For networks with packet filters only APV download

For networks with packet filters and transformers APT download

This work has been re-implemented by Google for verifying its virtual private clouds.

References

This article "Atomic Predicates" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Atomic Predicates. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.

---