University of Texas at Austin Department of Computer SciencesNetworking Research Laboratory
Department of Computer Sciences
The University of Texas at Austin

Director: Simon S. Lam (more publications)

Scalable Network Verification Using Atomic Predicates

For networks with packet filters only, which model forwarding tables and access control lists, packet equivalence is intuitive. This is because when a packet arrives at a filter, it either exits unchanged or is filtered. Informally, two packets are equivalent if and only if they are treated identically by every filter in the network. In the following papers, atomic predicates are defined which specify the coarsest equivalence classes of packets.  We present efficient algorithms for computing these atomic predicates.

For real networks, each atomic predicate represents a very large number of equivalent packets in many disjoint fragments of the packet space.  Our verifier computes reachability trees for atomic predicates, each of which represents a very large number of packets with equivalent behavior, rather than for individual packets. 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.

Hongkun Yang and Simon S. Lam, ``Real-time Verification of Network Properties Using Atomic Predicates,'' Proceedings of IEEE ICNP 2013, Göttingen, Germany, October 2013.

Hongkun Yang and Simon S. Lam, ``Real-time Verification of Network Properties using Atomic Predicates,'' IEEE/ACM Transactions on Networking, April 2016, Volume 24, Issue 2, pages 887-900 (first published as IEEE Early Access Article, 2015, Digital Object Identifier: 10.1109/TNET.2015.2398197).

Plotkin et al. \cite{POPL2016} refer to atomic predicates defined in the above papers as "Yang-Lam equivalence."

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, we set out to develop 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. We 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, we 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 the following paper:

Hongkun Yang and Simon S. Lam, ``Scalable Verification of Networks With Packet Transformers Using Atomic Predicates,'' IEEE/ACM Transactions on Networking, 2017, Volume PP, Issue 99, pages 1-16 (first published as IEEE Early Access Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).