Department of Computer Sciences

The University of Texas at Austin

Director:
**Simon S. Lam**
(more publications)

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.

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)*.